Final cleanup

Author: YaelDillies

LeanCamCombi.lean

@@ -10,10 +10,13 @@ import LeanCamCombi.GrowthInGroups.Lecture1
 import LeanCamCombi.GrowthInGroups.Lecture2
 import LeanCamCombi.GrowthInGroups.Lecture3
 import LeanCamCombi.GrowthInGroups.Lecture4
+import LeanCamCombi.Mathlib.Algebra.BigOperators.Field
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
+import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
 import LeanCamCombi.Mathlib.Data.Fintype.Card
+import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.PlainCombi.KatonaCircle
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/Mathlib/Algebra/BigOperators/Field.lean

@@ -0,0 +1,28 @@
+import Mathlib.Algebra.BigOperators.Field
+import Mathlib.Data.Finset.Density
+
+namespace Finset
+variable {α β : Type*} [Fintype β]
+
+@[simp]
+lemma dens_disjiUnion (s : Finset α) (t : α → Finset β) (h) :
+    (s.disjiUnion t h).dens = ∑ a ∈ s, (t a).dens := by simp [dens, sum_div]
+
+variable {s : Finset α} {t : α → Finset β}
+
+lemma dens_biUnion [DecidableEq β] (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) :
+    (s.biUnion t).dens = ∑ u ∈ s, (t u).dens := by
+  simp [dens, card_biUnion h, sum_div]
+
+lemma dens_biUnion_le [DecidableEq β] : (s.biUnion t).dens ≤ ∑ a ∈ s, (t a).dens := by
+  simp [dens, ← sum_div]; gcongr; positivity; norm_cast; exact card_biUnion_le
+
+lemma dens_eq_sum_dens_fiberwise [DecidableEq α] {f : β → α} {t : Finset β} (h : ∀ x ∈ t, f x ∈ s) :
+    t.dens = ∑ a ∈ s, {b ∈ t | f b = a}.dens := by
+  simp [dens, ← sum_div, card_eq_sum_card_fiberwise h]
+
+lemma dens_eq_sum_dens_image [DecidableEq α] (f : β → α) (t : Finset β) :
+    t.dens = ∑ a ∈ t.image f, {b ∈ t | f b = a}.dens :=
+  dens_eq_sum_dens_fiberwise fun _ ↦ mem_image_of_mem _
+
+end Finset

LeanCamCombi/Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -0,0 +1,8 @@
+import Mathlib.Combinatorics.SetFamily.LYM
+
+/-!
+# TODO
+
+* Use semantic naming convention instead of symbol-reading
+* Add the `∑ s ∈ 𝒜, ((card α).choose #s)⁻¹ ≤ 1` variant
+-/

