PlainCombi: LYM inequality using the Katona circle method (#42)

Co-authored-by: Yaël Dillies <[email protected]>

Author: ctchou

LeanCamCombi.lean

@@ -10,12 +10,18 @@ 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
 import LeanCamCombi.PlainCombi.OrderShatter
+import LeanCamCombi.PlainCombi.ProbLYM
 import LeanCamCombi.PlainCombi.VanDenBergKesten
 import LeanCamCombi.StableCombi.AddSet
 import LeanCamCombi.StableCombi.Formula

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/Fintype/Card.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Fintype.Card
+
+namespace Fintype
+variable {α : Type*} {p : α → Prop}
+
+-- TODO: Replace `card_subtype_le`
+lemma card_subtype_le' [Fintype α] [Fintype {a // p a}] : card {a // p a} ≤ card α := by
+  classical convert card_subtype_le _; infer_instance
+
+end Fintype

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

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2024 Ching-Tsun Chou, Chris Wong. All rights reserved.
+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.Mathlib.Data.Nat.Choose.Cast
+import Mathlib.Data.Finset.Density
+import Mathlib.Data.Fintype.Prod
+import Mathlib.Data.Fintype.Perm
+
+/-!
+# The Katona circle method
+
+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.
+-/
+
+open Fintype Finset Nat
+
+variable {α : Type*} [Fintype α]
+
+variable (α) in
+/-- A numbering of a fintype `α` is a bijection between `α` and `Fin (card α)`. -/
+abbrev Numbering : Type _ := α ≃ Fin (card α)
+
+@[simp] lemma Fintype.card_numbering [DecidableEq α] : card (Numbering α) = (card α)! :=
+  card_equiv (equivFin _)
+
+namespace Numbering
+variable {f : Numbering α} {s t : Finset α}
+
+/-- `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
+
+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
+
+variable [DecidableEq α]
+
+instance : Decidable (IsPrefix f s) := by unfold IsPrefix; infer_instance
+
+/-- 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

LeanCamCombi/PlainCombi/ProbLYM.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2024 Ching-Tsun Chou, Chris Wong. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou, Chris Wong
+-/
+import LeanCamCombi.Mathlib.Algebra.BigOperators.Field
+import LeanCamCombi.PlainCombi.KatonaCircle
+
+/-!
+# The LYM inequality using probability theory
+
+This file proves the LYM inequality using (very elementary) probability theory.
+
+
+
+## References
+
+This proof formalizes Section 1.2 of Prof. Yufei Zhao's lecture notes for MIT 18.226:
+
+<https://yufeizhao.com/pm/probmethod_notes.pdf>
+
+A video of Prof. Zhao's lecture is available on YouTube:
+
+<https://youtu.be/exBXHYl4po8>
+
+The proof of Theorem 1.10, Lecture 3 in the Cambridge lecture notes on combinatorics:
+
+<https://github.com/YaelDillies/maths-notes/blob/master/combinatorics.pdf>
+
+is basically the same proof, except without using probability theory.
+-/
+
+open Finset Fintype Numbering
+
+variable {α : Type*} [Fintype α] {𝒜 : Finset (Finset α)}
+
+/-- The **Lubell-Yamamoto-Meshalkin inequality**, proved using the Katona circle method. -/
+theorem LYM_inequality (h𝒜 : IsAntichain (· ⊆ ·) 𝒜.toSet) :
+    ∑ s ∈ 𝒜, ((card α).choose #s : ℚ≥0)⁻¹ ≤ 1 := by
+  classical
+  calc
+    _ = ∑ s ∈ 𝒜, (prefixed s).dens := by simp
+    _ = (𝒜.biUnion prefixed).dens := by
+      rw [dens_biUnion]
+      exact fun s hs t ht hst ↦ disjoint_prefixed_prefixed (h𝒜 hs ht hst) (h𝒜 ht hs hst.symm)
+    _ ≤ 1 := dens_le_one