feat(order/partition/equipartition): Equipartitions (#12023)

Define `finpartition.is_equipartition`, a predicate for saying that the parts of a `finpartition` of a `finset` are all the same size up to a difference of `1`.

Co-authored-by: Bhavik Mehta <bhavik.mehta8@gmail.com>

src/data/set/basic.lean

@@ -1597,6 +1597,9 @@ ext $ λ y, ⟨λ hy, (hs hx hy) ▸ mem_singleton _, λ hy, (eq_of_mem_singleto
 @[simp] lemma subsingleton_singleton {a} : ({a} : set α).subsingleton :=
 λ x hx y hy, (eq_of_mem_singleton hx).symm ▸ (eq_of_mem_singleton hy).symm ▸ rfl
 
+lemma subsingleton_of_subset_singleton (h : s ⊆ {a}) : s.subsingleton :=
+subsingleton_singleton.mono h
+
 lemma subsingleton_of_forall_eq (a : α) (h : ∀ b ∈ s, b = a) : s.subsingleton :=
 λ b hb c hc, (h _ hb).trans (h _ hc).symm
 

src/data/set/equitable.lean

@@ -73,8 +73,9 @@ end set
 open set
 
 namespace finset
+variables {s : finset α} {f : α → ℕ} {a : α}
 
-lemma equitable_on_iff_le_le_add_one {s : finset α} {f : α → ℕ} :
+lemma equitable_on_iff_le_le_add_one :
   equitable_on (s : set α) f ↔
     ∀ a ∈ s, (∑ i in s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i in s, f i) / s.card + 1 :=
 begin
@@ -97,7 +98,15 @@ begin
   exact λ _ _, rfl,
 end
 
-lemma equitable_on_iff {s : finset α} {f : α → ℕ} :
+lemma equitable_on.le (h : equitable_on (s : set α) f) (ha : a ∈ s) :
+  (∑ i in s, f i) / s.card ≤ f a :=
+(equitable_on_iff_le_le_add_one.1 h a ha).1
+
+lemma equitable_on.le_add_one (h : equitable_on (s : set α) f) (ha : a ∈ s) :
+  f a ≤ (∑ i in s, f i) / s.card + 1 :=
+(equitable_on_iff_le_le_add_one.1 h a ha).2
+
+lemma equitable_on_iff :
   equitable_on (s : set α) f ↔
     ∀ a ∈ s, f a = (∑ i in s, f i) / s.card ∨ f a = (∑ i in s, f i) / s.card + 1 :=
 by simp_rw [equitable_on_iff_le_le_add_one, nat.le_and_le_add_one_iff]

src/order/partition/equipartition.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Bhavik Mehta
+-/
+import data.set.equitable
+import order.partition.finpartition
+
+/-!
+# Finite equipartitions
+
+This file defines finite equipartitions, the partitions whose parts all are the same size up to a
+difference of `1`.
+
+## Main declarations
+
+* `finpartition.is_equipartition`: Predicate for a `finpartition` to be an equipartition.
+-/
+
+open finset fintype
+
+namespace finpartition
+variables {α : Type*} [decidable_eq α] {s t : finset α} (P : finpartition s)
+
+/-- An equipartition is a partition whose parts are all the same size, up to a difference of `1`. -/
+def is_equipartition : Prop := (P.parts : set (finset α)).equitable_on card
+
+lemma is_equipartition_iff_card_parts_eq_average : P.is_equipartition ↔
+  ∀ a : finset α, a ∈ P.parts → a.card = s.card/P.parts.card ∨ a.card = s.card/P.parts.card + 1 :=
+by simp_rw [is_equipartition, finset.equitable_on_iff, P.sum_card_parts]
+
+variables {P}
+
+lemma _root_.set.subsingleton.is_equipartition (h : (P.parts : set (finset α)).subsingleton) :
+  P.is_equipartition :=
+h.equitable_on _
+
+lemma is_equipartition.average_le_card_part (hP : P.is_equipartition) (ht : t ∈ P.parts) :
+  s.card / P.parts.card ≤ t.card :=
+by { rw ←P.sum_card_parts, exact equitable_on.le hP ht }
+
+lemma is_equipartition.card_part_le_average_add_one (hP : P.is_equipartition) (ht : t ∈ P.parts) :
+  t.card ≤ s.card / P.parts.card + 1 :=
+by { rw ←P.sum_card_parts, exact equitable_on.le_add_one hP ht }
+
+/-! ### Discrete and indiscrete finpartition -/
+
+variables (s)
+
+lemma bot_is_equipartition : (⊥ : finpartition s).is_equipartition :=
+set.equitable_on_iff_exists_eq_eq_add_one.2 ⟨1, by simp⟩
+
+lemma top_is_equipartition : (⊤ : finpartition s).is_equipartition :=
+(parts_top_subsingleton _).is_equipartition
+
+lemma indiscrete_is_equipartition {hs : s ≠ ∅} : (indiscrete hs).is_equipartition :=
+by { rw [is_equipartition, indiscrete_parts, coe_singleton], exact set.equitable_on_singleton s _ }
+
+end finpartition

src/order/partition/finpartition.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.basic
-import order.locally_finite
 import order.atoms
+import order.locally_finite
 import order.sup_indep
 
 /-!
@@ -14,6 +14,9 @@ import order.sup_indep
 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:
@@ -202,8 +205,21 @@ instance [decidable (a = ⊥)] : order_top (finpartition a) :=
     { exact λ b hb, ⟨a, mem_singleton_self _, P.le hb⟩ }
   end }
 
-end order
+lemma parts_top_subset (a : α) [decidable (a = ⊥)] : (⊤ : finpartition a).parts ⊆ {a} :=
+begin
+  intros b hb,
+  change b ∈ finpartition.parts (dite _ _ _) at hb,
+  split_ifs at hb,
+  { simp only [copy_parts, empty_parts, not_mem_empty] at hb,
+    exact hb.elim },
+  { exact hb }
+end
 
+lemma parts_top_subsingleton (a : α) [decidable (a = ⊥)] :
+  ((⊤ : finpartition a).parts : set α).subsingleton :=
+set.subsingleton_of_subset_singleton $ λ b hb, mem_singleton.1 $ parts_top_subset _ hb
+
+end order
 end lattice
 
 section distrib_lattice