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.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

Link Finpartition and Setoid.isPartition.

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 s.parts id

  The partition is supremum-independent

• supParts : Finset.sup s.parts id = a

  The supremum of the partition is a

• not_bot_mem : ⊥ ∉ s.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

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

@[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 := (_ : Finset.SupIndep parts id), supParts := sup_parts, not_bot_mem := (_ : ⊥ ∈ parts → False) }

@[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 := (_ : Finset.SupIndep P.parts id), supParts := (_ : Finset.sup P.parts id = b), not_bot_mem := (_ : ⊥ ∉ 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 := (_ : Finset.SupIndep ∅ id), supParts := (_ : Finset.sup ∅ id = ⊥), 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 := (_ : Finset.SupIndep {a} id), supParts := (_ : Finset.sup {a} id = id a), not_bot_mem := (_ : ⊥ ∈ {a} → False) }

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} : Finset.Nonempty P.parts ↔ a ≠ ⊥

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

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

Equations

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

@[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 (_ : a ≠ ⊥) }, uniq := (_ : ∀ (P : Finpartition a), P = default) }

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 (_ : ∀ (P Q : Finpartition a), P ≤ Q → Q ≤ P → P = Q)

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

Equations

• Finpartition.instOrderTopFinpartitionInstLEFinpartition = OrderTop.mk (_ : ∀ (P : Finpartition a), P ≤ ⊤)

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

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

@[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

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

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) : Finset.card Q.parts ≤ Finset.card P.parts

@[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 (_ : ↑i ∈ P.parts)).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

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

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) : Finset.card (Finpartition.bind P Q).parts = Finset.sum (Finset.attach P.parts) fun (A : { x : α // x ∈ P.parts }) => Finset.card (Q ↑A (_ : ↑A ∈ P.parts)).parts

@[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

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

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} : Finset.card (Finpartition.extend P hb hab hc).parts = Finset.card P.parts + 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

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

@[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) : Finset.Nonempty a

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.sum_card_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : (Finset.sum P.parts fun (i : Finset α) => Finset.card i) = Finset.card s

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' := (_ : Function.Injective singleton) } s

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

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

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

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

def Finpartition.atomise {α : Type u_1} [DecidableEq α] (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

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

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

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

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

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

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