feat: port Order.Partition.Equipartition (#2058)

Co-authored-by: Moritz Firsching <firsching@google.com>

Mathlib.lean

@@ -832,6 +832,7 @@ import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous
 import Mathlib.Order.OrderIsoNat
 import Mathlib.Order.PartialSups
+import Mathlib.Order.Partition.Equipartition
 import Mathlib.Order.Partition.Finpartition
 import Mathlib.Order.PropInstances
 import Mathlib.Order.RelClasses

Mathlib/Order/Partition/Equipartition.lean

@@ -0,0 +1,90 @@
+/-
+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
+
+! This file was ported from Lean 3 source module order.partition.equipartition
+! leanprover-community/mathlib commit b363547b3113d350d053abdf2884e9850a56b205
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.Set.Equitable
+import Mathlib.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.IsEquipartition`: Predicate for a `Finpartition` to be an equipartition.
+-/
+
+
+open Finset Fintype
+
+namespace Finpartition
+
+variable {α : Type _} [DecidableEq α] {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 IsEquipartition : Prop :=
+  (P.parts : Set (Finset α)).EquitableOn card
+#align finpartition.is_equipartition Finpartition.IsEquipartition
+
+theorem isEquipartition_iff_card_parts_eq_average :
+    P.IsEquipartition ↔
+      ∀ a : Finset α,
+        a ∈ P.parts → a.card = s.card / P.parts.card ∨ a.card = s.card / P.parts.card + 1 :=
+  by simp_rw [IsEquipartition, Finset.equitableOn_iff, P.sum_card_parts]
+#align finpartition.is_equipartition_iff_card_parts_eq_average
+    Finpartition.isEquipartition_iff_card_parts_eq_average
+
+variable {P}
+
+theorem Set.Subsingleton.isEquipartition (h : (P.parts : Set (Finset α)).Subsingleton) :
+    P.IsEquipartition :=
+  Set.Subsingleton.equitableOn h _
+#align finpartition.set.subsingleton.is_equipartition Finpartition.Set.Subsingleton.isEquipartition
+
+theorem IsEquipartition.card_parts_eq_average (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
+    t.card = s.card / P.parts.card ∨ t.card = s.card / P.parts.card + 1 :=
+  P.isEquipartition_iff_card_parts_eq_average.1 hP _ ht
+#align finpartition.is_equipartition.card_parts_eq_average
+    Finpartition.IsEquipartition.card_parts_eq_average
+
+theorem IsEquipartition.average_le_card_part (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
+    s.card / P.parts.card ≤ t.card := by
+  rw [← P.sum_card_parts]
+  exact Finset.EquitableOn.le hP ht
+#align finpartition.is_equipartition.average_le_card_part
+    Finpartition.IsEquipartition.average_le_card_part
+
+theorem IsEquipartition.card_part_le_average_add_one (hP : P.IsEquipartition) (ht : t ∈ P.parts) :
+    t.card ≤ s.card / P.parts.card + 1 := by
+  rw [← P.sum_card_parts]
+  exact Finset.EquitableOn.le_add_one hP ht
+#align finpartition.is_equipartition.card_part_le_average_add_one
+    Finpartition.IsEquipartition.card_part_le_average_add_one
+
+/-! ### Discrete and indiscrete finpartition -/
+
+
+variable (s) -- [Decidable (a = ⊥)]
+
+theorem bot_isEquipartition : (⊥ : Finpartition s).IsEquipartition :=
+  Set.equitableOn_iff_exists_eq_eq_add_one.2 ⟨1, by simp⟩
+#align finpartition.bot_is_equipartition Finpartition.bot_isEquipartition
+
+theorem top_isEquipartition [Decidable (s = ⊥)] : (⊤ : Finpartition s).IsEquipartition :=
+  Set.Subsingleton.isEquipartition (parts_top_subsingleton _)
+#align finpartition.top_is_equipartition Finpartition.top_isEquipartition
+
+theorem indiscrete_isEquipartition {hs : s ≠ ∅} : (indiscrete hs).IsEquipartition := by
+  rw [IsEquipartition, indiscrete_parts, coe_singleton]
+  exact Set.equitableOn_singleton s _
+#align finpartition.indiscrete_is_equipartition Finpartition.indiscrete_isEquipartition
+
+end Finpartition