Finite partitions

In this file, we define finite partitions. A finpartition of a : α is a finite set of pairwise disjoint parts parts : Finset α which does not contain ⊥ and whose supremum is a.

Finpartitions of a finset are at the heart of Szemerédi's regularity lemma. They are also studied purely order theoretically in Sperner theory.

Constructions

We provide many ways to build finpartitions:

• Finpartition.ofErase: Builds a finpartition by erasing ⊥ for you.
• Finpartition.ofSubset: Builds a finpartition from a subset of the parts of a previous finpartition.
• Finpartition.empty: The empty finpartition of ⊥.
• Finpartition.indiscrete: The indiscrete, aka trivial, aka pure, finpartition made of a single part.
• Finpartition.discrete: The discrete finpartition of s : Finset α made of singletons.
• Finpartition.bind: Puts together the finpartitions of the parts of a finpartition into a new finpartition.
• Finpartition.ofSetoid: With Fintype α, constructs the finpartition of univ : Finset α induced by the equivalence classes of s : Setoid α.
• Finpartition.atomise: Makes a finpartition of s : Finset α by breaking s along all finsets in F : Finset (Finset α). Two elements of s belong to the same part iff they belong to the same elements of F.

Finpartition.indiscrete and Finpartition.bind together form the monadic structure of Finpartition.

Implementation notes

Forbidding ⊥ as a part follows mathematical tradition and is a pragmatic choice concerning operations on Finpartition. Not caring about ⊥ being a part or not breaks extensionality (it's not because the parts of P and the parts of Q have the same elements that P = Q). Enforcing ⊥ to be a part makes Finpartition.bind uglier and doesn't rid us of the need of Finpartition.ofErase.

TODO

The order is the wrong way around to make Finpartition a a graded order. Is it bad to depart from the literature and turn the order around?

theorem Finpartition.ext {α : Type u_1} : ∀ {inst : Lattice α} {inst_1 : OrderBot α} {a : α} (x y : Finpartition a), x.parts = y.parts → x = y

theorem Finpartition.ext_iff {α : Type u_1} : ∀ {inst : Lattice α} {inst_1 : OrderBot α} {a : α} (x y : Finpartition a), x = y ↔ x.parts = y.parts

structure Finpartition {α : Type u_1} [Lattice α] [OrderBot α] (a : α) : Type u_1

A finite partition of a : α is a pairwise disjoint finite set of elements whose supremum is a. We forbid ⊥ as a part.

• parts : Finset α

  The elements of the finite partition of a

• supIndep : Finset.SupIndep self.parts id

  The partition is supremum-independent

• sup_parts : Finset.sup self.parts id = a

  The supremum of the partition is a

• not_bot_mem : ⊥ ∉ self.parts

  No element of the partition is bottom

instance instDecidableEqFinpartition : {α : Type u_2} → {inst : Lattice α} → {inst_1 : OrderBot α} → {a : α} → [inst_2 : DecidableEq α] → DecidableEq (Finpartition a)

Equations

• instDecidableEqFinpartition = decEqFinpartition✝

@[simp]

theorem Finpartition.ofErase_parts {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : Finset.SupIndep parts id) (sup_parts : Finset.sup parts id = a) : (Finpartition.ofErase parts sup_indep sup_parts).parts = Finset.erase parts ⊥

def Finpartition.ofErase {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : Finset.SupIndep parts id) (sup_parts : Finset.sup parts id = a) : Finpartition a

A Finpartition constructor which does not insist on ⊥ not being a part.

Equations

• Finpartition.ofErase parts sup_indep sup_parts = { parts := Finset.erase parts ⊥, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

@[simp]

theorem Finpartition.ofSubset_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts) (sup_parts : Finset.sup parts id = b) : (Finpartition.ofSubset P subset sup_parts).parts = parts

def Finpartition.ofSubset {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) {parts : Finset α} (subset : parts ⊆ P.parts) (sup_parts : Finset.sup parts id = b) : Finpartition b

A Finpartition constructor from a bigger existing finpartition.

Equations

• Finpartition.ofSubset P subset sup_parts = { parts := parts, supIndep := ⋯, sup_parts := sup_parts, not_bot_mem := ⋯ }

@[simp]

theorem Finpartition.copy_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) (h : a = b) : (Finpartition.copy P h).parts = P.parts

