From d3f5adb0e2c5010a5f36101b2822cdf992fa1b1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 11 Jul 2022 16:51:18 +0000 Subject: [PATCH] feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222) Define the equitabilisation of a partition and a way to find an arbitrary equipartition of any size. Co-authored-by: Bhavik Mehta --- .../simple_graph/regularity/equitabilise.lean | 193 ++++++++++++++++++ src/order/partition/finpartition.lean | 17 +- 2 files changed, 204 insertions(+), 6 deletions(-) create mode 100644 src/combinatorics/simple_graph/regularity/equitabilise.lean diff --git a/src/combinatorics/simple_graph/regularity/equitabilise.lean b/src/combinatorics/simple_graph/regularity/equitabilise.lean new file mode 100644 index 0000000000000..008d1b1777392 --- /dev/null +++ b/src/combinatorics/simple_graph/regularity/equitabilise.lean @@ -0,0 +1,193 @@ +/- +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 order.partition.equipartition + +/-! +# Equitabilising a partition + +This file allows to blow partitions up into parts of controlled size. Given a partition `P` and +`a b m : ℕ`, we want to find a partition `Q` with `a` parts of size `m` and `b` parts of size +`m + 1` such that all parts of `P` are "as close as possible" to unions of parts of `Q`. By +"as close as possible", we mean that each part of `P` can be written as the union of some parts of +`Q` along with at most `m` other elements. + +## Main declarations + +* `finpartition.equitabilise`: `P.equitabilise h` where `h : a * m + b * (m + 1)` is a partition + with `a` parts of size `m` and `b` parts of size `m + 1` which almost refines `P`. +* `finpartition.exists_equipartition_card_eq`: We can find equipartitions of arbitrary size. +-/ + +open finset nat + +namespace finpartition +variables {α : Type*} [decidable_eq α] {s t : finset α} {m n a b : ℕ} {P : finpartition s} + +/-- Given a partition `P` of `s`, as well as a proof that `a * m + b * (m + 1) = s.card`, we can +find a new partition `Q` of `s` where each part has size `m` or `m + 1`, every part of `P` is the +union of parts of `Q` plus at most `m` extra elements, there are `b` parts of size `m + 1` and +(provided `m > 0`, because a partition does not have parts of size `0`) there are `a` parts of size +`m` and hence `a + b` parts in total. -/ +lemma equitabilise_aux (P : finpartition s) (hs : a * m + b * (m + 1) = s.card) : + ∃ Q : finpartition s, + (∀ x : finset α, x ∈ Q.parts → x.card = m ∨ x.card = m + 1) ∧ + (∀ x, x ∈ P.parts → (x \ (Q.parts.filter $ λ y, y ⊆ x).bUnion id).card ≤ m) ∧ + (Q.parts.filter $ λ i, card i = m + 1).card = b := +begin + -- Get rid of the easy case `m = 0` + obtain rfl | m_pos := m.eq_zero_or_pos, + { refine ⟨⊥, by simp, _, by simpa using hs.symm⟩, + simp only [le_zero_iff, card_eq_zero, mem_bUnion, exists_prop, mem_filter, id.def, and_assoc, + sdiff_eq_empty_iff_subset, subset_iff], + exact λ x hx a ha, ⟨{a}, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, + mem_singleton_self _⟩ }, + -- Prove the case `m > 0` by strong induction on `s` + induction s using finset.strong_induction with s ih generalizing P a b, + -- If `a = b = 0`, then `s = ∅` and we can partition into zero parts + by_cases hab : a = 0 ∧ b = 0, + { simp only [hab.1, hab.2, add_zero, zero_mul, eq_comm, card_eq_zero] at hs, + subst hs, + exact ⟨finpartition.empty _, by simp, by simp [unique.eq_default P], by simp [hab.2]⟩ }, + simp_rw [not_and_distrib, ←ne.def, ←pos_iff_ne_zero] at hab, + -- `n` will be the size of the smallest part + set n := if 0 < a then m else m + 1 with hn, + -- Some easy facts about it + obtain ⟨hn₀, hn₁, hn₂, hn₃⟩ : 0 < n ∧ n ≤ m + 1 ∧ n ≤ a * m + b * (m + 1) ∧ + ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = s.card - n, + { rw [hn, ←hs], + split_ifs; rw [tsub_mul, one_mul], + { refine ⟨m_pos, le_succ _, le_add_right (le_mul_of_pos_left ‹0 < a›), _⟩, + rw tsub_add_eq_add_tsub (le_mul_of_pos_left h), }, + { refine ⟨succ_pos', le_rfl, le_add_left (le_mul_of_pos_left $ hab.resolve_left ‹¬0 < a›), _⟩, + rw ←add_tsub_assoc_of_le (le_mul_of_pos_left $ hab.resolve_left ‹¬0 < a›) } }, + /- We will call the inductive hypothesis on a partition of `s \ t` for a carefully chosen `t ⊆ s`. + To decide which, however, we must distinguish the case where all parts of `P` have size `m` (in + which case we take `t` to be an arbitrary subset of `s` of size `n`) from the case where at least + one part `u` of `P` has size `m + 1` (in which case we take `t` to be an arbitrary subset of `u` + of size `n`). The rest of each branch is just tedious calculations to satisfy the induction + hypothesis. -/ + by_cases ∀ u ∈ P.parts, card u < m + 1, + { obtain ⟨t, hts, htn⟩ := exists_smaller_set s n (hn₂.trans_eq hs), + have ht : t.nonempty := by rwa [←card_pos, htn], + have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card, + { rw [card_sdiff ‹t ⊆ s›, htn, hn₃] }, + obtain ⟨R, hR₁, hR₂, hR₃⟩ := @ih (s \ t) (sdiff_ssubset hts ‹t.nonempty›) (P.avoid t) + (if 0 < a then a-1 else a) (if 0 < a then b else b-1) hcard, + refine ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel hts), _, _, _⟩, + { simp only [extend_parts, mem_insert, forall_eq_or_imp, and_iff_left hR₁, htn, hn], + exact ite_eq_or_eq _ _ _ }, + { exact λ x hx, (card_le_of_subset $ sdiff_subset _ _).trans (lt_succ_iff.1 $ h _ hx) }, + simp_rw [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff], + split_ifs with ha, + { rw [hR₃, if_pos ha] }, + rw [card_insert_of_not_mem (λ H, _), hR₃, if_neg ha, tsub_add_cancel_of_le], + { exact hab.resolve_left ha }, + { exact ht.ne_empty (le_sdiff_iff.1 $ R.le $ filter_subset _ _ H) } }, + push_neg at h, + obtain ⟨u, hu₁, hu₂⟩ := h, + obtain ⟨t, htu, htn⟩ := exists_smaller_set _ _ (hn₁.trans hu₂), + have ht : t.nonempty := by rwa [←card_pos, htn], + have hcard : ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = (s \ t).card, + { rw [card_sdiff (htu.trans $ P.le hu₁), htn, hn₃] }, + obtain ⟨R, hR₁, hR₂, hR₃⟩ := @ih (s \ t) (sdiff_ssubset (htu.trans $ P.le hu₁) ht) (P.avoid t) + (if 0 < a then a-1 else a) (if 0 < a then b else b-1) hcard, + refine ⟨R.extend ht.ne_empty sdiff_disjoint (sdiff_sup_cancel $ htu.trans $ P.le hu₁), _, _, _⟩, + { simp only [mem_insert, forall_eq_or_imp, extend_parts, and_iff_left hR₁, htn, hn], + exact ite_eq_or_eq _ _ _ }, + { conv in (_ ∈ _) {rw ←insert_erase hu₁}, + simp only [and_imp, mem_insert, forall_eq_or_imp, ne.def, extend_parts], + refine ⟨_, λ x hx, (card_le_of_subset _).trans $ hR₂ x _⟩, + { simp only [filter_insert, if_pos htu, bUnion_insert, mem_erase, id.def], + obtain rfl | hut := eq_or_ne u t, + { rw sdiff_eq_empty_iff_subset.2 (subset_union_left _ _), + exact bot_le }, + refine (card_le_of_subset $ λ i, _).trans (hR₂ (u \ t) $ + P.mem_avoid.2 ⟨u, hu₁, λ i, hut $ i.antisymm htu, rfl⟩), + simp only [not_exists, mem_bUnion, and_imp, mem_union, mem_filter, mem_sdiff, id.def, + not_or_distrib], + exact λ hi₁ hi₂ hi₃, ⟨⟨hi₁, hi₂⟩, λ x hx hx', hi₃ _ hx $ hx'.trans $ sdiff_subset _ _⟩ }, + { apply sdiff_subset_sdiff subset.rfl (bUnion_subset_bUnion_of_subset_left _ _), + exact filter_subset_filter _ (subset_insert _ _) }, + simp only [avoid, of_erase, mem_erase, mem_image, bot_eq_empty], + exact ⟨(nonempty_of_mem_parts _ $ mem_of_mem_erase hx).ne_empty, _, mem_of_mem_erase hx, + (disjoint_of_subset_right htu $ P.disjoint (mem_of_mem_erase hx) hu₁ $ + ne_of_mem_erase hx).sdiff_eq_left⟩ }, + simp only [extend_parts, filter_insert, htn, hn, m.succ_ne_self.symm.ite_eq_right_iff], + split_ifs, + { rw [hR₃, if_pos h] }, + { rw [card_insert_of_not_mem (λ H, _), hR₃, if_neg h, nat.sub_add_cancel (hab.resolve_left h)], + exact ht.ne_empty (le_sdiff_iff.1 $ R.le $ filter_subset _ _ H) } +end + +variables (P) (h : a * m + b * (m + 1) = s.card) + +/-- Given a partition `P` of `s`, as well as a proof that `a * m + b * (m + 1) = s.card`, build a +new partition `Q` of `s` where each part has size `m` or `m + 1`, every part of `P` is the union of +parts of `Q` plus at most `m` extra elements, there are `b` parts of size `m + 1` and (provided +`m > 0`, because a partition does not have parts of size `0`) there are `a` parts of size `m` and +hence `a + b` parts in total. -/ +noncomputable def equitabilise : finpartition s := (P.equitabilise_aux h).some + +variables {P h} + +lemma card_eq_of_mem_parts_equitabilise : + t ∈ (P.equitabilise h).parts → t.card = m ∨ t.card = m + 1 := +(P.equitabilise_aux h).some_spec.1 _ + +lemma equitabilise_is_equipartition : (P.equitabilise h).is_equipartition := +set.equitable_on_iff_exists_eq_eq_add_one.2 ⟨m, λ u, card_eq_of_mem_parts_equitabilise⟩ + +variables (P h) + +lemma card_filter_equitabilise_big : + ((P.equitabilise h).parts.filter $ λ u : finset α, u.card = m + 1).card = b := +(P.equitabilise_aux h).some_spec.2.2 + +lemma card_filter_equitabilise_small (hm : m ≠ 0) : + ((P.equitabilise h).parts.filter $ λ u : finset α, u.card = m).card = a := +begin + refine (mul_eq_mul_right_iff.1 $ (add_left_inj (b * (m + 1))).1 _).resolve_right hm, + rw [h, ←(P.equitabilise h).sum_card_parts], + have hunion : (P.equitabilise h).parts = (P.equitabilise h).parts.filter (λ u, u.card = m) ∪ + (P.equitabilise h).parts.filter (λ u, u.card = m + 1), + { rw [←filter_or, filter_true_of_mem], + exact λ x, card_eq_of_mem_parts_equitabilise }, + nth_rewrite 1 hunion, + rw [sum_union, sum_const_nat (λ x hx, (mem_filter.1 hx).2), + sum_const_nat (λ x hx, (mem_filter.1 hx).2), P.card_filter_equitabilise_big], + refine λ x hx, succ_ne_self m _, + rw [inf_eq_inter, mem_inter, mem_filter, mem_filter] at hx, + rw [succ_eq_add_one, ←hx.2.2, hx.1.2], +end + +lemma card_parts_equitabilise (hm : m ≠ 0) : (P.equitabilise h).parts.card = a + b := +begin + rw [←filter_true_of_mem (λ x, card_eq_of_mem_parts_equitabilise), filter_or, card_union_eq, + P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big], + exact disjoint_filter.2 (λ x _ h₀ h₁, nat.succ_ne_self m $ h₁.symm.trans h₀), + apply_instance +end + +lemma card_parts_equitabilise_subset_le : + t ∈ P.parts → (t \ ((P.equitabilise h).parts.filter $ λ u, u ⊆ t).bUnion id).card ≤ m := +(classical.some_spec $ P.equitabilise_aux h).2.1 t + +variables (s) + +/-- We can find equipartitions of arbitrary size. -/ +lemma exists_equipartition_card_eq (hn : n ≠ 0) (hs : n ≤ s.card) : + ∃ P : finpartition s, P.is_equipartition ∧ P.parts.card = n := +begin + rw ←pos_iff_ne_zero at hn, + have : (n - s.card % n) * (s.card / n) + (s.card % n) * (s.card / n + 1) = s.card, + { rw [tsub_mul, mul_add, ←add_assoc, tsub_add_cancel_of_le + (nat.mul_le_mul_right _ (mod_lt _ hn).le), mul_one, add_comm, mod_add_div] }, + refine ⟨(indiscrete (card_pos.1 $ hn.trans_le hs).ne_empty).equitabilise this, + equitabilise_is_equipartition, _⟩, + rw [card_parts_equitabilise _ _ (nat.div_pos hs hn).ne', tsub_add_cancel_of_le (mod_lt _ hn).le], +end + +end finpartition diff --git a/src/order/partition/finpartition.lean b/src/order/partition/finpartition.lean index 4446611792a9f..4b3eaa69b38d1 100644 --- a/src/order/partition/finpartition.lean +++ b/src/order/partition/finpartition.lean @@ -372,18 +372,23 @@ card_insert_of_not_mem $ λ h, hb $ hab.symm.eq_bot_of_le $ P.le h end distrib_lattice section generalized_boolean_algebra -variables [generalized_boolean_algebra α] [decidable_eq α] {a : α} (P : finpartition a) +variables [generalized_boolean_algebra α] [decidable_eq α] {a b c : α} (P : finpartition a) /-- Restricts a finpartition to avoid a given element. -/ @[simps] def avoid (b : α) : finpartition (a \ b) := of_erase (P.parts.image (\ b)) (P.disjoint.image_finset_of_le $ λ a, sdiff_le).sup_indep - (begin - rw [sup_image, comp.left_id, finset.sup_sdiff_right], - congr, - exact P.sup_parts, - end) + (by rw [sup_image, comp.left_id, finset.sup_sdiff_right, ←id_def, P.sup_parts]) + +@[simp] lemma mem_avoid : c ∈ (P.avoid b).parts ↔ ∃ d ∈ P.parts, ¬ d ≤ b ∧ d \ b = c := +begin + simp only [avoid, of_erase_parts, mem_erase, ne.def, mem_image, exists_prop, + ←exists_and_distrib_left, @and.left_comm (c ≠ ⊥)], + refine exists_congr (λ d, and_congr_right' $ and_congr_left _), + rintro rfl, + rw sdiff_eq_bot_iff, +end end generalized_boolean_algebra end finpartition