Don't use NumberingOn. Move to under PlainCombi

Author: YaelDillies

LeanCamCombi.lean

@@ -13,9 +13,11 @@ import LeanCamCombi.GrowthInGroups.Lecture4
 import LeanCamCombi.Mathlib.Combinatorics.Additive.ApproximateSubgroup
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
+import LeanCamCombi.Mathlib.Data.Fintype.Card
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 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/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/ProbLYM.lean LeanCamCombi/PlainCombi/ProbLYM.leanLeanCamCombi/ProbLYM.lean renamed to LeanCamCombi/PlainCombi/ProbLYM.lean

@@ -3,7 +3,7 @@ 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 Mathlib.Data.Fintype.Perm
 import Mathlib.Probability.UniformOn
 
@@ -42,87 +42,67 @@ in mathlib because we need the special property `set_prefix_subset` below. -/
 @[reducible]
 def Numbering (α : Type*) [Fintype α] := α ≃ Fin (card α)
 
-@[reducible]
-def NumberingOn {α : Type*} (s : Finset α) := {x // x ∈ s} ≃ Fin s.card
-
 variable {α : Type*} [Fintype α] [DecidableEq α]
 
 theorem card_Numbering : card (Numbering α) = (card α).factorial := by
   exact Fintype.card_equiv (Fintype.equivFinOfCardEq rfl)
 
-omit [Fintype α] in
-theorem card_NumberingOn (s : Finset α) : card (NumberingOn s) = s.card.factorial := by
-  simp only [NumberingOn]
-  have h1 : card {x // x ∈ s} = card (Fin s.card) := by simp
-  have h2 : {x // x ∈ s} ≃ Fin s.card := by exact Fintype.equivOfCardEq h1
-  simp [Fintype.card_equiv h2]
-
 /-- `IsPrefix s f` means that the elements of `s` precede the elements of `sᶜ`
 in the numbering `f`. -/
 def IsPrefix (s : Finset α) (f : Numbering α) :=
-  ∀ x, x ∈ s ↔ f x < s.card
+  ∀ x, x ∈ s ↔ f x < #s
 
 omit [DecidableEq α] in
 theorem subset_IsPrefix_IsPrefix {s1 s2 : Finset α} {f : Numbering α}
   (h_s1 : IsPrefix s1 f) (h_s2 : IsPrefix s2 f) (h_card : s1.card ≤ s2.card) : s1 ⊆ s2 := by
   intro a h_as1
   exact (h_s2 a).mpr (lt_of_lt_of_le ((h_s1 a).mp h_as1) h_card)
 
-def equiv_IsPrefix_NumberingOn2 (s : Finset α) : {f // IsPrefix s f} ≃ NumberingOn s × NumberingOn sᶜ where
+def equiv_IsPrefix_Numbering2 (s : Finset α) :
+    {f // IsPrefix s f} ≃ Numbering s × Numbering ↑(sᶜ) where
   toFun := fun ⟨f, hf⟩ ↦
-    ({
-      toFun := fun ⟨x, hx⟩ ↦ ⟨f x, by rwa [← hf x]⟩
-      invFun := fun ⟨n, hn⟩ ↦ ⟨f.symm ⟨n, by have := s.card_le_univ; omega⟩, by rw [hf]; simpa⟩
-      left_inv := by rintro ⟨x, hx⟩; simp
-      right_inv := by rintro ⟨n, hn⟩; simp
-    },
-    {
-      toFun := fun ⟨x, hx⟩ ↦ ⟨f x - s.card, by
-        rw [s.mem_compl, hf] at hx
-        rw [s.card_compl]
-        exact Nat.sub_lt_sub_right (by omega) (by omega)
-      ⟩
-      invFun := fun ⟨n, hn⟩ ↦ ⟨f.symm ⟨n + s.card, by rw [s.card_compl] at hn; omega⟩,
-                               by rw [s.mem_compl, hf]; simp⟩
-      left_inv := by
+    { fst.toFun x := ⟨f x, by simp [← hf x]⟩
+      fst.invFun n :=
+        ⟨f.symm ⟨n, n.2.trans_le <| by simpa using s.card_le_univ⟩, by rw [hf]; simpa using n.2⟩
+      fst.left_inv x := by simp
+      fst.right_inv n := by simp
+      snd.toFun x := ⟨f x - #s, by
+        have := (hf x).not.1 (Finset.mem_compl.1 x.2)
+        simp at this ⊢
+        omega⟩
+      snd.invFun n :=
+        ⟨f.symm ⟨n + #s, Nat.add_lt_of_lt_sub <| by simpa using n.2⟩, by rw [s.mem_compl, hf]; simp⟩
+      snd.left_inv := by
         rintro ⟨x, hx⟩
         rw [s.mem_compl, hf, not_lt] at hx
         simp [Nat.sub_add_cancel hx]
-      right_inv := by rintro ⟨n, hn⟩; simp
-    })
-  invFun := fun (g, g') ↦ ⟨
-    {
-      toFun := fun x ↦
+      snd.right_inv := by rintro ⟨n, hn⟩; simp }
+  invFun := fun (g, g') ↦
+    { val.toFun x :=
         if hx : x ∈ s then
-          g ⟨x, hx⟩ |>.castLE s.card_le_univ
+          g ⟨x, hx⟩ |>.castLE Fintype.card_subtype_le'
         else
-          g' ⟨x, by simpa⟩ |>.addNat s.card |>.cast (by simp)
-      invFun := fun ⟨n, hn⟩ ↦
-        if hn' : n < s.card then
-          g.symm ⟨n, hn'⟩
+          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.card, by rw [s.card_compl]; omega⟩
-      left_inv := by intro x; by_cases hx : x ∈ s <;> simp [hx]
-      right_inv := by
-        rintro ⟨n, hn⟩
-        by_cases hn' : n < s.card
-        · simp [hn']
-        · simp [hn']
-          split_ifs
-          · rename_i h
-            have : ∀ x, ↑(g'.symm x) ∉ s := by
-              intro x
-              simp only [← Finset.mem_compl, Finset.coe_mem]
-            exact this _ h |>.elim
-          · simp [Nat.sub_add_cancel (not_lt.mp hn')]
-    },
-    by
-      intro x
-      constructor
-      · intro hx
-        simp [hx]
-      · by_cases hx : x ∈ s <;> simp [hx]
-  ⟩
+          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 x := by
+        constructor
+        · intro hx
+          simpa [hx, -Fin.is_lt] using (g _).is_lt
+        · by_cases hx : x ∈ s <;> simp [hx] }
   left_inv := by
     rintro ⟨f, hf⟩
     ext x
@@ -149,11 +129,10 @@ def PrefixedNumbering (s : Finset α) : Finset (Numbering α) :=
   {f | IsPrefix s f}
 
 theorem card_PrefixedNumbering (s : Finset α) :
-    (PrefixedNumbering s).card = s.card.factorial * (card α - s.card).factorial := by
-  have h_eq:= Fintype.card_congr (equiv_IsPrefix_NumberingOn2 s)
+    (PrefixedNumbering s).card = (#s).factorial * (card α - #s).factorial := by
+  have h_eq:= Fintype.card_congr (equiv_IsPrefix_Numbering2 s)
   rw [Fintype.card_subtype] at h_eq
-  rw [PrefixedNumbering, h_eq, Fintype.card_prod,
-      card_NumberingOn s, card_NumberingOn sᶜ, card_compl]
+  simp [PrefixedNumbering, h_eq, card_Numbering]
 
 private lemma auxLemma {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
     (↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
@@ -174,11 +153,11 @@ private lemma auxLemma {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
 instance : MeasurableSpace (Numbering α) := ⊤
 
 theorem count_PrefixedNumbering (s : Finset α) :
-    count (PrefixedNumbering s).toSet = ↑(s.card.factorial * (card α - s.card).factorial) := by
+    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.card := by
+    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]
@@ -191,7 +170,7 @@ theorem disj_PrefixedNumbering {s t : Finset α} (h_st : ¬ s ⊆ t) (h_ts : ¬
   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.card t.card with h_st' | h_ts'
+  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')
 
@@ -211,10 +190,9 @@ theorem prob_biUnion_antichain (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
   rw [measure_biUnion_finset hd hm (μ := uniformOn Set.univ)]
 
 theorem LYM_inequality (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
-    ∑ s ∈ 𝓐, ((1 : ENNReal) / (card α).choose s.card) ≤ 1 := by
-  have h1 : ∀ s ∈ 𝓐,
-      (1 : ENNReal) / (card α).choose s.card = uniformOn Set.univ (PrefixedNumbering s).toSet := by
-    intro s h_s
+    ∑ 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