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?

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 : self.parts.SupIndep id

  The partition is supremum-independent

• sup_parts : self.parts.sup id = a

  The supremum of the partition is a

• not_bot_mem : ⊥ ∉ self.parts

  No element of the partition is bottom

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

theorem Finpartition.supIndep {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) : self.parts.SupIndep id

The partition is supremum-independent

theorem Finpartition.sup_parts {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) : self.parts.sup id = a

The supremum of the partition is a

theorem Finpartition.not_bot_mem {α : Type u_1} [Lattice α] [OrderBot α] {a : α} (self : Finpartition a) : ⊥ ∉ 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✝

def Finpartition.ofErase {α : Type u_1} [Lattice α] [OrderBot α] [DecidableEq α] {a : α} (parts : Finset α) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup 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 := parts.erase ⊥, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ }

@[simp]

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

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

A Finpartition constructor from a bigger existing finpartition.

Equations

• P.ofSubset subset sup_parts = { parts := parts, supIndep := ⋯, sup_parts := 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 : parts.sup id = b) : (P.ofSubset subset sup_parts).parts = 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

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

@[simp]

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

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 (↑e).toEmbedding 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 (↑e).toEmbedding P.parts

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

The empty finpartition.

Equations

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

@[simp]

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

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

Equations

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

@[simp]

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

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 := ⋯ }

@[simp]

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

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) : (↑P.parts).PairwiseDisjoint 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.instUniqueBot {α : Type u_1} [Lattice α] [OrderBot α] : Unique (Finpartition ⊥)

Equations

• Finpartition.instUniqueBot = { toInhabited := inferInstance, uniq := ⋯ }

@[reducible, inline]

abbrev 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

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

instance Finpartition.instFintypeOfDecidableEq {α : 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.instLE {α : 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.instLE = { le := fun (P Q : Finpartition a) => ∀ ⦃b : α⦄, b ∈ P.parts → ∃ c ∈ Q.parts, b ≤ c }

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

Equations

• Finpartition.instPartialOrder = PartialOrder.mk ⋯

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

Equations

• Finpartition.instOrderTopOfDecidableEqBot = 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 = ⊥)] : (↑⊤.parts).Subsingleton

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

Equations

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

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

Equations

• Finpartition.instInf = { 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.image (fun (bc : α × α) => bc.1 ⊓ bc.2) (P.parts ×ˢ Q.parts)).erase ⊥

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

Equations

• Finpartition.instSemilatticeInf = 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

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

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

@[simp]

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

theorem Finpartition.mem_bind {α : Type u_1} [DistribLattice α] [OrderBot α] [DecidableEq α] {a : α} {b : α} {P : Finpartition a} {Q : (i : α) → i ∈ P.parts → Finpartition i} : b ∈ (P.bind 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) : (P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card

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

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

@[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) : (P.extend hb hab hc).parts = insert b P.parts

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

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

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

@[simp]

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

@[simp]

theorem Finpartition.mem_avoid {α : Type u_1} [GeneralizedBooleanAlgebra α] [DecidableEq α] {a : α} {b : α} {c : α} (P : Finpartition a) : c ∈ (P.avoid 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) : P.parts.biUnion 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

• P.part 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) : P.part a ∈ P.parts

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

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

theorem Finpartition.mem_part_iff_part_eq_part {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) {a : α} {b : α} (ha : a ∈ s) (hb : b ∈ s) : a ∈ P.part b ↔ P.part a = P.part b

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

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

def Finpartition.equivSigmaParts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : { x : α // x ∈ s } ≃ (t : { x : Finset α // x ∈ P.parts }) × { x : α // x ∈ ↑t }

Equivalence between a finpartition's parts as a dependent sum and the partitioned set.

Equations

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

theorem Finpartition.exists_enumeration {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∃ (f : { x : α // x ∈ s } ≃ (t : { x : Finset α // x ∈ P.parts }) × Fin (↑t).card), ∀ (a b : { x : α // x ∈ s }), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst

theorem Finpartition.sum_card_parts {α : Type u_1} [DecidableEq α] {s : Finset α} (P : Finpartition s) : ∑ i ∈ P.parts, i.card = s.card

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

⊥ is the partition in singletons, aka discrete partition.

Equations

• Finpartition.instBotFinset s = { bot := { parts := Finset.map { toFun := singleton, inj' := ⋯ } s, supIndep := ⋯, sup_parts := ⋯, not_bot_mem := ⋯ } }

@[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.instOrderBotFinset {α : Type u_1} [DecidableEq α] (s : Finset α) : OrderBot (Finpartition s)

Equations

• Finpartition.instOrderBotFinset s = OrderBot.mk ⋯

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

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

def Finpartition.ofSetoid {α : Type u_1} [DecidableEq α] [Fintype α] (s : Setoid α) [DecidableRel ⇑s] : 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 (fun (b : α) => s a b) 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 ⇑s] {b : α} : b ∈ (Finpartition.ofSetoid s).part a ↔ s a b

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

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

theorem Finpartition.mem_atomise {α : Type u_1} [DecidableEq α] {s : Finset α} {t : Finset α} {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 α} (hs : s.Nonempty) : (Finpartition.atomise s ∅).parts = {s}

theorem Finpartition.card_atomise_le {α : Type u_1} [DecidableEq α] {s : Finset α} {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 α} {F : Finset (Finset α)} (ht : t ∈ F) (hts : t ⊆ s) : (Finset.filter (fun (u : Finset α) => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts).biUnion 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.filter (fun (u : Finset α) => u ⊆ t ∧ u.Nonempty) (Finpartition.atomise s F).parts).card ≤ 2 ^ (F.card - 1)