def Finpartition.copy {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {b : α} (P : Finpartition a) (h : a = b) : Finpartition b

Changes the type of a finpartition to an equal one.

Equations

• Finpartition.copy P h = { parts := P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

def Finpartition.map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} (e : α ≃o β) (P : Finpartition a) : Finpartition (e a)

Transfer a finpartition over an order isomorphism.

Equations

• Finpartition.map e P = { parts := Finset.map (Equiv.toEmbedding ↑e) P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

@[simp]

theorem Finpartition.parts_map {α : Type u_1} [Lattice α] [OrderBot α] {β : Type u_2} [Lattice β] [OrderBot β] {a : α} {e : α ≃o β} {P : Finpartition a} : (Finpartition.map e P).parts = Finset.map (Equiv.toEmbedding ↑e) P.parts

@[simp]

theorem Finpartition.empty_parts (α : Type u_1) [Lattice α] [OrderBot α] : (Finpartition.empty α).parts = ∅

def Finpartition.empty (α : Type u_1) [Lattice α] [OrderBot α] : Finpartition ⊥

The empty finpartition.

Equations

• Finpartition.empty α = { parts := ∅, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

instance Finpartition.instInhabitedFinpartitionBotToBotToLEToPreorderToPartialOrderToSemilatticeInf (α : Type u_1) [Lattice α] [OrderBot α] : Inhabited (Finpartition ⊥)

Equations

• Finpartition.instInhabitedFinpartitionBotToBotToLEToPreorderToPartialOrderToSemilatticeInf α = { default := Finpartition.empty α }

@[simp]

theorem Finpartition.default_eq_empty (α : Type u_1) [Lattice α] [OrderBot α] : default = Finpartition.empty α

@[simp]

theorem Finpartition.indiscrete_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ≠ ⊥) : (Finpartition.indiscrete ha).parts = {a}

def Finpartition.indiscrete {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (ha : a ≠ ⊥) : Finpartition a

The finpartition in one part, aka indiscrete finpartition.

Equations

• Finpartition.indiscrete ha = { parts := {a}, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

theorem Finpartition.le {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b ∈ P.parts) : b ≤ a

theorem Finpartition.ne_bot {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) {b : α} (hb : b ∈ P.parts) : b ≠ ⊥

theorem Finpartition.disjoint {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) : Set.PairwiseDisjoint (↑P.parts) id

theorem Finpartition.parts_eq_empty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} : P.parts = ∅ ↔ a = ⊥

theorem Finpartition.parts_nonempty_iff {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} : P.parts.Nonempty ↔ a ≠ ⊥

theorem Finpartition.parts_nonempty {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (P : Finpartition a) (ha : a ≠ ⊥) : P.parts.Nonempty

instance Finpartition.instUniqueFinpartitionBotToBotToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [Lattice α] [OrderBot α] : Unique (Finpartition ⊥)

Equations

• Finpartition.instUniqueFinpartitionBotToBotToLEToPreorderToPartialOrderToSemilatticeInf = let __src := inferInstance; { toInhabited := __src, uniq := ⋯ }

@[reducible]

def IsAtom.uniqueFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} {P : Finpartition a} (ha : IsAtom a) : Unique (Finpartition a)

There's a unique partition of an atom.

Equations

• IsAtom.uniqueFinpartition ha = { toInhabited := { default := Finpartition.indiscrete ⋯ }, uniq := ⋯ }

instance Finpartition.instFintypeFinpartition {α : Type u_1} [Lattice α] [OrderBot α] [Fintype α] [DecidableEq α] (a : α) : Fintype (Finpartition a)

Equations

• One or more equations did not get rendered due to their size.

Refinement order

instance Finpartition.instLEFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} : LE (Finpartition a)

We say that P ≤ Q if P refines Q: each part of P is less than some part of Q.

Equations

• Finpartition.instLEFinpartition = { le := fun (P Q : Finpartition a) => ∀ ⦃b : α⦄, b ∈ P.parts → ∃ c ∈ Q.parts, b ≤ c }

instance Finpartition.instPartialOrderFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} : PartialOrder (Finpartition a)

Equations

• Finpartition.instPartialOrderFinpartition = let __src := inferInstance; PartialOrder.mk ⋯

instance Finpartition.instOrderTopFinpartitionInstLEFinpartition {α : Type u_1} [Lattice α] [OrderBot α] {a : α} [Decidable (a = ⊥)] : OrderTop (Finpartition a)

Equations

• Finpartition.instOrderTopFinpartitionInstLEFinpartition = OrderTop.mk ⋯

theorem Finpartition.parts_top_subset {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = ⊥)] : ⊤.parts ⊆ {a}