LeanCamCombi/Mathlib/Data/Nat/Choose/Cast.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Data.Nat.Choose.Basic
+import Mathlib.Data.Nat.Factorial.Cast
+
+/-!
+# TODO
+
+Replace
+-/
+
+
+open Nat
+
+variable (K : Type*) [DivisionSemiring K] [CharZero K]
+
+namespace Nat
+
+theorem cast_choose' {a b : ℕ} (h : a ≤ b) : (b.choose a : K) = b ! / (a ! * (b - a)!) := by
+  have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_ne_zero _)
+  rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
+  rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
+
+theorem cast_add_choose' {a b : ℕ} : ((a + b).choose a : K) = (a + b)! / (a ! * b !) := by
+  rw [cast_choose' K (_root_.le_add_right le_rfl), add_tsub_cancel_left]
+
+theorem cast_choose_eq_ascPochhammer_div' (a b : ℕ) :
+    (a.choose b : K) = (ascPochhammer K b).eval ↑(a - (b - 1)) / b ! := by
+  rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul,
+    mul_comm, ← descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
+
+end Nat

LeanCamCombi/PlainCombi/KatonaCircle.lean

@@ -4,100 +4,118 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Chris Wong
 -/
 import LeanCamCombi.Mathlib.Data.Fintype.Card
-import LeanCamCombi.PlainCombi.ProbLYM
-import Mathlib.Probability.UniformOn
+import LeanCamCombi.Mathlib.Data.Nat.Choose.Cast
+import Mathlib.Data.Finset.Density
+import Mathlib.Data.Fintype.Prod
+import Mathlib.Data.Fintype.Perm
 
 /-!
-# The LYM inequality using probability theory
+# The Katona circle method
 
-This file proves the LYM inequality using (very elementary) probability theory.
+This file provides tooling to use the Katona circle method, which is double-counting ways to order
+`n` elements on a circle under some condition.
+-/
 
-## References
+open Fintype Finset Nat
 
-This proof formalizes Section 1.2 of Prof. Yufei Zhao's lecture notes for MIT 18.226:
+variable {α : Type*} [Fintype α]
 
-<https://yufeizhao.com/pm/probmethod_notes.pdf>
+variable (α) in
+/-- A numbering of a fintype `α` is a bijection between `α` and `Fin (card α)`. -/
+abbrev Numbering : Type _ := α ≃ Fin (card α)
 
-A video of Prof. Zhao's lecture is available on YouTube:
+@[simp] lemma Fintype.card_numbering [DecidableEq α] : card (Numbering α) = (card α)! :=
+  card_equiv (equivFin _)
 
-<https://youtu.be/exBXHYl4po8>
+namespace Numbering
+variable {f : Numbering α} {s t : Finset α}
 
-The proof of Theorem 1.10, Lecture 3 in the Cambridge lecture notes on combinatorics:
+/-- `IsPrefix f s` means that the elements of `s` precede the elements of `sᶜ`
+in the numbering `f`. -/
+def IsPrefix (f : Numbering α) (s : Finset α) := ∀ x, x ∈ s ↔ f x < #s
 
-<https://github.com/YaelDillies/maths-notes/blob/master/combinatorics.pdf>
+lemma IsPrefix.subset_of_card_le_card (hs : IsPrefix f s) (ht : IsPrefix f t) (hst : #s ≤ #t) :
+    s ⊆ t := fun a ha ↦ (ht a).mpr <| ((hs a).mp ha).trans_le hst
 
-is basically the same proof, except without using probability theory.
--/
+variable [DecidableEq α]
+
+instance : Decidable (IsPrefix f s) := by unfold IsPrefix; infer_instance
 
-open BigOperators Fintype Finset Set MeasureTheory ProbabilityTheory
-open MeasureTheory.Measure
-open scoped ENNReal
-
-noncomputable section
-
-private lemma auxLemma {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
-    (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
-  -- The following proof is due to Aaron Liu.
-  subst heq
-  have hm : m ≠ 0 := by rintro rfl ; simp at hn
-  have hk : k ≠ 0 := by rintro rfl ; simp at hn
-  refine (ENNReal.toReal_eq_toReal ?_ ?_).mp ?_
-  · intro h
-    apply_fun ENNReal.toReal at h
-    simp [hm, hk] at h
-  · intro h
-    apply_fun ENNReal.toReal at h
-    simp [hk] at h
-  · field_simp
-    ring
-
-variable {α : Type*} [Fintype α] [DecidableEq α]
-
-instance : MeasurableSpace (Numbering α) := ⊤
-
-theorem count_PrefixedNumbering (s : Finset α) :
-    count (PrefixedNumbering s).toSet = ↑((#s).factorial * (card α - #s).factorial) := by
-  rw [← card_PrefixedNumbering s, count_apply_finset]
-
-theorem prob_PrefixedNumbering (s : Finset α) :
-    uniformOn Set.univ (PrefixedNumbering s).toSet = 1 / (card α).choose #s := by
-  rw [uniformOn_univ, count_PrefixedNumbering s, card_Numbering]
-  apply auxLemma (Nat.factorial_pos (card α))
-  rw [← mul_assoc]
-  exact Nat.choose_mul_factorial_mul_factorial (Finset.card_le_univ s)
-
-theorem disj_PrefixedNumbering {s t : Finset α} (h_st : ¬ s ⊆ t) (h_ts : ¬ t ⊆ s) :
-    Disjoint (PrefixedNumbering s).toSet (PrefixedNumbering t).toSet := by
-  refine Set.disjoint_iff.mpr ?_
-  intro p
-  simp only [mem_inter_iff, Finset.mem_coe, mem_empty_iff_false, imp_false, not_and]
-  simp [PrefixedNumbering]
-  intro h_s h_t
-  rcases Nat.le_total #s t.card with h_st' | h_ts'
-  · exact h_st (subset_IsPrefix_IsPrefix h_s h_t h_st')
-  · exact h_ts (subset_IsPrefix_IsPrefix h_t h_s h_ts')
-
-variable {𝓐 : Finset (Finset α)}
-
-theorem prob_biUnion_antichain (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
-    uniformOn Set.univ (⋃ s ∈ 𝓐, (PrefixedNumbering s).toSet) =
-    ∑ s ∈ 𝓐, uniformOn Set.univ (PrefixedNumbering s).toSet := by
-  have hd : 𝓐.toSet.PairwiseDisjoint (fun s ↦ (PrefixedNumbering s).toSet) := by
-    intro s h_s t h_t h_ne
-    simp only [Function.onFun]
-    have h_st := h𝓐 h_s h_t h_ne
-    have h_ts := h𝓐 h_t h_s h_ne.symm
-    exact disj_PrefixedNumbering h_st h_ts
-  have hm : ∀ s ∈ 𝓐, MeasurableSet (PrefixedNumbering s).toSet := by
-    intro s h_s ; exact trivial
-  rw [measure_biUnion_finset hd hm (μ := uniformOn Set.univ)]
-
-theorem LYM_inequality (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
-    ∑ s ∈ 𝓐, ((1 : ENNReal) / (card α).choose #s) ≤ 1 := by
-  have h1 s (hs : s ∈ 𝓐) :
-      (1 : ENNReal) / (card α).choose #s = uniformOn Set.univ (PrefixedNumbering s).toSet := by
-    rw [prob_PrefixedNumbering]
-  rw [Finset.sum_congr (rfl : 𝓐 = 𝓐) h1, ← prob_biUnion_antichain h𝓐]
-  exact prob_le_one
-
-end
+/-- The set of numberings of which `s` is a prefix. -/
+def prefixed (s : Finset α) : Finset (Numbering α) := {f | IsPrefix f s}
+
+@[simp] lemma mem_prefixed : f ∈ prefixed s ↔ IsPrefix f s := by simp [prefixed]
+
+/-- Decompose a numbering of which `s` is a prefix into a numbering of `s` and a numbering on `sᶜ`.
+-/
+def prefixedEquiv (s : Finset α) : prefixed s ≃ Numbering s × Numbering ↑(sᶜ) where
+  toFun f :=
+    { fst.toFun x := ⟨f.1 x, by simp [← mem_prefixed.1 f.2 x]⟩
+      fst.invFun n :=
+        ⟨f.1.symm ⟨n, n.2.trans_le <| by simpa using s.card_le_univ⟩, by
+          rw [mem_prefixed.1 f.2]; simpa using n.2⟩
+      fst.left_inv x := by simp
+      fst.right_inv n := by simp
+      snd.toFun x := ⟨f.1 x - #s, by
+        have := (mem_prefixed.1 f.2 x).not.1 (Finset.mem_compl.1 x.2)
+        simp at this ⊢
+        omega⟩
+      snd.invFun n :=
+        ⟨f.1.symm ⟨n + #s, Nat.add_lt_of_lt_sub <| by simpa using n.2⟩, by
+          rw [s.mem_compl, mem_prefixed.1 f.2]; simp⟩
+      snd.left_inv := by
+        rintro ⟨x, hx⟩
+        rw [s.mem_compl, mem_prefixed.1 f.2, not_lt] at hx
+        simp [Nat.sub_add_cancel hx]
+      snd.right_inv := by rintro ⟨n, hn⟩; simp }
+  invFun := fun (g, g') ↦
+    { val.toFun x :=
+        if hx : x ∈ s then
+          g ⟨x, hx⟩ |>.castLE Fintype.card_subtype_le'
+        else
+          g' ⟨x, by simpa⟩ |>.addNat #s |>.cast (by simp [card_le_univ])
+      val.invFun n :=
+        if hn : n < #s then
+          g.symm ⟨n, by simpa using hn⟩
+        else
+          g'.symm ⟨n - #s, by simp; omega⟩
+      val.left_inv x := by
+        by_cases hx : x ∈ s
+        · have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
+          simp [hx, this]
+        · simp [hx, Equiv.symm_apply_eq]
+      val.right_inv n := by
+        obtain hns | hsn := lt_or_le n.1 #s
+        · simp [hns]
+        · simp [hsn.not_lt, hsn, dif_neg (mem_compl.1 <| Subtype.prop _), Fin.ext_iff,
+            Fintype.card_subtype_le']
+      property := mem_prefixed.2 fun x ↦ by
+        constructor
+        · intro hx
+          simpa [hx, -Fin.is_lt] using (g _).is_lt
+        · by_cases hx : x ∈ s <;> simp [hx] }
+  left_inv f := by
+    ext x
+    by_cases hx : x ∈ s
+    · simp [hx]
+    · rw [mem_prefixed.1 f.2, not_lt] at hx
+      simp [hx]
+  right_inv g := by simp +contextual [Prod.ext_iff, DFunLike.ext_iff]
+
+lemma card_prefixed (s : Finset α) : #(prefixed s) = (#s)! * (card α - #s)! := by
+  simpa [-mem_prefixed] using Fintype.card_congr (prefixedEquiv s)
+
+@[simp]
+lemma dens_prefixed (s : Finset α) : (prefixed s).dens = ((card α).choose #s : ℚ≥0)⁻¹ := by
+  simp [dens, card_prefixed, Nat.cast_choose' _ s.card_le_univ]
+
+-- TODO: This can be strengthened to an iff
+lemma disjoint_prefixed_prefixed (hst : ¬ s ⊆ t) (hts : ¬ t ⊆ s) :
+    Disjoint (prefixed s) (prefixed t) := by
+  simp only [Finset.disjoint_left, mem_prefixed]
+  intro f hs ht
+  obtain hst' | hts' := Nat.le_total #s #t
+  · exact hst <| hs.subset_of_card_le_card ht hst'
+  · exact hts <| ht.subset_of_card_le_card hs hts'
+
+end Numbering