From baf9a1c0d18b1f8d8831fb3e5027761a61ae2e54 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 16 Oct 2023 17:05:15 +0000 Subject: [PATCH 01/12] refactor: New `Colex` API This fully rewrites `Combinatorics.Colex` to use a type synonym approach instead of abusing defeq. We also provide some API about initial segments of colex. --- Mathlib/Combinatorics/Colex.lean | 659 +++++++++++++++---------------- 1 file changed, 314 insertions(+), 345 deletions(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index c7ad3d9d073c7..e92941b872369 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -3,8 +3,9 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Bhavik Mehta, Alena Gusakov -/ -import Mathlib.Data.Fintype.Basic import Mathlib.Algebra.GeomSum +import Mathlib.Data.Finset.Slice +import Mathlib.Order.SupClosed #align_import combinatorics.colex from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c" @@ -14,410 +15,378 @@ import Mathlib.Algebra.GeomSum We define the colex ordering for finite sets, and give a couple of important lemmas and properties relating to it. -The colex ordering likes to avoid large values - it can be thought of on -`Finset ℕ` as the "binary" ordering. That is, order A based on -`∑_{i ∈ A} 2^i`. +The colex ordering likes to avoid large values - In the special case of `ℕ`, it can be thought of as +the "binary" ordering. That is, order s based on `∑_{i ∈ s} 2^i`. It's defined here in a slightly more general way, requiring only `LT α` in the definition of colex on `Finset α`. In the context of the Kruskal-Katona -theorem, we are interested in particular on how colex behaves for sets of a +lemma, we are interested in particular on how colex behaves for sets of a fixed size. If the size is 3, colex on ℕ starts 123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ... ## Main statements -* `Colex.hom_lt_iff`: strictly monotone functions preserve colex + * Colex order properties - linearity, decidability and so on. -* `forall_lt_of_colex_lt_of_forall_lt`: if A < B in colex, and everything - in B is < t, then everything in A is < t. This confirms the idea that - an enumeration under colex will exhaust all sets using elements < t before - allowing t to be included. -* `sum_two_pow_le_iff_lt`: colex for α = ℕ is the same as binary +* `Finset.Colex.forall_lt_mono`: if `s < t` in colex, and everything in `t` is `< a`, then + everything in `s` is `< a`. This confirms the idea that an enumeration under colex will exhaust + all sets using elements `< a` before allowing `a` to be included. +* `Finse.toColex_image_lt_toColex_image`: Strictly monotone functions preserve colex. +* `Finset.sum_two_pow_le_iff_colex_le`: colex for α = ℕ is the same as binary (this also proves binary expansions are unique) ## See also Related files are: * `Data.List.Lex`: Lexicographic order on lists. -* `Data.Pi.Lex`: Lexicographic order on `(i : α) → α i`. +* `Data.Pi.Lex`: Lexicographic order on `Πₗ i, α i`. * `Data.PSigma.Order`: Lexicographic order on `Σ' i, α i`. * `Data.Sigma.Order`: Lexicographic order on `Σ i, α i`. * `Data.Prod.Lex`: Lexicographic order on `α × β`. -## Tags -colex, colexicographic, binary +## TODO + +* Generalise `Colex.initSeg` so that it applies to `ℕ`. ## References + * https://github.com/b-mehta/maths-notes/blob/master/iii/mich/combinatorics.pdf +## Tags + +colex, colexicographic, binary -/ +open Finset +open scoped BigOperators + +/-- If all the elements of a finset `s` of naturals are less than `n`, then the sum of their powers of `2` is less than `2 ^ k`. -/ +lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : + ∑ k in s, 2 ^ k < 2 ^ n := by + calc + ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk + _ = 2 ^ n - 1 := by + simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] + _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one +#align nat.sum_two_pow_lt Nat.sum_two_pow_lt -variable {α : Type*} +variable {α β : Type*} -open Finset -open BigOperators +namespace Finset -/-- We define this type synonym to refer to the colexicographic ordering on finsets -rather than the natural subset ordering. --/ -def Finset.Colex (α) := - Finset α --- Porting note: `deriving Inhabited` doesn't work -#align finset.colex Finset.Colex +/-- Type synonym of `Finset α` equipped with the colexicographic order rather than the inclusion +order. -/ +def Colex (α) := Finset α instance : Inhabited (Finset.Colex α) := inferInstanceAs (Inhabited (Finset α)) -/-- A convenience constructor to turn a `Finset α` into a `Finset.Colex α`, useful in order to -use the colex ordering rather than the subset ordering. --/ -def Finset.toColex {α} (s : Finset α) : Finset.Colex α := - s -#align finset.to_colex Finset.toColex +/-- `toColex` is the "identity" function between `Finset α` and `Finset.Colex α`. -/ +def toColex : Finset α ≃ Colex α := Equiv.refl _ -@[simp] -theorem Colex.eq_iff (A B : Finset α) : A.toColex = B.toColex ↔ A = B := - Iff.rfl -#align colex.eq_iff Colex.eq_iff +/-- `ofColex` is the "identity" function between `Finset.Colex α` and `Finset α`. -/ +def ofColex : Colex α ≃ Finset α := Equiv.refl _ -/-- `A` is less than `B` in the colex ordering if the largest thing that's not in both sets is in B. -In other words, `max (A ∆ B) ∈ B` (if the maximum exists). --/ -instance Colex.instLT [LT α] : LT (Finset.Colex α) := - ⟨fun A B : Finset α => ∃ k : α, (∀ {x}, k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A ∧ k ∈ B⟩ +@[simp] lemma toColex_symm_eq : (@toColex α).symm = ofColex := rfl +@[simp] lemma ofColex_symm_eq : (@ofColex α).symm = toColex := rfl +@[simp] lemma toColex_ofColex (s : Colex α) : toColex (ofColex s) = s := rfl +@[simp] lemma ofColex_toColex (s : Finset α) : ofColex (toColex s) = s := rfl +-- Tagged `nolint simpNF` because eligible for `dsimp` +@[simp, nolint simpNF] lemma toColex_inj {s t : Finset α} : toColex s = toColex t ↔ s = t := Iff.rfl +@[simp, nolint simpNF] lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t := Iff.rfl +lemma toColex_ne_toColex {s t : Finset α} : toColex s ≠ toColex t ↔ s ≠ t := Iff.rfl +lemma ofColex_ne_ofColex {s t : Colex α} : ofColex s ≠ ofColex t ↔ s ≠ t := Iff.rfl + +/-- Recursor for `Colex α`. -/ +@[elab_as_elim] +def Colex.rec {C : Colex α → Sort*} (h : ∀ s, C (toColex s)) : ∀ s, C s := h + +namespace Colex +section LT +variable [LT α] {s t u : Finset α} + +/-- `s` is less than `t` in the colex ordering if the largest thing that's not in both sets is in t. +In other words, `max (s ∆ t) ∈ t` (if the maximum exists). -/ +instance instLT : LT (Colex α) := + ⟨fun s t ↦ ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t⟩ /-- We can define (≤) in the obvious way. -/ -instance Colex.instLE [LT α] : LE (Finset.Colex α) := - ⟨fun A B => A < B ∨ A = B⟩ +instance instLE : LE (Colex α) := ⟨fun s t ↦ s = t ∨ s < t⟩ -theorem Colex.lt_def [LT α] (A B : Finset α) : - A.toColex < B.toColex ↔ ∃ k, (∀ {x}, k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A ∧ k ∈ B := +lemma lt_def {s t : Colex α} : + s < t ↔ ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t := Iff.rfl -#align colex.lt_def Colex.lt_def -theorem Colex.le_def [LT α] (A B : Finset α) : - A.toColex ≤ B.toColex ↔ A.toColex < B.toColex ∨ A = B := +lemma le_def {s t : Colex α} : + s ≤ t ↔ s = t ∨ + ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t := Iff.rfl -#align colex.le_def Colex.le_def - -/-- If everything in `A` is less than `k`, we can bound the sum of powers. -/ -theorem Nat.sum_two_pow_lt {k : ℕ} {A : Finset ℕ} (h₁ : ∀ {x}, x ∈ A → x < k) : - A.sum (Nat.pow 2) < 2 ^ k := by - apply lt_of_le_of_lt (sum_le_sum_of_subset fun t => mem_range.2 ∘ h₁) - have z := geom_sum_mul_add 1 k - rw [mul_one, one_add_one_eq_two] at z - rw [← z] - apply Nat.lt_succ_self -#align nat.sum_two_pow_lt Nat.sum_two_pow_lt -namespace Colex +lemma toColex_lt_toColex : + toColex s < toColex t ↔ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := Iff.rfl + +lemma toColex_le_toColex : + toColex s ≤ toColex t ↔ s = t ∨ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := + Iff.rfl + +instance instIsIrrefl : IsIrrefl (Colex α) (· < ·) := ⟨by simp [lt_def]⟩ + +variable [DecidableEq α] + +/-- The colexigraphic order is insensitive to removing elements. -/ +lemma toColex_sdiff_lt_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : + toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t := by + simp only [toColex_lt_toColex, toColex_lt_toColex, mem_sdiff, not_and, not_not] + refine exists_congr fun k ↦ ⟨?_, ?_⟩ + · rintro ⟨h, hksu, hkt, hku⟩ + refine ⟨fun x hx ↦ ?_, mt hksu hku, hkt⟩ + specialize h hx + tauto + · rintro ⟨h, hks, hkt⟩ + exact ⟨fun x hx ↦ by rw [h hx], fun hks' ↦ (hks hks').elim, hkt, not_mem_mono hus hks⟩ + +@[simp] lemma toColex_sdiff_lt_toColex_sdiff' : + toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t := by + simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left s t) (inter_subset_right s t) + +end LT + +section LinearOrder +variable [LinearOrder α] [LinearOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} + {s t u : Finset α} {a b : α} {r : ℕ} + +instance : IsStrictTotalOrder (Colex α) (· < ·) where + irrefl := irrefl_of (· < ·) + trans s t u := by + rintro ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩ + obtain h | h := (ne_of_mem_of_not_mem inB notinB).lt_or_lt + · refine' ⟨k₂, fun x hx ↦ _, by rwa [k₁z h], inC⟩ + rw [←k₂z hx] + exact k₁z (h.trans hx) + · refine' ⟨k₁, fun x hx ↦ _, notinA, by rwa [←k₂z h]⟩ + rw [k₁z hx] + exact k₂z (h.trans hx) + trichotomous s t := by + classical + obtain rfl | hts := eq_or_ne t s + · simp + obtain ⟨k, hk, z⟩ := exists_max_image (ofColex t ∆ ofColex s) id (symmDiff_nonempty.2 hts) + refine' (mem_symmDiff.1 hk).imp (fun hk => ⟨k, fun a ha ↦ _, hk.2, hk.1⟩) fun hk ↦ + Or.inr ⟨k, fun a ha ↦ _, hk.2, hk.1⟩ <;> + simpa [mem_symmDiff, not_or, iff_iff_implies_and_implies, and_comm, not_imp_not] + using not_imp_not.2 (z a) ha.not_le + +instance instDecidableLT : @DecidableRel (Colex α) (· < ·) := fun s t ↦ + decidable_of_iff' + (∃ k ∈ ofColex t, + (∀ x ∈ ofColex s ∪ ofColex t, k < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ k ∉ ofColex s) $ + exists_congr fun a ↦ by + simp only [mem_union, exists_prop, or_imp, @and_comm (_ ∈ ofColex t), and_assoc] + exact and_congr_left' $ forall_congr' $ by tauto + +instance instLinearOrder : LinearOrder (Colex α) := linearOrderOfSTO (· < ·) + +instance instBot : Bot (Colex α) where + bot := toColex ∅ + +@[simp] lemma toColex_empty : toColex (∅ : Finset α) = ⊥ := rfl +@[simp] lemma ofColex_bot : ofColex (⊥ : Colex α) = ∅ := rfl + +instance instOrderBot : OrderBot (Colex α) where + bot_le s := by + induction' s using Finset.Colex.rec with s + rw [le_def] + obtain rfl | hs := s.eq_empty_or_nonempty + · simp + refine' Or.inr ⟨max' _ hs, _, by simp, max'_mem _ _⟩ + simp only [max'_lt_iff, ofColex_bot, not_mem_empty, ofColex_toColex, false_iff] + exact fun x hs hx ↦ lt_irrefl _ $ hs _ hx + +/-- The colexigraphic order is insensitive to removing elements. -/ +lemma toColex_sdiff_le_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : + toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t := by + rw [le_iff_le_iff_lt_iff_lt, toColex_sdiff_lt_toColex_sdiff hut hus] + +@[simp] lemma toColex_sdiff_le_toColex_sdiff' : + toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t := by + rw [le_iff_le_iff_lt_iff_lt, toColex_sdiff_lt_toColex_sdiff'] + +lemma colex_lt_of_ssubset (h : s ⊂ t) : toColex s < toColex t := by + rw [←toColex_sdiff_lt_toColex_sdiff', sdiff_eq_empty_iff_subset.2 h.1, toColex_empty, + bot_lt_iff_ne_bot, ←toColex_empty, toColex_ne_toColex] + simpa using h.not_subset + +/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as `⊆` is not a +linear order. -/ +lemma colex_le_of_subset (h : s ⊆ t) : toColex s ≤ toColex t := by + rw [←toColex_sdiff_le_toColex_sdiff', sdiff_eq_empty_iff_subset.2 h, toColex_empty]; exact bot_le + +instance [Fintype α] : BoundedOrder (Colex α) where + top := toColex univ + le_top _x := colex_le_of_subset (subset_univ _) + +@[simp] lemma toColex_univ [Fintype α] : toColex (univ : Finset α) = ⊤ := rfl +@[simp] lemma ofColex_top [Fintype α] : ofColex (⊤ : Colex α) = univ := rfl + +/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`. -/ +lemma toColex_lt_singleton : toColex s < toColex {a} ↔ ∀ x ∈ s, x < a := by + simp only [toColex_lt_toColex, mem_singleton, ←and_assoc, exists_eq_right, ←not_le (a := a)] + refine ⟨fun t x hx hax ↦ ?_, fun h ↦ ⟨fun z hz ↦ ?_, by simpa using h a⟩⟩ + · obtain hax | rfl := hax.lt_or_eq + · exact hax.ne' $ (t.1 hax).1 hx + · exact t.2 hx + · exact ⟨fun i ↦ ((h _ i) hz.le).elim, fun i ↦ (hz.ne' i).elim⟩ + +/-- `{a} ≤ s` in colex iff `r` contains an element greated than or equal to `a`. -/ +lemma singleton_le_toColex : (toColex {a} : Colex α) ≤ toColex s ↔ ∃ x ∈ s, a ≤ x := by + simp only [←not_lt, toColex_lt_singleton, not_forall, exists_prop] + +/-- Colex is an extension of the base order. -/ +lemma singleton_lt_singleton : (toColex {a} : Colex α) < toColex {b} ↔ a < b := by + simp [toColex_lt_singleton] + +/-- Colex is an extension of the base order. -/ +lemma singleton_le_singleton : (toColex {a} : Colex α) ≤ toColex {b} ↔ a ≤ b := by + rw [le_iff_le_iff_lt_iff_lt, singleton_lt_singleton] + +/-- If `s` is before `t` in colex, and everything in `t` is small, then everything in `s` is small. +-/ +lemma forall_lt_mono (h₁ : toColex s ≤ toColex t) (h₂ : ∀ x ∈ t, x < a) : ∀ x ∈ s, x < a := by + obtain rfl | ⟨k, z, -, hk⟩ := toColex_le_toColex.1 h₁ + · assumption + · refine' fun x hx => lt_of_not_le fun h ↦ h.not_lt $ h₂ x _ + rwa [←z ((h₂ k hk).trans_le h)] /-- Strictly monotone functions preserve the colex ordering. -/ -theorem hom_lt_iff {β : Type*} [LinearOrder α] [DecidableEq β] [Preorder β] {f : α → β} - (h₁ : StrictMono f) (A B : Finset α) : - (A.image f).toColex < (B.image f).toColex ↔ A.toColex < B.toColex := by - simp only [Colex.lt_def, not_exists, mem_image, exists_prop, not_and] +lemma toColex_image_lt_toColex_image (hf : StrictMono f) : + toColex (s.image f) < toColex (t.image f) ↔ toColex s < toColex t := by + simp only [toColex_lt_toColex, not_exists, mem_image, exists_prop, not_and] constructor · rintro ⟨k, z, q, k', _, rfl⟩ - exact - ⟨k', @fun x hx => by - simpa [h₁.injective.eq_iff] using z (h₁ hx), fun t => q _ t rfl, ‹k' ∈ B›⟩ + exact ⟨k', fun x hx => by simpa [hf.injective.eq_iff] using z (hf hx), + fun t ↦ q _ t rfl, ‹k' ∈ t›⟩ rintro ⟨k, z, ka, _⟩ - refine' ⟨f k, @fun x hx => _, _, k, ‹k ∈ B›, rfl⟩ + refine' ⟨f k, fun x hx ↦ _, _, k, ‹k ∈ t›, rfl⟩ · constructor - any_goals + all_goals rintro ⟨x', hx', rfl⟩ refine' ⟨x', _, rfl⟩ - first |rwa [← z _]|rwa [z _] - rwa [StrictMono.lt_iff_lt h₁] at hx - · simp only [h₁.injective, Function.Injective.eq_iff] - exact fun x hx => ne_of_mem_of_not_mem hx ka -#align colex.hom_lt_iff Colex.hom_lt_iff - -/-- A special case of `Colex.hom_lt_iff` which is sometimes useful. -/ -@[simp] -theorem hom_fin_lt_iff {n : ℕ} (A B : Finset (Fin n)) : - (A.image fun i : Fin n => (i : ℕ)).toColex < (B.image fun i : Fin n => (i : ℕ)).toColex ↔ - A.toColex < B.toColex := by - refine' Colex.hom_lt_iff _ _ _ - exact (fun x y k => k) -#align colex.hom_fin_lt_iff Colex.hom_fin_lt_iff - -instance [LT α] : IsIrrefl (Finset.Colex α) (· < ·) := - ⟨fun _ h => Exists.elim h fun _ ⟨_, a, b⟩ => a b⟩ - -@[trans] -theorem lt_trans [LinearOrder α] {a b c : Finset.Colex α} : a < b → b < c → a < c := by - rintro ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩ - cases' lt_or_gt_of_ne (ne_of_mem_of_not_mem inB notinB) with h h - · refine' ⟨k₂, @fun x hx => _, _, inC⟩ - rw [← k₂z hx] - apply k₁z (Trans.trans h hx) - rwa [k₁z h] - · refine' ⟨k₁, @fun x hx => _, notinA, by rwa [← k₂z h]⟩ - rw [k₁z hx] - apply k₂z (Trans.trans h hx) -#align colex.lt_trans Colex.lt_trans - -@[trans] -theorem le_trans [LinearOrder α] (a b c : Finset.Colex α) : a ≤ b → b ≤ c → a ≤ c := fun AB BC => - AB.elim (fun k => BC.elim (fun t => Or.inl (lt_trans k t)) fun t => t ▸ AB) fun k => k.symm ▸ BC -#align colex.le_trans Colex.le_trans - -instance [LinearOrder α] : IsTrans (Finset.Colex α) (· < ·) := - ⟨fun _ _ _ => Colex.lt_trans⟩ - -theorem lt_trichotomy [LinearOrder α] (A B : Finset.Colex α) : A < B ∨ A = B ∨ B < A := by - by_cases h₁ : A = B - · tauto - have h : Finset.Nonempty (A \ B ∪ B \ A) := by - rw [nonempty_iff_ne_empty] - intro a - simp only [union_eq_empty, sdiff_eq_empty_iff_subset] at a - apply h₁ (Subset.antisymm a.1 a.2) - rcases exists_max_image (A \ B ∪ B \ A) id h with ⟨k, ⟨hk, z⟩⟩ - · simp only [mem_union, mem_sdiff] at hk - cases' hk with hk hk - · right - right - refine' ⟨k, @fun t th => _, hk.2, hk.1⟩ - specialize z t - by_contra h₂ - simp only [mem_union, mem_sdiff, id.def] at z - rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm] at h₂ - apply not_le_of_lt th (z h₂) - · left - refine' ⟨k, @fun t th => _, hk.2, hk.1⟩ - specialize z t - by_contra h₃ - simp only [mem_union, mem_sdiff, id.def] at z - rw [not_iff, iff_iff_and_or_not_and_not, not_not, and_comm, or_comm] at h₃ - apply not_le_of_lt th (z h₃) -#align colex.lt_trichotomy Colex.lt_trichotomy - -instance [LinearOrder α] : IsTrichotomous (Finset.Colex α) (· < ·) := - ⟨lt_trichotomy⟩ - -instance decidableLt [LinearOrder α] : ∀ {A B : Finset.Colex α}, Decidable (A < B) := - show ∀ {A B : Finset α}, Decidable (A.toColex < B.toColex) from @fun A B => - decidable_of_iff' (∃ k ∈ B, (∀ x ∈ A ∪ B, k < x → (x ∈ A ↔ x ∈ B)) ∧ k ∉ A) - (by - rw [Colex.lt_def] - apply exists_congr - simp only [mem_union, exists_prop, or_imp, and_comm (a := _ ∈ B), and_assoc] - intro k - refine' and_congr_left' (forall_congr' _) - tauto) -#align colex.decidable_lt Colex.decidableLt - -instance [LinearOrder α] : LinearOrder (Finset.Colex α) := - { instLT, - instLE with - le_refl := fun A => Or.inr rfl - le_trans := le_trans - le_antisymm := fun A B AB BA => - AB.elim (fun k => BA.elim (fun t => (asymm k t).elim) fun t => t.symm) id - le_total := fun A B => - (lt_trichotomy A B).elim3 (Or.inl ∘ Or.inl) (Or.inl ∘ Or.inr) (Or.inr ∘ Or.inl) - -- Porting note: we must give some hints for instances - decidableLE := by - letI : DecidableEq (Finset.Colex α) := inferInstanceAs (DecidableEq (Finset α)) - exact fun A B => inferInstanceAs (Decidable (A < B ∨ A = B)) - decidableLT := inferInstance - decidableEq := inferInstanceAs (DecidableEq (Finset α)) - lt_iff_le_not_le := fun A B => by - constructor - · intro t - refine' ⟨Or.inl t, _⟩ - rintro (i | rfl) - · apply asymm_of _ t i - · apply irrefl _ t - rintro ⟨h₁ | rfl, h₂⟩ - · apply h₁ - apply h₂.elim (Or.inr rfl) } - -/-- The instances set up let us infer that `(· < ·)` is a strict total order. -/ -example [LinearOrder α] : IsStrictTotalOrder (Finset.Colex α) (· < ·) := - inferInstance + first + | rwa [←z _] + | rwa [z _] + rwa [StrictMono.lt_iff_lt hf] at hx + · simp only [hf.injective, Function.Injective.eq_iff] + exact fun x hx ↦ ne_of_mem_of_not_mem hx ka /-- Strictly monotone functions preserve the colex ordering. -/ -theorem hom_le_iff {β : Type*} [LinearOrder α] [LinearOrder β] {f : α → β} (h₁ : StrictMono f) - (A B : Finset α) : (A.image f).toColex ≤ (B.image f).toColex ↔ A.toColex ≤ B.toColex := by - rw [le_iff_le_iff_lt_iff_lt, hom_lt_iff h₁] -#align colex.hom_le_iff Colex.hom_le_iff +lemma toColex_image_le_toColex_image (hf : StrictMono f) : + toColex (s.image f) ≤ toColex (t.image f) ↔ toColex s ≤ toColex t := by + rw [le_iff_le_iff_lt_iff_lt, toColex_image_lt_toColex_image hf] --- Porting note: fixed the doc -/-- A special case of `hom_le_iff` which is sometimes useful. -/ -@[simp] -theorem hom_fin_le_iff {n : ℕ} (A B : Finset (Fin n)) : - (A.image fun i : Fin n => (i : ℕ)).toColex ≤ (B.image fun i : Fin n => (i : ℕ)).toColex ↔ - A.toColex ≤ B.toColex := - Colex.hom_le_iff Fin.val_strictMono _ _ -#align colex.hom_fin_le_iff Colex.hom_fin_le_iff +/-! ### Initial segments -/ -/-- If `A` is before `B` in colex, and everything in `B` is small, then everything in `A` is small. +/-- `𝒜` is an initial segment of the colexigraphic order on sets of `r`, and that if `t` is below +`s` in colex where `t` has size `r` and `s` is in `𝒜`, then `t` is also in `𝒜`. In effect, `𝒜` is +downwards closed with respect to colex among sets of size `r`. -/ +def IsInitSeg (𝒜 : Finset (Finset α)) (r : ℕ) : Prop := + (𝒜 : Set (Finset α)).Sized r ∧ + ∀ ⦃s t : Finset α⦄, s ∈ 𝒜 → toColex t < toColex s ∧ t.card = r → t ∈ 𝒜 + +@[simp] lemma isInitSeg_empty : IsInitSeg (∅ : Finset (Finset α)) r := by simp [IsInitSeg] + +/-- Initial segments are nested in some way. In particular, if they're the same size they're equal. -/ -theorem forall_lt_of_colex_lt_of_forall_lt [LinearOrder α] {A B : Finset α} (t : α) - (h₁ : A.toColex < B.toColex) (h₂ : ∀ x ∈ B, x < t) : ∀ x ∈ A, x < t := by - rw [Colex.lt_def] at h₁ - rcases h₁ with ⟨k, z, _, _⟩ - intro x hx - apply lt_of_not_ge - intro a - refine' not_lt_of_ge a (h₂ x _) - rwa [← z] - apply lt_of_lt_of_le (h₂ k ‹_›) a -#align colex.forall_lt_of_colex_lt_of_forall_lt Colex.forall_lt_of_colex_lt_of_forall_lt - -/-- `s.toColex < {r}.toColex` iff all elements of `s` are less than `r`. -/ -theorem lt_singleton_iff_mem_lt [LinearOrder α] {r : α} {s : Finset α} : - s.toColex < ({r} : Finset α).toColex ↔ ∀ x ∈ s, x < r := by - simp only [lt_def, mem_singleton, ← and_assoc, exists_eq_right] - constructor - · intro t x hx - rw [← not_le] - intro h - rcases lt_or_eq_of_le h with (h₁ | rfl) - · exact ne_of_irrefl h₁ ((t.1 h₁).1 hx).symm - · exact t.2 hx - · exact fun h => - ⟨fun {z} hz => ⟨fun i => (asymm hz (h _ i)).elim, fun i => (hz.ne' i).elim⟩, - by simpa using h r⟩ -#align colex.lt_singleton_iff_mem_lt Colex.lt_singleton_iff_mem_lt - --- Porting note: fixed the doc -/-- If `{r}` is less than or equal to s in the colexicographical sense, - then s contains an element greater than or equal to r. -/ -theorem mem_le_of_singleton_le [LinearOrder α] {r : α} {s : Finset α} : - ({r} : Finset α).toColex ≤ s.toColex ↔ ∃ x ∈ s, r ≤ x := by - simp only [← not_lt] - simp [lt_singleton_iff_mem_lt] -#align colex.mem_le_of_singleton_le Colex.mem_le_of_singleton_le - -/-- Colex is an extension of the base ordering on α. -/ -theorem singleton_lt_iff_lt [LinearOrder α] {r s : α} : - ({r} : Finset α).toColex < ({s} : Finset α).toColex ↔ r < s := by simp [lt_singleton_iff_mem_lt] -#align colex.singleton_lt_iff_lt Colex.singleton_lt_iff_lt - -/-- Colex is an extension of the base ordering on α. -/ -theorem singleton_le_iff_le [LinearOrder α] {r s : α} : - ({r} : Finset α).toColex ≤ ({s} : Finset α).toColex ↔ r ≤ s := by - rw [le_iff_le_iff_lt_iff_lt, singleton_lt_iff_lt] -#align colex.singleton_le_iff_le Colex.singleton_le_iff_le - -/-- Colex doesn't care if you remove the other set -/ -@[simp] -theorem sdiff_lt_sdiff_iff_lt [LT α] [DecidableEq α] (A B : Finset α) : - (A \ B).toColex < (B \ A).toColex ↔ A.toColex < B.toColex := by - rw [Colex.lt_def, Colex.lt_def] - apply exists_congr - intro k - simp only [mem_sdiff, not_and, not_not] - constructor - · rintro ⟨z, kAB, kB, kA⟩ - refine' ⟨_, kA, kB⟩ - · intro x hx - specialize z hx - tauto - · rintro ⟨z, kA, kB⟩ - refine' ⟨_, fun _ => kB, kB, kA⟩ - intro x hx - rw [z hx] -#align colex.sdiff_lt_sdiff_iff_lt Colex.sdiff_lt_sdiff_iff_lt +lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) : 𝒜₁ ⊆ 𝒜₂ ∨ 𝒜₂ ⊆ 𝒜₁ := by + classical + simp_rw [←sdiff_eq_empty_iff_subset, ←not_nonempty_iff_eq_empty] + by_contra' h + obtain ⟨⟨s, hs⟩, t, ht⟩ := h + rw [mem_sdiff] at hs ht + obtain hst | rfl | hts := trichotomous_of (· < ·) (toColex s) (toColex t) + · exact hs.2 $ h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩ + · exact ht.2 hs.1 + · exact ht.2 $ h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩ + +variable [Fintype α] + +/-- Gives all sets up to `s` with the same size as it: this is equivalent to +being an initial segment of colex. -/ +def initSeg (s : Finset α) : Finset (Finset α) := + univ.filter fun t ↦ s.card = t.card ∧ toColex t ≤ toColex s -/-- Colex doesn't care if you remove the other set -/ @[simp] -theorem sdiff_le_sdiff_iff_le [LinearOrder α] (A B : Finset α) : - (A \ B).toColex ≤ (B \ A).toColex ↔ A.toColex ≤ B.toColex := by - rw [le_iff_le_iff_lt_iff_lt, sdiff_lt_sdiff_iff_lt] -#align colex.sdiff_le_sdiff_iff_le Colex.sdiff_le_sdiff_iff_le - -theorem empty_toColex_lt [LinearOrder α] {A : Finset α} (hA : A.Nonempty) : - (∅ : Finset α).toColex < A.toColex := by - rw [Colex.lt_def] - refine' ⟨max' _ hA, _, by simp, max'_mem _ _⟩ - simp only [false_iff_iff, not_mem_empty] - intro x hx t - apply not_le_of_lt hx (le_max' _ _ t) -#align colex.empty_to_colex_lt Colex.empty_toColex_lt - -/-- If `A ⊂ B`, then `A` is less than `B` in the colex order. Note the converse does not hold, as -`⊆` is not a linear order. -/ -theorem colex_lt_of_ssubset [LinearOrder α] {A B : Finset α} (h : A ⊂ B) : - A.toColex < B.toColex := by - rw [← sdiff_lt_sdiff_iff_lt, sdiff_eq_empty_iff_subset.2 h.1] - exact empty_toColex_lt (by simpa [Finset.Nonempty] using exists_of_ssubset h) -#align colex.colex_lt_of_ssubset Colex.colex_lt_of_ssubset +lemma mem_initSeg : t ∈ initSeg s ↔ s.card = t.card ∧ toColex t ≤ toColex s := by simp [initSeg] + +lemma mem_initSeg_self : s ∈ initSeg s := by simp +@[simp] lemma initSeg_nonempty : (initSeg s).Nonempty := ⟨s, mem_initSeg_self⟩ + +lemma isInitSeg_initSeg : IsInitSeg (initSeg s) s.card := by + refine ⟨fun t ht => (mem_initSeg.1 ht).1.symm, fun t₁ t₂ ht₁ ht₂ ↦ mem_initSeg.2 ⟨ht₂.2.symm, ?_⟩⟩ + rw [mem_initSeg] at ht₁ + exact ht₂.1.le.trans ht₁.2 + +lemma IsInitSeg.exists_initSeg (h𝒜 : IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonempty) : + ∃ s : Finset α, s.card = r ∧ 𝒜 = initSeg s := by + have hs := sup'_mem (ofColex ⁻¹' 𝒜) (LinearOrder.supClosed _) 𝒜 h𝒜₀ toColex + (fun a ha ↦ by simpa using ha) + refine' ⟨_, h𝒜.1 hs, _⟩ + ext t + rw [mem_initSeg] + refine' ⟨fun p ↦ _, _⟩ + · rw [h𝒜.1 p, h𝒜.1 hs] + exact ⟨rfl, le_sup' _ p⟩ + rintro ⟨cards, le⟩ + obtain p | p := le.eq_or_lt + · rwa [toColex_inj.1 p] + · exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩ + +/-- Being a nonempty initial segment of colex if equivalent to being an `initSeg`. -/ +lemma isInitSeg_iff_exists_initSeg : + IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s : Finset α, s.card = r ∧ 𝒜 = initSeg s := by + refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩ + rintro ⟨s, rfl, rfl⟩ + exact ⟨isInitSeg_initSeg, initSeg_nonempty⟩ + +end LinearOrder +end Colex -@[simp] -theorem empty_toColex_le [LinearOrder α] {A : Finset α} : (∅ : Finset α).toColex ≤ A.toColex := by - rcases A.eq_empty_or_nonempty with (rfl | hA) - · simp - · apply (empty_toColex_lt hA).le -#align colex.empty_to_colex_le Colex.empty_toColex_le +open Colex -/-- If `A ⊆ B`, then `A ≤ B` in the colex order. Note the converse does not hold, as `⊆` is not a -linear order. -/ -theorem colex_le_of_subset [LinearOrder α] {A B : Finset α} (h : A ⊆ B) : - A.toColex ≤ B.toColex := by - rw [← sdiff_le_sdiff_iff_le, sdiff_eq_empty_iff_subset.2 h] - apply empty_toColex_le -#align colex.colex_le_of_subset Colex.colex_le_of_subset - -/-- The function from finsets to finsets with the colex order is a relation homomorphism. -/ -@[simps] -def toColexRelHom [LinearOrder α] : - ((· ⊆ ·) : Finset α → Finset α → Prop) →r ((· ≤ ·) : Finset.Colex α → Finset.Colex α → Prop) - where - toFun := Finset.toColex - map_rel' {_ _} := colex_le_of_subset -#align colex.to_colex_rel_hom Colex.toColexRelHom - -instance [LinearOrder α] : OrderBot (Finset.Colex α) where - bot := (∅ : Finset α).toColex - bot_le _ := empty_toColex_le - -instance [LinearOrder α] [Fintype α] : OrderTop (Finset.Colex α) where - top := Finset.univ.toColex - le_top _ := colex_le_of_subset (subset_univ _) - -instance [LinearOrder α] : Lattice (Finset.Colex α) := - { inferInstanceAs (SemilatticeSup (Finset.Colex α)), - inferInstanceAs (SemilatticeInf (Finset.Colex α)) with } - -instance [LinearOrder α] [Fintype α] : BoundedOrder (Finset.Colex α) := - { inferInstanceAs (OrderTop (Finset.Colex α)), - inferInstanceAs (OrderBot (Finset.Colex α)) with } - -/-- For subsets of ℕ, we can show that colex is equivalent to binary. -/ -theorem sum_two_pow_lt_iff_lt (A B : Finset ℕ) : - ((∑ i in A, 2 ^ i) < ∑ i in B, 2 ^ i) ↔ A.toColex < B.toColex := by - have z : ∀ A B : Finset ℕ, A.toColex < B.toColex → ∑ i in A, 2 ^ i < ∑ i in B, 2 ^ i := by - intro A B - rw [← sdiff_lt_sdiff_iff_lt, Colex.lt_def] - rintro ⟨k, z, kA, kB⟩ - rw [← sdiff_union_inter A B] - conv_rhs => rw [← sdiff_union_inter B A] +/-! +### Colex on `ℕ` + +The colexicographic order agrees with the order induced by interpreting a set of naturals as a +binary expansion. +-/ + +section Nat +variable {s t : Finset ℕ} + +/-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order +induced by the binary expansion. -/ +lemma sum_two_pow_lt_iff_colex_lt : ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i ↔ toColex s < toColex t := by + have z : ∀ s t : Finset ℕ, toColex s < toColex t → ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i := by + intro s t + rw [←toColex_sdiff_lt_toColex_sdiff', toColex_lt_toColex] + rintro ⟨a, ha, has, hat⟩ + rw [←sdiff_union_inter s t] + conv_rhs => rw [←sdiff_union_inter t s] rw [sum_union (disjoint_sdiff_inter _ _), sum_union (disjoint_sdiff_inter _ _), inter_comm, add_lt_add_iff_right] - apply lt_of_lt_of_le (@Nat.sum_two_pow_lt k (A \ B) _) - · apply single_le_sum (fun _ _ => Nat.zero_le _) kB + apply (@Nat.sum_two_pow_lt a (s \ t) _).trans_le + · apply single_le_sum (fun _ _ ↦ Nat.zero_le _) hat intro x hx - apply lt_of_le_of_ne (le_of_not_lt _) - · apply ne_of_mem_of_not_mem hx kA - -- Porting note: `intro` required because `apply` behaves differently - intro kx - have := (z kx).1 hx + refine' (ne_of_mem_of_not_mem hx has).lt_or_lt.resolve_right $ fun hax ↦ _ + have := (ha hax).1 hx rw [mem_sdiff] at this hx exact hx.2 this.1 - refine' - ⟨fun h => (lt_trichotomy A B).resolve_right fun h₁ => h₁.elim _ (not_lt_of_gt h ∘ z _ _), z A B⟩ + refine' ⟨fun h ↦ (lt_trichotomy (toColex s) $ toColex t).resolve_right fun h₁ ↦ + h₁.elim _ (not_lt_of_gt h ∘ z _ _), z s t⟩ + rw [toColex_inj] rintro rfl - apply irrefl _ h -#align colex.sum_two_pow_lt_iff_lt Colex.sum_two_pow_lt_iff_lt + exact irrefl _ h -/-- For subsets of ℕ, we can show that colex is equivalent to binary. -/ -theorem sum_two_pow_le_iff_lt (A B : Finset ℕ) : - ((∑ i in A, 2 ^ i) ≤ ∑ i in B, 2 ^ i) ↔ A.toColex ≤ B.toColex := by - rw [le_iff_le_iff_lt_iff_lt, sum_two_pow_lt_iff_lt] -#align colex.sum_two_pow_le_iff_lt Colex.sum_two_pow_le_iff_lt +/-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order +induced by the binary expansion. -/ +lemma sum_two_pow_le_iff_colex_le : ∑ i in s, 2 ^ i ≤ ∑ i in t, 2 ^ i ↔ toColex s ≤ toColex t := by + rw [le_iff_le_iff_lt_iff_lt, sum_two_pow_lt_iff_colex_lt] -end Colex +end Nat +end Finset From c1b79f4be5d38c7036ce1defc80f96c36442a746 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 16 Oct 2023 17:12:16 +0000 Subject: [PATCH 02/12] Kruskal-Katona theorem --- Mathlib/Combinatorics/Colex.lean | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index e92941b872369..1b79e1209284b 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -10,18 +10,19 @@ import Mathlib.Order.SupClosed #align_import combinatorics.colex from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c" /-! -# Colex - -We define the colex ordering for finite sets, and give a couple of important -lemmas and properties relating to it. - -The colex ordering likes to avoid large values - In the special case of `ℕ`, it can be thought of as -the "binary" ordering. That is, order s based on `∑_{i ∈ s} 2^i`. -It's defined here in a slightly more general way, requiring only `LT α` in -the definition of colex on `Finset α`. In the context of the Kruskal-Katona -lemma, we are interested in particular on how colex behaves for sets of a -fixed size. If the size is 3, colex on ℕ starts -123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ... +# Colexigraphic order + +We define the colex order for finite sets, and give a couple of important lemmas and properties +relating to it. + +The colex ordering likes to avoid large values: If the biggest element of `t` is bigger than all elements of `s`, then `s < t`. + +In the special case of `ℕ`, it can be thought of as the "binary" ordering. That is, order `s` based +on `∑_{i ∈ s} 2^i`. It's defined here on `Finset α` for any linear order `α`. + +In the context of the Kruskal-Katona theorem, we are interested in how colex behaves for sets of a +fixed size. Eg for size 3, the colex order on ℕ starts +`123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ...` ## Main statements From 68e125c5ed86c540dae540efc0310da41641460c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 18 Oct 2023 05:43:37 +0000 Subject: [PATCH 03/12] turn into a one-field structure --- Mathlib/Combinatorics/Colex.lean | 42 ++++++++++++++++---------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 1b79e1209284b..9e999cd1c3d69 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -75,29 +75,28 @@ namespace Finset /-- Type synonym of `Finset α` equipped with the colexicographic order rather than the inclusion order. -/ -def Colex (α) := Finset α +@[ext] +structure Colex (α) := toColex :: (ofColex : Finset α) -instance : Inhabited (Finset.Colex α) := inferInstanceAs (Inhabited (Finset α)) +-- TODO: Why can't we export? +--export Colex (toColex) + +open Colex /-- `toColex` is the "identity" function between `Finset α` and `Finset.Colex α`. -/ -def toColex : Finset α ≃ Colex α := Equiv.refl _ +add_decl_doc toColex /-- `ofColex` is the "identity" function between `Finset.Colex α` and `Finset α`. -/ -def ofColex : Colex α ≃ Finset α := Equiv.refl _ +add_decl_doc ofColex -@[simp] lemma toColex_symm_eq : (@toColex α).symm = ofColex := rfl -@[simp] lemma ofColex_symm_eq : (@ofColex α).symm = toColex := rfl -@[simp] lemma toColex_ofColex (s : Colex α) : toColex (ofColex s) = s := rfl -@[simp] lemma ofColex_toColex (s : Finset α) : ofColex (toColex s) = s := rfl --- Tagged `nolint simpNF` because eligible for `dsimp` -@[simp, nolint simpNF] lemma toColex_inj {s t : Finset α} : toColex s = toColex t ↔ s = t := Iff.rfl -@[simp, nolint simpNF] lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t := Iff.rfl -lemma toColex_ne_toColex {s t : Finset α} : toColex s ≠ toColex t ↔ s ≠ t := Iff.rfl -lemma ofColex_ne_ofColex {s t : Colex α} : ofColex s ≠ ofColex t ↔ s ≠ t := Iff.rfl +instance : Inhabited (Colex α) := ⟨⟨∅⟩⟩ -/-- Recursor for `Colex α`. -/ -@[elab_as_elim] -def Colex.rec {C : Colex α → Sort*} (h : ∀ s, C (toColex s)) : ∀ s, C s := h +@[simp] lemma toColex_ofColex (s : Colex α) : toColex (ofColex s) = s := rfl +lemma ofColex_toColex (s : Finset α) : ofColex (toColex s) = s := rfl +lemma toColex_inj {s t : Finset α} : toColex s = toColex t ↔ s = t := by simp +@[simp] lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t := by cases s; cases t; simp +lemma toColex_ne_toColex {s t : Finset α} : toColex s ≠ toColex t ↔ s ≠ t := by simp +lemma ofColex_ne_ofColex {s t : Colex α} : ofColex s ≠ ofColex t ↔ s ≠ t := by simp namespace Colex section LT @@ -124,8 +123,8 @@ lemma toColex_lt_toColex : toColex s < toColex t ↔ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := Iff.rfl lemma toColex_le_toColex : - toColex s ≤ toColex t ↔ s = t ∨ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := - Iff.rfl + toColex s ≤ toColex t ↔ s = t ∨ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := by + simp [le_def] instance instIsIrrefl : IsIrrefl (Colex α) (· < ·) := ⟨by simp [lt_def]⟩ @@ -168,7 +167,7 @@ instance : IsStrictTotalOrder (Colex α) (· < ·) where classical obtain rfl | hts := eq_or_ne t s · simp - obtain ⟨k, hk, z⟩ := exists_max_image (ofColex t ∆ ofColex s) id (symmDiff_nonempty.2 hts) + obtain ⟨k, hk, z⟩ := exists_max_image _ id (symmDiff_nonempty.2 $ ofColex_ne_ofColex.2 hts) refine' (mem_symmDiff.1 hk).imp (fun hk => ⟨k, fun a ha ↦ _, hk.2, hk.1⟩) fun hk ↦ Or.inr ⟨k, fun a ha ↦ _, hk.2, hk.1⟩ <;> simpa [mem_symmDiff, not_or, iff_iff_implies_and_implies, and_comm, not_imp_not] @@ -300,9 +299,10 @@ lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) by_contra' h obtain ⟨⟨s, hs⟩, t, ht⟩ := h rw [mem_sdiff] at hs ht - obtain hst | rfl | hts := trichotomous_of (· < ·) (toColex s) (toColex t) + obtain hst | hst | hts := trichotomous_of (α := Colex α) (· < ·) (toColex s) (toColex t) · exact hs.2 $ h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩ - · exact ht.2 hs.1 + · simp only [toColex.injEq] at hst + exact ht.2 $ hst ▸ hs.1 · exact ht.2 $ h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩ variable [Fintype α] From dfe40930f5e673e798d556aaa5982bb5014a884e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 18 Oct 2023 21:50:54 +0200 Subject: [PATCH 04/12] for example Co-authored-by: Bhavik Mehta --- Mathlib/Combinatorics/Colex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 9e999cd1c3d69..5901e4e30d00b 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -21,7 +21,7 @@ In the special case of `ℕ`, it can be thought of as the "binary" ordering. Tha on `∑_{i ∈ s} 2^i`. It's defined here on `Finset α` for any linear order `α`. In the context of the Kruskal-Katona theorem, we are interested in how colex behaves for sets of a -fixed size. Eg for size 3, the colex order on ℕ starts +fixed size. For example, for size 3, the colex order on ℕ starts `123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ...` ## Main statements From 831fc09130fa4f26b6fdab9800af498409515e0d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 18 Oct 2023 21:52:14 +0200 Subject: [PATCH 05/12] claim authorship --- Mathlib/Combinatorics/Colex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 5901e4e30d00b..5829aa62d9e06 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2020 Bhavik Mehta. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bhavik Mehta, Alena Gusakov +Authors: Bhavik Mehta, Alena Gusakov, Yaël Dillies -/ import Mathlib.Algebra.GeomSum import Mathlib.Data.Finset.Slice From fc31223344758c1810e61bf08bd63b08c96c4c7a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 18 Oct 2023 21:52:25 +0200 Subject: [PATCH 06/12] typo Co-authored-by: Bhavik Mehta --- Mathlib/Combinatorics/Colex.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 5829aa62d9e06..488fc2e26fa64 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -30,7 +30,7 @@ fixed size. For example, for size 3, the colex order on ℕ starts * `Finset.Colex.forall_lt_mono`: if `s < t` in colex, and everything in `t` is `< a`, then everything in `s` is `< a`. This confirms the idea that an enumeration under colex will exhaust all sets using elements `< a` before allowing `a` to be included. -* `Finse.toColex_image_lt_toColex_image`: Strictly monotone functions preserve colex. +* `Finset.toColex_image_lt_toColex_image`: Strictly monotone functions preserve colex. * `Finset.sum_two_pow_le_iff_colex_le`: colex for α = ℕ is the same as binary (this also proves binary expansions are unique) From baaf2d937ef7dac6ee38c88f729f5fced632f674 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 21 Oct 2023 17:34:12 -0400 Subject: [PATCH 07/12] chore: bump lean toolchain --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index aac5c604dccb7..183a307edb2d1 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc2 +leanprover/lean4:v4.2.0-rc4 From de19b8b408af982a78c65820d7bd5d1c944a10d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 21 Oct 2023 22:13:46 +0000 Subject: [PATCH 08/12] fancy new def --- Mathlib/Algebra/BigOperators/Order.lean | 12 + Mathlib/Algebra/GeomSum.lean | 10 + Mathlib/Combinatorics/Colex.lean | 383 ++++++++++++------------ Mathlib/Data/Finset/Basic.lean | 3 + Mathlib/Order/BooleanAlgebra.lean | 9 + 5 files changed, 233 insertions(+), 184 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Order.lean b/Mathlib/Algebra/BigOperators/Order.lean index 4ad6c01c03fa9..3d39bd76c5beb 100644 --- a/Mathlib/Algebra/BigOperators/Order.lean +++ b/Mathlib/Algebra/BigOperators/Order.lean @@ -540,6 +540,18 @@ theorem prod_eq_prod_iff_of_le {f g : ι → M} (h : ∀ i ∈ s, f i ≤ g i) : #align finset.prod_eq_prod_iff_of_le Finset.prod_eq_prod_iff_of_le #align finset.sum_eq_sum_iff_of_le Finset.sum_eq_sum_iff_of_le +variable [DecidableEq ι] + +@[to_additive] lemma prod_sdiff_le_prod_sdiff : + ∏ i in s \ t, f i ≤ ∏ i in t \ s, f i ↔ ∏ i in s, f i ≤ ∏ i in t, f i := by + rw [←mul_le_mul_iff_right, ←prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter, ←prod_union, + inter_comm, sdiff_union_inter]; simpa only [inter_comm] using disjoint_sdiff_inter t s + +@[to_additive] lemma prod_sdiff_lt_prod_sdiff : + ∏ i in s \ t, f i < ∏ i in t \ s, f i ↔ ∏ i in s, f i < ∏ i in t, f i := by + rw [←mul_lt_mul_iff_right, ←prod_union (disjoint_sdiff_inter _ _), sdiff_union_inter, ←prod_union, + inter_comm, sdiff_union_inter]; simpa only [inter_comm] using disjoint_sdiff_inter t s + end OrderedCancelCommMonoid section LinearOrderedCancelCommMonoid diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index e5aec67a3a769..de5db4b7693ff 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -584,3 +584,13 @@ theorem geom_sum_neg_iff [LinearOrderedRing α] (hn : n ≠ 0) : #align geom_sum_neg_iff geom_sum_neg_iff end Order + +/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of +`2` is less than `2 ^ n`. -/ +lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : + ∑ k in s, 2 ^ k < 2 ^ n := by + calc + ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 <| hs _ hk + _ = 2 ^ n - 1 := by + simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] + _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 488fc2e26fa64..6e8d84981dc6d 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -15,7 +15,8 @@ import Mathlib.Order.SupClosed We define the colex order for finite sets, and give a couple of important lemmas and properties relating to it. -The colex ordering likes to avoid large values: If the biggest element of `t` is bigger than all elements of `s`, then `s < t`. +The colex ordering likes to avoid large values: If the biggest element of `t` is bigger than all +elements of `s`, then `s < t`. In the special case of `ℕ`, it can be thought of as the "binary" ordering. That is, order `s` based on `∑_{i ∈ s} 2^i`. It's defined here on `Finset α` for any linear order `α`. @@ -56,17 +57,9 @@ Related files are: colex, colexicographic, binary -/ -open Finset +open Finset Function open scoped BigOperators -/-- If all the elements of a finset `s` of naturals are less than `n`, then the sum of their powers of `2` is less than `2 ^ k`. -/ -lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : - ∑ k in s, 2 ^ k < 2 ^ n := by - calc - ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk - _ = 2 ^ n - 1 := by - simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] - _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one #align nat.sum_two_pow_lt Nat.sum_two_pow_lt variable {α β : Type*} @@ -94,191 +87,225 @@ instance : Inhabited (Colex α) := ⟨⟨∅⟩⟩ @[simp] lemma toColex_ofColex (s : Colex α) : toColex (ofColex s) = s := rfl lemma ofColex_toColex (s : Finset α) : ofColex (toColex s) = s := rfl lemma toColex_inj {s t : Finset α} : toColex s = toColex t ↔ s = t := by simp -@[simp] lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t := by cases s; cases t; simp +@[simp] +lemma ofColex_inj {s t : Colex α} : ofColex s = ofColex t ↔ s = t := by cases s; cases t; simp lemma toColex_ne_toColex {s t : Finset α} : toColex s ≠ toColex t ↔ s ≠ t := by simp lemma ofColex_ne_ofColex {s t : Colex α} : ofColex s ≠ ofColex t ↔ s ≠ t := by simp -namespace Colex -section LT -variable [LT α] {s t u : Finset α} +lemma toColex_injective : Injective (toColex : Finset α → Colex α) := fun _ _ ↦ toColex_inj.1 +lemma ofColex_injective : Injective (ofColex : Colex α → Finset α) := fun _ _ ↦ ofColex_inj.1 -/-- `s` is less than `t` in the colex ordering if the largest thing that's not in both sets is in t. -In other words, `max (s ∆ t) ∈ t` (if the maximum exists). -/ -instance instLT : LT (Colex α) := - ⟨fun s t ↦ ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t⟩ +namespace Colex +section PartialOrder +variable [PartialOrder α] [PartialOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} + {s t u : Finset α} {a b : α} -/-- We can define (≤) in the obvious way. -/ -instance instLE : LE (Colex α) := ⟨fun s t ↦ s = t ∨ s < t⟩ +instance instLE : LE (Colex α) := + ⟨fun s t ↦ ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b⟩ -lemma lt_def {s t : Colex α} : - s < t ↔ ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t := - Iff.rfl +private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toColex u) + (a : α) (has : a ∈ s) (hat : a ∉ t) : + ∃ b : α, b ∈ u ∧ b ∉ s ∧ a ≤ b := by + classical + let s' : Finset α := s.filter (fun a' => a' ∉ t ∧ a ≤ a') + have ⟨b, hb, hbmax⟩ := exists_maximal s' ⟨a, by simp [has, hat]⟩ + simp only [mem_filter, and_imp] at hb hbmax + have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1 + by_cases hcu : c ∈ u + · exact ⟨c, hcu, hcs, hb.2.2.trans hbc⟩ + have ⟨d, hdu, hdt, hcd⟩ := htu hct hcu + have had : a ≤ d := hb.2.2.trans <| hbc.trans hcd + refine ⟨d, hdu, fun hds ↦ ?_, had⟩ + exact hbmax d hds hdt had <| hbc.trans_lt <| hcd.lt_of_ne <| ne_of_mem_of_not_mem hct hdt + +private lemma antisymm_aux (hst : toColex s ≤ toColex t) (hts : toColex t ≤ toColex s) : s ⊆ t := by + intro a has + by_contra' hat + have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts a has hat + exact hb₂ hb₁ + +instance instPartialOrder : PartialOrder (Colex α) where + le_refl s a ha ha' := (ha' ha).elim + le_antisymm s t hst hts := Colex.ext _ _ <| (antisymm_aux hst hts).antisymm (antisymm_aux hts hst) + le_trans s t u hst htu a has hau := by + by_cases hat : a ∈ ofColex t + · have ⟨b, hbu, hbt, hab⟩ := htu hat hau + by_cases hbs : b ∈ ofColex s + · have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu b hbs hbt + exact ⟨c, hcu, hcs, hab.trans hbc⟩ + · exact ⟨b, hbu, hbs, hab⟩ + · exact trans_aux hst htu _ has hat lemma le_def {s t : Colex α} : - s ≤ t ↔ s = t ∨ - ∃ a, (∀ ⦃x⦄, a < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ a ∉ ofColex s ∧ a ∈ ofColex t := + s ≤ t ↔ ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b := Iff.rfl +lemma toColex_le_toColex : + toColex s ≤ toColex t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t → ∃ b, b ∈ t ∧ b ∉ s ∧ a ≤ b := Iff.rfl + lemma toColex_lt_toColex : - toColex s < toColex t ↔ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := Iff.rfl + toColex s < toColex t ↔ s ≠ t ∧ ∀ ⦃a⦄, a ∈ s → a ∉ t → ∃ b, b ∈ t ∧ b ∉ s ∧ a ≤ b := by + simp [lt_iff_le_and_ne, toColex_le_toColex, and_comm] -lemma toColex_le_toColex : - toColex s ≤ toColex t ↔ s = t ∨ ∃ k, (∀ ⦃x⦄, k < x → (x ∈ s ↔ x ∈ t)) ∧ k ∉ s ∧ k ∈ t := by - simp [le_def] +/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as inclusion does +not form a linear order. -/ +lemma toColex_mono : Monotone (toColex : Finset α → Colex α) := + fun _s _t hst _a has hat ↦ (hat <| hst has).elim -instance instIsIrrefl : IsIrrefl (Colex α) (· < ·) := ⟨by simp [lt_def]⟩ +/-- If `s ⊂ t`, then `s < t` in the colex order. Note the converse does not hold, as inclusion does +not form a linear order. -/ +lemma toColex_strictMono : StrictMono (toColex : Finset α → Colex α) := + toColex_mono.strictMono_of_injective toColex_injective -variable [DecidableEq α] +instance instOrderBot : OrderBot (Colex α) where + bot := toColex ∅ + bot_le s a ha := by cases ha -/-- The colexigraphic order is insensitive to removing elements. -/ -lemma toColex_sdiff_lt_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : - toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t := by - simp only [toColex_lt_toColex, toColex_lt_toColex, mem_sdiff, not_and, not_not] - refine exists_congr fun k ↦ ⟨?_, ?_⟩ - · rintro ⟨h, hksu, hkt, hku⟩ - refine ⟨fun x hx ↦ ?_, mt hksu hku, hkt⟩ - specialize h hx - tauto - · rintro ⟨h, hks, hkt⟩ - exact ⟨fun x hx ↦ by rw [h hx], fun hks' ↦ (hks hks').elim, hkt, not_mem_mono hus hks⟩ +@[simp] lemma toColex_empty : toColex (∅ : Finset α) = ⊥ := rfl +@[simp] lemma ofColex_bot : ofColex (⊥ : Colex α) = ∅ := rfl -@[simp] lemma toColex_sdiff_lt_toColex_sdiff' : - toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t := by - simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left s t) (inter_subset_right s t) +/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/ +lemma forall_le_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b ≤ a) : ∀ b ∈ s, b ≤ a := by + rintro b hb + by_cases b ∈ t + · exact ht _ ‹_› + · obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_› + exact hbc.trans <| ht _ hct + +/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small. -/ +lemma forall_lt_mono (hst : toColex s ≤ toColex t) (ht : ∀ b ∈ t, b < a) : ∀ b ∈ s, b < a := by + rintro b hb + by_cases b ∈ t + · exact ht _ ‹_› + · obtain ⟨c, hct, -, hbc⟩ := hst hb ‹_› + exact hbc.trans_lt <| ht _ hct + +/-- `s ≤ {a}` in colex iff all elements of `s` are strictly less than `a`, except possibly `a` in +which case `s = {a}`. -/ +lemma toColex_le_singleton : toColex s ≤ toColex {a} ↔ ∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a) := by + simp only [toColex_le_toColex, mem_singleton, and_assoc, exists_eq_left] + refine forall₂_congr fun b _ ↦ ?_; obtain rfl | hba := eq_or_ne b a <;> aesop -end LT +/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`. -/ +lemma toColex_lt_singleton : toColex s < toColex {a} ↔ ∀ b ∈ s, b < a := by + rw [lt_iff_le_and_ne, toColex_le_singleton, toColex_ne_toColex] + refine ⟨fun h b hb ↦ (h.1 _ hb).1.lt_of_ne ?_, + fun h ↦ ⟨fun b hb ↦ ⟨(h _ hb).le, fun ha ↦ (lt_irrefl _ <| h _ ha).elim⟩, ?_⟩⟩ <;> rintro rfl + · refine h.2 <| eq_singleton_iff_unique_mem.2 ⟨hb, fun c hc ↦ (h.1 _ hc).2 hb⟩ + · simp at h + +/-- `{a} ≤ s` in colex iff `s` contains an element greated than or equal to `a`. -/ +lemma singleton_le_toColex : (toColex {a} : Colex α) ≤ toColex s ↔ ∃ x ∈ s, a ≤ x := by + simp [toColex_le_toColex]; by_cases a ∈ s <;> aesop -section LinearOrder -variable [LinearOrder α] [LinearOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} - {s t u : Finset α} {a b : α} {r : ℕ} +/-- Colex is an extension of the base order. -/ +lemma singleton_le_singleton : (toColex {a} : Colex α) ≤ toColex {b} ↔ a ≤ b := by + simp [toColex_le_singleton, eq_comm] -instance : IsStrictTotalOrder (Colex α) (· < ·) where - irrefl := irrefl_of (· < ·) - trans s t u := by - rintro ⟨k₁, k₁z, notinA, inB⟩ ⟨k₂, k₂z, notinB, inC⟩ - obtain h | h := (ne_of_mem_of_not_mem inB notinB).lt_or_lt - · refine' ⟨k₂, fun x hx ↦ _, by rwa [k₁z h], inC⟩ - rw [←k₂z hx] - exact k₁z (h.trans hx) - · refine' ⟨k₁, fun x hx ↦ _, notinA, by rwa [←k₂z h]⟩ - rw [k₁z hx] - exact k₂z (h.trans hx) - trichotomous s t := by - classical - obtain rfl | hts := eq_or_ne t s - · simp - obtain ⟨k, hk, z⟩ := exists_max_image _ id (symmDiff_nonempty.2 $ ofColex_ne_ofColex.2 hts) - refine' (mem_symmDiff.1 hk).imp (fun hk => ⟨k, fun a ha ↦ _, hk.2, hk.1⟩) fun hk ↦ - Or.inr ⟨k, fun a ha ↦ _, hk.2, hk.1⟩ <;> - simpa [mem_symmDiff, not_or, iff_iff_implies_and_implies, and_comm, not_imp_not] - using not_imp_not.2 (z a) ha.not_le +/-- Colex is an extension of the base order. -/ +lemma singleton_lt_singleton : (toColex {a} : Colex α) < toColex {b} ↔ a < b := by + simp [toColex_lt_singleton] -instance instDecidableLT : @DecidableRel (Colex α) (· < ·) := fun s t ↦ - decidable_of_iff' - (∃ k ∈ ofColex t, - (∀ x ∈ ofColex s ∪ ofColex t, k < x → (x ∈ ofColex s ↔ x ∈ ofColex t)) ∧ k ∉ ofColex s) $ - exists_congr fun a ↦ by - simp only [mem_union, exists_prop, or_imp, @and_comm (_ ∈ ofColex t), and_assoc] - exact and_congr_left' $ forall_congr' $ by tauto +variable [DecidableEq α] -instance instLinearOrder : LinearOrder (Colex α) := linearOrderOfSTO (· < ·) +instance instDecidableEq : DecidableEq (Colex α) := fun s t ↦ + decidable_of_iff' (s.ofColex = t.ofColex) <| Colex.ext_iff _ _ -instance instBot : Bot (Colex α) where - bot := toColex ∅ +instance instDecidableLE [@DecidableRel α (· ≤ ·)] : @DecidableRel (Colex α) (· ≤ ·) := fun s t ↦ + decidable_of_iff' + (∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b) Iff.rfl -@[simp] lemma toColex_empty : toColex (∅ : Finset α) = ⊥ := rfl -@[simp] lemma ofColex_bot : ofColex (⊥ : Colex α) = ∅ := rfl +instance instDecidableLT [@DecidableRel α (· ≤ ·)] : @DecidableRel (Colex α) (· < ·) := + decidableLTOfDecidableLE -instance instOrderBot : OrderBot (Colex α) where - bot_le s := by - induction' s using Finset.Colex.rec with s - rw [le_def] - obtain rfl | hs := s.eq_empty_or_nonempty - · simp - refine' Or.inr ⟨max' _ hs, _, by simp, max'_mem _ _⟩ - simp only [max'_lt_iff, ofColex_bot, not_mem_empty, ofColex_toColex, false_iff] - exact fun x hs hx ↦ lt_irrefl _ $ hs _ hx +lemma le_iff_sdiff_subset_lowerClosure {s t : Colex α} : + s ≤ t ↔ (ofColex s : Set α) \ ofColex t ⊆ lowerClosure (ofColex t \ ofColex s : Set α) := by + simp [le_def, Set.subset_def, and_assoc] /-- The colexigraphic order is insensitive to removing elements. -/ lemma toColex_sdiff_le_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t := by - rw [le_iff_le_iff_lt_iff_lt, toColex_sdiff_lt_toColex_sdiff hut hus] + simp_rw [toColex_le_toColex, ←and_imp, ←and_assoc, ←mem_sdiff, sdiff_sdiff_sdiff_cancel_right hus, + sdiff_sdiff_sdiff_cancel_right hut] + +/-- The colexigraphic order is insensitive to removing elements. -/ +lemma toColex_sdiff_lt_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : + toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t := + lt_iff_lt_of_le_iff_le' (toColex_sdiff_le_toColex_sdiff hut hus) <| + toColex_sdiff_le_toColex_sdiff hus hut @[simp] lemma toColex_sdiff_le_toColex_sdiff' : toColex (s \ t) ≤ toColex (t \ s) ↔ toColex s ≤ toColex t := by - rw [le_iff_le_iff_lt_iff_lt, toColex_sdiff_lt_toColex_sdiff'] - -lemma colex_lt_of_ssubset (h : s ⊂ t) : toColex s < toColex t := by - rw [←toColex_sdiff_lt_toColex_sdiff', sdiff_eq_empty_iff_subset.2 h.1, toColex_empty, - bot_lt_iff_ne_bot, ←toColex_empty, toColex_ne_toColex] - simpa using h.not_subset - -/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as `⊆` is not a -linear order. -/ -lemma colex_le_of_subset (h : s ⊆ t) : toColex s ≤ toColex t := by - rw [←toColex_sdiff_le_toColex_sdiff', sdiff_eq_empty_iff_subset.2 h, toColex_empty]; exact bot_le + simpa using toColex_sdiff_le_toColex_sdiff (inter_subset_left s t) (inter_subset_right s t) -instance [Fintype α] : BoundedOrder (Colex α) where - top := toColex univ - le_top _x := colex_le_of_subset (subset_univ _) - -@[simp] lemma toColex_univ [Fintype α] : toColex (univ : Finset α) = ⊤ := rfl -@[simp] lemma ofColex_top [Fintype α] : ofColex (⊤ : Colex α) = univ := rfl - -/-- `s < {a}` in colex iff all elements of `s` are strictly less than `a`. -/ -lemma toColex_lt_singleton : toColex s < toColex {a} ↔ ∀ x ∈ s, x < a := by - simp only [toColex_lt_toColex, mem_singleton, ←and_assoc, exists_eq_right, ←not_le (a := a)] - refine ⟨fun t x hx hax ↦ ?_, fun h ↦ ⟨fun z hz ↦ ?_, by simpa using h a⟩⟩ - · obtain hax | rfl := hax.lt_or_eq - · exact hax.ne' $ (t.1 hax).1 hx - · exact t.2 hx - · exact ⟨fun i ↦ ((h _ i) hz.le).elim, fun i ↦ (hz.ne' i).elim⟩ - -/-- `{a} ≤ s` in colex iff `r` contains an element greated than or equal to `a`. -/ -lemma singleton_le_toColex : (toColex {a} : Colex α) ≤ toColex s ↔ ∃ x ∈ s, a ≤ x := by - simp only [←not_lt, toColex_lt_singleton, not_forall, exists_prop] - -/-- Colex is an extension of the base order. -/ -lemma singleton_lt_singleton : (toColex {a} : Colex α) < toColex {b} ↔ a < b := by - simp [toColex_lt_singleton] +@[simp] lemma toColex_sdiff_lt_toColex_sdiff' : + toColex (s \ t) < toColex (t \ s) ↔ toColex s < toColex t := by + simpa using toColex_sdiff_lt_toColex_sdiff (inter_subset_left s t) (inter_subset_right s t) -/-- Colex is an extension of the base order. -/ -lemma singleton_le_singleton : (toColex {a} : Colex α) ≤ toColex {b} ↔ a ≤ b := by - rw [le_iff_le_iff_lt_iff_lt, singleton_lt_singleton] +end PartialOrder -/-- If `s` is before `t` in colex, and everything in `t` is small, then everything in `s` is small. --/ -lemma forall_lt_mono (h₁ : toColex s ≤ toColex t) (h₂ : ∀ x ∈ t, x < a) : ∀ x ∈ s, x < a := by - obtain rfl | ⟨k, z, -, hk⟩ := toColex_le_toColex.1 h₁ - · assumption - · refine' fun x hx => lt_of_not_le fun h ↦ h.not_lt $ h₂ x _ - rwa [←z ((h₂ k hk).trans_le h)] +variable [LinearOrder α] [LinearOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} + {s t u : Finset α} {a b : α} {r : ℕ} -/-- Strictly monotone functions preserve the colex ordering. -/ -lemma toColex_image_lt_toColex_image (hf : StrictMono f) : - toColex (s.image f) < toColex (t.image f) ↔ toColex s < toColex t := by - simp only [toColex_lt_toColex, not_exists, mem_image, exists_prop, not_and] - constructor - · rintro ⟨k, z, q, k', _, rfl⟩ - exact ⟨k', fun x hx => by simpa [hf.injective.eq_iff] using z (hf hx), - fun t ↦ q _ t rfl, ‹k' ∈ t›⟩ - rintro ⟨k, z, ka, _⟩ - refine' ⟨f k, fun x hx ↦ _, _, k, ‹k ∈ t›, rfl⟩ - · constructor - all_goals - rintro ⟨x', hx', rfl⟩ - refine' ⟨x', _, rfl⟩ - first - | rwa [←z _] - | rwa [z _] - rwa [StrictMono.lt_iff_lt hf] at hx - · simp only [hf.injective, Function.Injective.eq_iff] - exact fun x hx ↦ ne_of_mem_of_not_mem hx ka +instance instLinearOrder : LinearOrder (Colex α) where + le_total s t := by + classical + obtain rfl | hts := eq_or_ne t s + · simp + have ⟨a, ha, hamax⟩ := exists_max_image _ id (symmDiff_nonempty.2 <| ofColex_ne_ofColex.2 hts) + simp_rw [mem_symmDiff] at ha hamax + exact ha.imp (fun ha b hbs hbt ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inr ⟨hbs, hbt⟩⟩) + (fun ha b hbt hbs ↦ ⟨a, ha.1, ha.2, hamax _ <| Or.inl ⟨hbt, hbs⟩⟩) + decidableLE := instDecidableLE + decidableLT := instDecidableLT + +private lemma max_mem_aux {s t : Colex α} (hst : s ≠ t) : (ofColex s ∆ ofColex t).Nonempty := by + simpa + +lemma toColex_lt_toColex_iff_exists_forall_lt : + toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a := by + rw [←not_le, toColex_le_toColex, not_forall] + simp only [not_forall, not_exists, not_and, not_le, exists_prop, exists_and_left] + +lemma lt_iff_exists_forall_lt {s t : Colex α} : + s < t ↔ ∃ a ∈ ofColex t, a ∉ ofColex s ∧ ∀ b ∈ ofColex s, b ∉ ofColex t → b < a := + toColex_lt_toColex_iff_exists_forall_lt + +lemma toColex_le_toColex_iff_max'_mem : + toColex s ≤ toColex t ↔ ∀ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t := by + refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩ + · set m := (s ∆ t).max' (symmDiff_nonempty.2 hst) + by_contra hmt + have hms : m ∈ s := by simpa [mem_symmDiff, hmt] using max'_mem _ <| symmDiff_nonempty.2 hst + have ⟨b, hbt, hbs, hmb⟩ := h hms hmt + exact lt_irrefl _ <| (max'_lt_iff _ _).1 (hmb.lt_of_ne <| ne_of_mem_of_not_mem hms hbs) _ <| + mem_symmDiff.2 <| Or.inr ⟨hbt, hbs⟩ + · have hst : s ≠ t := ne_of_mem_of_not_mem' has hat + refine ⟨_, h hst, ?_, le_max' _ _ <| mem_symmDiff.2 <| Or.inl ⟨has, hat⟩⟩ + simpa [mem_symmDiff, h hst] using max'_mem _ <| symmDiff_nonempty.2 hst + +lemma le_iff_max'_mem {s t : Colex α} : + s ≤ t ↔ ∀ h : s ≠ t, (ofColex s ∆ ofColex t).max' (max_mem_aux h) ∈ ofColex t := + toColex_le_toColex_iff_max'_mem.trans + ⟨fun h hst ↦ h <| ofColex_ne_ofColex.2 hst, fun h hst ↦ h <| ofColex_ne_ofColex.1 hst⟩ + +lemma toColex_lt_toColex_iff_max'_mem : + toColex s < toColex t ↔ ∃ hst : s ≠ t, (s ∆ t).max' (symmDiff_nonempty.2 hst) ∈ t := by + rw [lt_iff_le_and_ne, toColex_le_toColex_iff_max'_mem]; aesop + +lemma lt_iff_max'_mem {s t : Colex α} : + s < t ↔ ∃ h : s ≠ t, (ofColex s ∆ ofColex t).max' (max_mem_aux h) ∈ ofColex t := by + rw [lt_iff_le_and_ne, le_iff_max'_mem]; aesop /-- Strictly monotone functions preserve the colex ordering. -/ lemma toColex_image_le_toColex_image (hf : StrictMono f) : toColex (s.image f) ≤ toColex (t.image f) ↔ toColex s ≤ toColex t := by - rw [le_iff_le_iff_lt_iff_lt, toColex_image_lt_toColex_image hf] + simp [toColex_le_toColex, hf.le_iff_le, hf.injective.eq_iff] + +/-- Strictly monotone functions preserve the colex ordering. -/ +lemma toColex_image_lt_toColex_image (hf : StrictMono f) : + toColex (s.image f) < toColex (t.image f) ↔ toColex s < toColex t := + lt_iff_lt_of_le_iff_le <| toColex_image_le_toColex_image hf /-! ### Initial segments -/ @@ -297,13 +324,13 @@ lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) classical simp_rw [←sdiff_eq_empty_iff_subset, ←not_nonempty_iff_eq_empty] by_contra' h - obtain ⟨⟨s, hs⟩, t, ht⟩ := h + have ⟨⟨s, hs⟩, t, ht⟩ := h rw [mem_sdiff] at hs ht obtain hst | hst | hts := trichotomous_of (α := Colex α) (· < ·) (toColex s) (toColex t) - · exact hs.2 $ h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩ + · exact hs.2 <| h₂.2 ht.1 ⟨hst, h₁.1 hs.1⟩ · simp only [toColex.injEq] at hst - exact ht.2 $ hst ▸ hs.1 - · exact ht.2 $ h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩ + exact ht.2 <| hst ▸ hs.1 + · exact ht.2 <| h₁.2 hs.1 ⟨hts, h₂.1 ht.1⟩ variable [Fintype α] @@ -345,7 +372,6 @@ lemma isInitSeg_iff_exists_initSeg : rintro ⟨s, rfl, rfl⟩ exact ⟨isInitSeg_initSeg, initSeg_nonempty⟩ -end LinearOrder end Colex open Colex @@ -360,34 +386,23 @@ binary expansion. section Nat variable {s t : Finset ℕ} +private lemma aux : StrictMono (fun s : Colex ℕ ↦ ∑ k in ofColex s, 2 ^ k) := by + rintro ⟨s⟩ ⟨t⟩ hst + rw [toColex_lt_toColex_iff_exists_forall_lt] at hst + obtain ⟨a, hat, has, ha⟩ := hst + rw [←sum_sdiff_lt_sum_sdiff] + exact (Nat.sum_two_pow_lt <| by simpa).trans_le <| + single_le_sum (fun _ _ ↦ by positivity) <| mem_sdiff.2 ⟨hat, has⟩ + /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the binary expansion. -/ -lemma sum_two_pow_lt_iff_colex_lt : ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i ↔ toColex s < toColex t := by - have z : ∀ s t : Finset ℕ, toColex s < toColex t → ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i := by - intro s t - rw [←toColex_sdiff_lt_toColex_sdiff', toColex_lt_toColex] - rintro ⟨a, ha, has, hat⟩ - rw [←sdiff_union_inter s t] - conv_rhs => rw [←sdiff_union_inter t s] - rw [sum_union (disjoint_sdiff_inter _ _), sum_union (disjoint_sdiff_inter _ _), inter_comm, - add_lt_add_iff_right] - apply (@Nat.sum_two_pow_lt a (s \ t) _).trans_le - · apply single_le_sum (fun _ _ ↦ Nat.zero_le _) hat - intro x hx - refine' (ne_of_mem_of_not_mem hx has).lt_or_lt.resolve_right $ fun hax ↦ _ - have := (ha hax).1 hx - rw [mem_sdiff] at this hx - exact hx.2 this.1 - refine' ⟨fun h ↦ (lt_trichotomy (toColex s) $ toColex t).resolve_right fun h₁ ↦ - h₁.elim _ (not_lt_of_gt h ∘ z _ _), z s t⟩ - rw [toColex_inj] - rintro rfl - exact irrefl _ h +lemma sum_two_pow_le_iff_colex_le : ∑ k in s, 2 ^ k ≤ ∑ k in t, 2 ^ k ↔ toColex s ≤ toColex t := + aux.le_iff_le /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the binary expansion. -/ -lemma sum_two_pow_le_iff_colex_le : ∑ i in s, 2 ^ i ≤ ∑ i in t, 2 ^ i ↔ toColex s ≤ toColex t := by - rw [le_iff_le_iff_lt_iff_lt, sum_two_pow_lt_iff_colex_lt] +lemma sum_two_pow_lt_iff_colex_lt : ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i ↔ toColex s < toColex t := + aux.lt_iff_lt end Nat end Finset diff --git a/Mathlib/Data/Finset/Basic.lean b/Mathlib/Data/Finset/Basic.lean index 2d47e11309c0e..9c486509822ab 100644 --- a/Mathlib/Data/Finset/Basic.lean +++ b/Mathlib/Data/Finset/Basic.lean @@ -193,6 +193,9 @@ instance decidableMem [_h : DecidableEq α] (a : α) (s : Finset α) : Decidable Multiset.decidableMem _ _ #align finset.decidable_mem Finset.decidableMem +@[simp] lemma forall_mem_not_eq {s : Finset α} {a : α} : (∀ b ∈ s, ¬ a = b) ↔ a ∉ s := by aesop +@[simp] lemma forall_mem_not_eq' {s : Finset α} {a : α} : (∀ b ∈ s, ¬ b = a) ↔ a ∉ s := by aesop + /-! ### set coercion -/ --Porting note: new definition diff --git a/Mathlib/Order/BooleanAlgebra.lean b/Mathlib/Order/BooleanAlgebra.lean index 78f8b54bbacdf..b5f0b96f663ef 100644 --- a/Mathlib/Order/BooleanAlgebra.lean +++ b/Mathlib/Order/BooleanAlgebra.lean @@ -417,6 +417,15 @@ theorem sdiff_sdiff_sup_sdiff' : z \ (x \ y ⊔ y \ x) = z ⊓ x ⊓ y ⊔ z \ x _ = z ⊓ x ⊓ y ⊔ z \ x ⊓ z \ y := by ac_rfl #align sdiff_sdiff_sup_sdiff' sdiff_sdiff_sup_sdiff' +lemma sdiff_sdiff_sdiff_cancel_left (hca : z ≤ x) : (x \ y) \ (x \ z) = z \ y := + sdiff_sdiff_sdiff_le_sdiff.antisymm <| + (disjoint_sdiff_self_right.mono_left sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_right hca + +lemma sdiff_sdiff_sdiff_cancel_right (hcb : z ≤ y) : (x \ z) \ (y \ z) = x \ y := by + rw [le_antisymm_iff, sdiff_le_comm] + exact ⟨sdiff_sdiff_sdiff_le_sdiff, + (disjoint_sdiff_self_left.mono_right sdiff_le).le_sdiff_of_le_left <| sdiff_le_sdiff_left hcb⟩ + theorem inf_sdiff : (x ⊓ y) \ z = x \ z ⊓ y \ z := sdiff_unique (calc From 885858758a98b52457b131455a3bfbf64abdf988 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Sat, 21 Oct 2023 22:15:37 +0000 Subject: [PATCH 09/12] break long line --- Mathlib/Algebra/GeomSum.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index de5db4b7693ff..c69c940ed8c61 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -590,7 +590,7 @@ end Order lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : ∑ k in s, 2 ^ k < 2 ^ n := by calc - ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 <| hs _ hk + ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk _ = 2 ^ n - 1 := by simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one From 1b74cf94e00ff2781904627313a051818eaaf5f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 9 Nov 2023 19:20:22 +0000 Subject: [PATCH 10/12] Eric's suggestions --- Mathlib/Combinatorics/Colex.lean | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 6e8d84981dc6d..04df39eaf644b 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -19,11 +19,11 @@ The colex ordering likes to avoid large values: If the biggest element of `t` is elements of `s`, then `s < t`. In the special case of `ℕ`, it can be thought of as the "binary" ordering. That is, order `s` based -on `∑_{i ∈ s} 2^i`. It's defined here on `Finset α` for any linear order `α`. +on $∑_{i ∈ s} 2^i$. It's defined here on `Finset α` for any linear order `α`. In the context of the Kruskal-Katona theorem, we are interested in how colex behaves for sets of a fixed size. For example, for size 3, the colex order on ℕ starts -`123, 124, 134, 234, 125, 135, 235, 145, 245, 345, ...` +`012, 013, 023, 123, 014, 024, 124, 034, 134, 234, ...` ## Main statements @@ -69,19 +69,17 @@ namespace Finset /-- Type synonym of `Finset α` equipped with the colexicographic order rather than the inclusion order. -/ @[ext] -structure Colex (α) := toColex :: (ofColex : Finset α) +structure Colex (α) := + /-- `toColex` is the "identity" function between `Finset α` and `Finset.Colex α`. -/ + toColex :: + /-- `ofColex` is the "identity" function between `Finset.Colex α` and `Finset α`. -/ + (ofColex : Finset α) -- TODO: Why can't we export? --export Colex (toColex) open Colex -/-- `toColex` is the "identity" function between `Finset α` and `Finset.Colex α`. -/ -add_decl_doc toColex - -/-- `ofColex` is the "identity" function between `Finset.Colex α` and `Finset α`. -/ -add_decl_doc ofColex - instance : Inhabited (Colex α) := ⟨⟨∅⟩⟩ @[simp] lemma toColex_ofColex (s : Colex α) : toColex (ofColex s) = s := rfl @@ -100,8 +98,8 @@ section PartialOrder variable [PartialOrder α] [PartialOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)} {s t u : Finset α} {a b : α} -instance instLE : LE (Colex α) := - ⟨fun s t ↦ ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b⟩ +instance instLE : LE (Colex α) where + le s t := ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toColex u) (a : α) (has : a ∈ s) (hat : a ∉ t) : @@ -157,6 +155,14 @@ not form a linear order. -/ lemma toColex_strictMono : StrictMono (toColex : Finset α → Colex α) := toColex_mono.strictMono_of_injective toColex_injective +/-- If `s ⊆ t`, then `s ≤ t` in the colex order. Note the converse does not hold, as inclusion does +not form a linear order. -/ +lemma toColex_le_toColex_of_subset (h : s ⊆ t) : toColex s ≤ toColex t := toColex_mono h + +/-- If `s ⊂ t`, then `s < t` in the colex order. Note the converse does not hold, as inclusion does +not form a linear order. -/ +lemma toColex_lt_toColex_of_ssubset (h : s ⊂ t) : toColex s < toColex t := toColex_strictMono h + instance instOrderBot : OrderBot (Colex α) where bot := toColex ∅ bot_le s a ha := by cases ha @@ -222,13 +228,13 @@ lemma le_iff_sdiff_subset_lowerClosure {s t : Colex α} : s ≤ t ↔ (ofColex s : Set α) \ ofColex t ⊆ lowerClosure (ofColex t \ ofColex s : Set α) := by simp [le_def, Set.subset_def, and_assoc] -/-- The colexigraphic order is insensitive to removing elements. -/ +/-- The colexigraphic order is insensitive to removing the same elements from both sets. -/ lemma toColex_sdiff_le_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : toColex (s \ u) ≤ toColex (t \ u) ↔ toColex s ≤ toColex t := by simp_rw [toColex_le_toColex, ←and_imp, ←and_assoc, ←mem_sdiff, sdiff_sdiff_sdiff_cancel_right hus, sdiff_sdiff_sdiff_cancel_right hut] -/-- The colexigraphic order is insensitive to removing elements. -/ +/-- The colexigraphic order is insensitive to removing the same elements from both sets. -/ lemma toColex_sdiff_lt_toColex_sdiff (hus : u ⊆ s) (hut : u ⊆ t) : toColex (s \ u) < toColex (t \ u) ↔ toColex s < toColex t := lt_iff_lt_of_le_iff_le' (toColex_sdiff_le_toColex_sdiff hut hus) <| From 5ed0b1c49becfe46fff290b487cd4a0f54464fd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 20 Nov 2023 17:21:49 +0000 Subject: [PATCH 11/12] generalise to arbitrary base --- Mathlib/Algebra/GeomSum.lean | 22 +++++++++++----- Mathlib/Combinatorics/Colex.lean | 45 +++++++++++++++++++------------- 2 files changed, 42 insertions(+), 25 deletions(-) diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean index 38da7d8f299d3..99d2b0e0e9b84 100644 --- a/Mathlib/Algebra/GeomSum.lean +++ b/Mathlib/Algebra/GeomSum.lean @@ -585,12 +585,20 @@ theorem geom_sum_neg_iff [LinearOrderedRing α] (hn : n ≠ 0) : end Order +variable {m n : ℕ} {s : Finset ℕ} + +/-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of +`m ≥ 2` is less than `m ^ n`. -/ +lemma Nat.geomSum_eq (hm : 2 ≤ m) (n : ℕ) : + ∑ k in range n, m ^ k = (m ^ n - 1) / (m - 1) := by + refine (Nat.div_eq_of_eq_mul_left (tsub_pos_iff_lt.2 hm) $ tsub_eq_of_eq_add ?_).symm + simpa only [tsub_add_cancel_of_le $ one_le_two.trans hm, eq_comm] using geom_sum_mul_add (m - 1) n + /-- If all the elements of a finset of naturals are less than `n`, then the sum of their powers of -`2` is less than `2 ^ n`. -/ -lemma Nat.sum_two_pow_lt {n : ℕ} {s : Finset ℕ} (hs : ∀ k ∈ s, k < n) : - ∑ k in s, 2 ^ k < 2 ^ n := by +`m ≥ 2` is less than `m ^ n`. -/ +lemma Nat.geomSum_lt (hm : 2 ≤ m) (hs : ∀ k ∈ s, k < n) : ∑ k in s, m ^ k < m ^ n := calc - ∑ k in s, 2 ^ k ≤ ∑ k in range n, 2 ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk - _ = 2 ^ n - 1 := by - simp_rw [←one_add_one_eq_two, ←geom_sum_mul_add 1 n, mul_one, add_tsub_cancel_right] - _ < 2 ^ n := tsub_lt_self (by positivity) zero_lt_one + ∑ k in s, m ^ k ≤ ∑ k in range n, m ^ k := sum_le_sum_of_subset fun k hk ↦ mem_range.2 $ hs _ hk + _ = (m ^ n - 1) / (m - 1) := Nat.geomSum_eq hm _ + _ ≤ m ^ n - 1 := Nat.div_le_self _ _ + _ < m ^ n := tsub_lt_self (by positivity) zero_lt_one diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 04df39eaf644b..0e5c842e5f5cf 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -60,7 +60,7 @@ colex, colexicographic, binary open Finset Function open scoped BigOperators -#align nat.sum_two_pow_lt Nat.sum_two_pow_lt +#align nat.sum_two_pow_lt Nat.geomSum_lt variable {α β : Type*} @@ -101,11 +101,12 @@ variable [PartialOrder α] [PartialOrder β] {f : α → β} {𝒜 𝒜₁ 𝒜 instance instLE : LE (Colex α) where le s t := ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b +-- TODO: This lemma is weirdly useful given how strange its statement is. +-- Is there a nicer statement? Should this lemma be made public? private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toColex u) - (a : α) (has : a ∈ s) (hat : a ∉ t) : - ∃ b : α, b ∈ u ∧ b ∉ s ∧ a ≤ b := by + (has : a ∈ s) (hat : a ∉ t) : ∃ b, b ∈ u ∧ b ∉ s ∧ a ≤ b := by classical - let s' : Finset α := s.filter (fun a' => a' ∉ t ∧ a ≤ a') + let s' : Finset α := s.filter fun b ↦ b ∉ t ∧ a ≤ b have ⟨b, hb, hbmax⟩ := exists_maximal s' ⟨a, by simp [has, hat]⟩ simp only [mem_filter, and_imp] at hb hbmax have ⟨c, hct, hcs, hbc⟩ := hst hb.1 hb.2.1 @@ -119,7 +120,7 @@ private lemma trans_aux (hst : toColex s ≤ toColex t) (htu : toColex t ≤ toC private lemma antisymm_aux (hst : toColex s ≤ toColex t) (hts : toColex t ≤ toColex s) : s ⊆ t := by intro a has by_contra' hat - have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts a has hat + have ⟨_b, hb₁, hb₂, _⟩ := trans_aux hst hts has hat exact hb₂ hb₁ instance instPartialOrder : PartialOrder (Colex α) where @@ -129,10 +130,10 @@ instance instPartialOrder : PartialOrder (Colex α) where by_cases hat : a ∈ ofColex t · have ⟨b, hbu, hbt, hab⟩ := htu hat hau by_cases hbs : b ∈ ofColex s - · have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu b hbs hbt + · have ⟨c, hcu, hcs, hbc⟩ := trans_aux hst htu hbs hbt exact ⟨c, hcu, hcs, hab.trans hbc⟩ · exact ⟨b, hbu, hbs, hab⟩ - · exact trans_aux hst htu _ has hat + · exact trans_aux hst htu has hat lemma le_def {s t : Colex α} : s ≤ t ↔ ∀ ⦃a⦄, a ∈ ofColex s → a ∉ ofColex t → ∃ b, b ∈ ofColex t ∧ b ∉ ofColex s ∧ a ≤ b := @@ -313,6 +314,10 @@ lemma toColex_image_lt_toColex_image (hf : StrictMono f) : toColex (s.image f) < toColex (t.image f) ↔ toColex s < toColex t := lt_iff_lt_of_le_iff_le <| toColex_image_le_toColex_image hf +lemma toColex_image_ofColex_strictMono (hf : StrictMono f) : + StrictMono fun s ↦ toColex $ image f $ ofColex s := + fun _s _t ↦ (toColex_image_lt_toColex_image hf).2 + /-! ### Initial segments -/ /-- `𝒜` is an initial segment of the colexigraphic order on sets of `r`, and that if `t` is below @@ -340,8 +345,8 @@ lemma IsInitSeg.total (h₁ : IsInitSeg 𝒜₁ r) (h₂ : IsInitSeg 𝒜₂ r) variable [Fintype α] -/-- Gives all sets up to `s` with the same size as it: this is equivalent to -being an initial segment of colex. -/ +/-- The initial segment of the colexicographic order on sets with `s.card` elements and ending at +`s`. -/ def initSeg (s : Finset α) : Finset (Finset α) := univ.filter fun t ↦ s.card = t.card ∧ toColex t ≤ toColex s @@ -371,7 +376,7 @@ lemma IsInitSeg.exists_initSeg (h𝒜 : IsInitSeg 𝒜 r) (h𝒜₀ : 𝒜.Nonem · rwa [toColex_inj.1 p] · exact h𝒜.2 hs ⟨p, cards ▸ h𝒜.1 hs⟩ -/-- Being a nonempty initial segment of colex if equivalent to being an `initSeg`. -/ +/-- Being a nonempty initial segment of colex is equivalent to being an `initSeg`. -/ lemma isInitSeg_iff_exists_initSeg : IsInitSeg 𝒜 r ∧ 𝒜.Nonempty ↔ ∃ s : Finset α, s.card = r ∧ 𝒜 = initSeg s := by refine ⟨fun h𝒜 ↦ h𝒜.1.exists_initSeg h𝒜.2, ?_⟩ @@ -390,25 +395,29 @@ binary expansion. -/ section Nat -variable {s t : Finset ℕ} +variable {s t : Finset ℕ} {n : ℕ} -private lemma aux : StrictMono (fun s : Colex ℕ ↦ ∑ k in ofColex s, 2 ^ k) := by +lemma geomSum_ofColex_strictMono (hn : 2 ≤ n) : StrictMono fun s ↦ ∑ k in ofColex s, n ^ k := by rintro ⟨s⟩ ⟨t⟩ hst rw [toColex_lt_toColex_iff_exists_forall_lt] at hst obtain ⟨a, hat, has, ha⟩ := hst rw [←sum_sdiff_lt_sum_sdiff] - exact (Nat.sum_two_pow_lt <| by simpa).trans_le <| - single_le_sum (fun _ _ ↦ by positivity) <| mem_sdiff.2 ⟨hat, has⟩ + exact (Nat.geomSum_lt hn $ by simpa).trans_le <| single_le_sum (fun _ _ ↦ by positivity) <| + mem_sdiff.2 ⟨hat, has⟩ /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the binary expansion. -/ -lemma sum_two_pow_le_iff_colex_le : ∑ k in s, 2 ^ k ≤ ∑ k in t, 2 ^ k ↔ toColex s ≤ toColex t := - aux.le_iff_le +lemma geomSum_le_geomSum_iff_toColex_le_toColex (hn : 2 ≤ n) : + ∑ k in s, n ^ k ≤ ∑ k in t, n ^ k ↔ toColex s ≤ toColex t := + (geomSum_ofColex_strictMono hn).le_iff_le /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order induced by the binary expansion. -/ -lemma sum_two_pow_lt_iff_colex_lt : ∑ i in s, 2 ^ i < ∑ i in t, 2 ^ i ↔ toColex s < toColex t := - aux.lt_iff_lt +lemma geomSum_lt_geomSum_iff_toColex_lt_toColex (hn : 2 ≤ n) : + ∑ i in s, n ^ i < ∑ i in t, n ^ i ↔ toColex s < toColex t := + (geomSum_ofColex_strictMono hn).lt_iff_lt + +-- TODO: Package the above as an order isomorphism `Colex ℕ ≃o ℕ` end Nat end Finset From 72918fd497f987331f078a45eafe845908336c33 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 24 Nov 2023 19:57:15 +0000 Subject: [PATCH 12/12] update module docs --- Mathlib/Combinatorics/Colex.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean index 0e5c842e5f5cf..0edc2182ed773 100644 --- a/Mathlib/Combinatorics/Colex.lean +++ b/Mathlib/Combinatorics/Colex.lean @@ -31,9 +31,9 @@ fixed size. For example, for size 3, the colex order on ℕ starts * `Finset.Colex.forall_lt_mono`: if `s < t` in colex, and everything in `t` is `< a`, then everything in `s` is `< a`. This confirms the idea that an enumeration under colex will exhaust all sets using elements `< a` before allowing `a` to be included. -* `Finset.toColex_image_lt_toColex_image`: Strictly monotone functions preserve colex. -* `Finset.sum_two_pow_le_iff_colex_le`: colex for α = ℕ is the same as binary - (this also proves binary expansions are unique) +* `Finset.toColex_image_le_toColex_image`: Strictly monotone functions preserve colex. +* `Finset.geomSum_le_geomSum_iff_toColex_le_toColex`: Colex for α = ℕ is the same as binary. + This also proves binary expansions are unique. ## See also @@ -391,7 +391,7 @@ open Colex ### Colex on `ℕ` The colexicographic order agrees with the order induced by interpreting a set of naturals as a -binary expansion. +`n`-ary expansion. -/ section Nat @@ -406,18 +406,18 @@ lemma geomSum_ofColex_strictMono (hn : 2 ≤ n) : StrictMono fun s ↦ ∑ k in mem_sdiff.2 ⟨hat, has⟩ /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order -induced by the binary expansion. -/ +induced by the `n`-ary expansion. -/ lemma geomSum_le_geomSum_iff_toColex_le_toColex (hn : 2 ≤ n) : ∑ k in s, n ^ k ≤ ∑ k in t, n ^ k ↔ toColex s ≤ toColex t := (geomSum_ofColex_strictMono hn).le_iff_le /-- For finsets of naturals of naturals, the colexicographic order is equivalent to the order -induced by the binary expansion. -/ +induced by the `n`-ary expansion. -/ lemma geomSum_lt_geomSum_iff_toColex_lt_toColex (hn : 2 ≤ n) : ∑ i in s, n ^ i < ∑ i in t, n ^ i ↔ toColex s < toColex t := (geomSum_ofColex_strictMono hn).lt_iff_lt --- TODO: Package the above as an order isomorphism `Colex ℕ ≃o ℕ` +-- TODO: Package the above in the `n = 2` case as an order isomorphism `Colex ℕ ≃o ℕ` end Nat end Finset