theorem Finpartition.parts_top_subsingleton {α : Type u_1} [Lattice α] [OrderBot α] (a : α) [Decidable (a = ⊥)] : Set.Subsingleton ↑⊤.parts

instance Finpartition.instInfFinpartitionToLattice {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} : Inf (Finpartition a)

Equations

• Finpartition.instInfFinpartitionToLattice = { inf := fun (P Q : Finpartition a) => Finpartition.ofErase (Finset.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) ⋯ ⋯ }

@[simp]

theorem Finpartition.parts_inf {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : Finpartition a) : (P ⊓ Q).parts = Finset.erase (Finset.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)) ⊥

instance Finpartition.instSemilatticeInfFinpartitionToLattice {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} : SemilatticeInf (Finpartition a)

Equations

• Finpartition.instSemilatticeInfFinpartitionToLattice = let __src := inferInstance; let __src_1 := inferInstance; SemilatticeInf.mk ⋯ ⋯ ⋯

theorem Finpartition.exists_le_of_le {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {P : Finpartition a} {Q : Finpartition a} (h : P ≤ Q) (hb : b ∈ Q.parts) : ∃ c ∈ P.parts, c ≤ b

theorem Finpartition.card_mono {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {P : Finpartition a} {Q : Finpartition a} (h : P ≤ Q) : Q.parts.card ≤ P.parts.card

@[simp]

theorem Finpartition.bind_parts {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i ∈ P.parts → Finpartition i) : (Finpartition.bind P Q).parts = Finset.biUnion (Finset.attach P.parts) fun (i : { x : α // x ∈ P.parts }) => (Q ↑i ⋯).parts

def Finpartition.bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (Q : (i : α) → i ∈ P.parts → Finpartition i) : Finpartition a

Given a finpartition P of a and finpartitions of each part of P, this yields the finpartition of a obtained by juxtaposing all the subpartitions.

Equations

• Finpartition.bind P Q = { parts := Finset.biUnion (Finset.attach P.parts) fun (i : { x : α // x ∈ P.parts }) => (Q ↑i ⋯).parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

theorem Finpartition.mem_bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {P : Finpartition a} {Q : (i : α) → i ∈ P.parts → Finpartition i} : b ∈ (Finpartition.bind P Q).parts ↔ ∃ (A : α) (hA : A ∈ P.parts), b ∈ (Q A hA).parts

theorem Finpartition.card_bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {P : Finpartition a} (Q : (i : α) → i ∈ P.parts → Finpartition i) : (Finpartition.bind P Q).parts.card = Finset.sum (Finset.attach P.parts) fun (A : { x : α // x ∈ P.parts }) => (Q ↑A ⋯).parts.card

@[simp]

theorem Finpartition.extend_parts {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c) : (Finpartition.extend P hb hab hc).parts = insert b P.parts

def Finpartition.extend {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c) : Finpartition c

Adds b to a finpartition of a to make a finpartition of a ⊔ b.

Equations

• Finpartition.extend P hb hab hc = { parts := insert b P.parts, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

theorem Finpartition.card_extend {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) (c : α) {hb : b ≠ ⊥} {hab : Disjoint a b} {hc : a ⊔ b = c} : (Finpartition.extend P hb hab hc).parts.card = P.parts.card + 1

@[simp]

theorem Finpartition.avoid_parts_val {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) : (Finpartition.avoid P b).parts.val = Multiset.erase (Multiset.dedup (Multiset.map (fun (x : α) => x \ b) P.parts.val)) ⊥

def Finpartition.avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} (P : Finpartition a) (b : α) : Finpartition (a \ b)

Restricts a finpartition to avoid a given element.

Equations

• Finpartition.avoid P b = Finpartition.ofErase (Finset.image (fun (x : α) => x \ b) P.parts) ⋯ ⋯

@[simp]

theorem Finpartition.mem_avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) : c ∈ (Finpartition.avoid P b).parts ↔ ∃ d ∈ P.parts, ¬d ≤ b ∧ d \ b = c

Finite partitions of finsets

theorem Finpartition.nonempty_of_mem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α} (ha : a ∈ P.parts) : a.Nonempty

theorem Finpartition.eq_of_mem_parts {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {u : Finset α} (P : Finpartition s) {a : α} (ht : t ∈ P.parts) (hu : u ∈ P.parts) (hat : a ∈ t) (hau : a ∈ u) : t = u

theorem Finpartition.exists_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : ∃ t ∈ P.parts, a ∈ t

theorem Finpartition.biUnion_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Finset.biUnion P.parts id = s

theorem Finpartition.existsUnique_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : ∃! (t : Finset α), t ∈ P.parts ∧ a ∈ t

def Finpartition.part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) (a : α) : Finset α

The part of the finpartition that a lies in.

Equations

• Finpartition.part P a = if ha : a ∈ s then Finset.choose (fun (a_1 : Finset α) => a ∈ a_1) P.parts ⋯ else ∅

theorem Finpartition.part_mem {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : Finpartition.part P a ∈ P.parts

theorem Finpartition.mem_part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} (ha : a ∈ s) : a ∈ Finpartition.part P a

theorem Finpartition.part_surjOn {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : Set.SurjOn (Finpartition.part P) ↑s ↑P.parts

theorem Finpartition.exists_subset_part_bijOn {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∃ r ⊆ s, Set.BijOn (Finpartition.part P) ↑r ↑P.parts

theorem Finpartition.sum_card_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : (Finset.sum P.parts fun (i : Finset α) => i.card) = s.card

instance Finpartition.instBotFinpartitionFinsetInstLatticeFinsetInstOrderBotFinsetToLEToPreorderPartialOrder {α : Type u_1} [DecidableEq α] (s : Finset α) : Bot (Finpartition s)

⊥ is the partition in singletons, aka discrete partition.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finpartition.parts_bot {α : Type u_1} [DecidableEq α] (s : Finset α) : ⊥.parts = Finset.map { toFun := singleton, inj' := ⋯ } s

theorem Finpartition.card_bot {α : Type u_1} [DecidableEq α] (s : Finset α) : ⊥.parts.card = s.card

theorem Finpartition.mem_bot_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} : t ∈ ⊥.parts ↔ ∃ a ∈ s, {a} = t

instance Finpartition.instOrderBotFinpartitionFinsetInstLatticeFinsetInstOrderBotFinsetToLEToPreorderPartialOrderInstLEFinpartition {α : Type u_1} [DecidableEq α] (s : Finset α) : OrderBot (Finpartition s)

Equations

• Finpartition.instOrderBotFinpartitionFinsetInstLatticeFinsetInstOrderBotFinsetToLEToPreorderPartialOrderInstLEFinpartition s = let __src := inferInstance; OrderBot.mk ⋯

theorem Finpartition.card_parts_le_card {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : P.parts.card ≤ s.card

def Finpartition.ofSetoid {α : Type u_1} [DecidableEq α] [Fintype α] (s : Setoid α) [DecidableRel Setoid.r] : Finpartition Finset.univ

A setoid over a finite type induces a finpartition of the type's elements, where the parts are the setoid's equivalence classes.

Equations

• Finpartition.ofSetoid s = { parts := Finset.image (fun (a : α) => Finset.filter (Setoid.r a) Finset.univ) Finset.univ, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

theorem Finpartition.mem_part_ofSetoid_iff_rel {α : Type u_1} [DecidableEq α] {a : α} [Fintype α] {s : Setoid α} [DecidableRel Setoid.r] {b : α} : b ∈ Finpartition.part (Finpartition.ofSetoid s) a ↔ Setoid.r a b

def Finpartition.atomise {α : Type u_1} [DecidableEq α] [Fintype α] (s : Finset α) (F : Finset (Finset α)) : Finpartition s

Cuts s along the finsets in F: Two elements of s will be in the same part if they are in the same finsets of F.

Equations

• Finpartition.atomise s F = Finpartition.ofErase (Finset.image (fun (Q : Finset (Finset α)) => Finset.filter (fun (i : α) => ∀ t ∈ F, t ∈ Q ↔ i ∈ t) s) (Finset.powerset F)) ⋯ ⋯

theorem Finpartition.mem_atomise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} : t ∈ (Finpartition.atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, Finset.filter (fun (i : α) => ∀ u ∈ F, u ∈ Q ↔ i ∈ u) s = t

theorem Finpartition.atomise_empty {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] (hs : s.Nonempty) : (Finpartition.atomise s ∅).parts = {s}

theorem Finpartition.card_atomise_le {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] {F : Finset (Finset α)} : (Finpartition.atomise s F).parts.card ≤ 2 ^ F.card

theorem Finpartition.biUnion_filter_atomise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} (ht : t ∈ F) (hts : t ⊆ s) : Finset.biUnion (Finset.filter (fun (u : Finset α) => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts) id = t

theorem Finpartition.card_filter_atomise_le_two_pow {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} [Fintype α] {F : Finset (Finset α)} (ht : t ∈ F) : (Finset.filter (fun (u : Finset α) => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts).card ≤ 2 ^ (F.card - 1)