Skip to content

Commit f05e5b7

Browse files
ctchouctchou
committed
Split out some code in ProbLYM.lean into KatonaCircle.lean
1 parent 3f2c83a commit f05e5b7

File tree

3 files changed

+107
-68
lines changed

3 files changed

+107
-68
lines changed

‎LeanCamCombi.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
1515
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
1616
import LeanCamCombi.Mathlib.Data.Fintype.Card
1717
import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
18+
import LeanCamCombi.PlainCombi.KatonaCircle
1819
import LeanCamCombi.PlainCombi.LittlewoodOfford
1920
import LeanCamCombi.PlainCombi.OrderShatter
2021
import LeanCamCombi.PlainCombi.ProbLYM

‎LeanCamCombi/PlainCombi/KatonaCircle.lean‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
/-
2+
Copyright (c) 2024 Ching-Tsun Chou, Chris Wong. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Ching-Tsun Chou, Chris Wong
5+
-/
6+
import LeanCamCombi.Mathlib.Data.Fintype.Card
7+
import LeanCamCombi.PlainCombi.ProbLYM
8+
import Mathlib.Probability.UniformOn
9+
10+
/-!
11+
# The LYM inequality using probability theory
12+
13+
This file proves the LYM inequality using (very elementary) probability theory.
14+
15+
## References
16+
17+
This proof formalizes Section 1.2 of Prof. Yufei Zhao's lecture notes for MIT 18.226:
18+
19+
<https://yufeizhao.com/pm/probmethod_notes.pdf>
20+
21+
A video of Prof. Zhao's lecture is available on YouTube:
22+
23+
<https://youtu.be/exBXHYl4po8>
24+
25+
The proof of Theorem 1.10, Lecture 3 in the Cambridge lecture notes on combinatorics:
26+
27+
<https://github.com/YaelDillies/maths-notes/blob/master/combinatorics.pdf>
28+
29+
is basically the same proof, except without using probability theory.
30+
-/
31+
32+
open BigOperators Fintype Finset Set MeasureTheory ProbabilityTheory
33+
open MeasureTheory.Measure
34+
open scoped ENNReal
35+
36+
noncomputable section
37+
38+
private lemma auxLemma {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
39+
(↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
40+
-- The following proof is due to Aaron Liu.
41+
subst heq
42+
have hm : m ≠ 0 := by rintro rfl ; simp at hn
43+
have hk : k ≠ 0 := by rintro rfl ; simp at hn
44+
refine (ENNReal.toReal_eq_toReal ?_ ?_).mp ?_
45+
· intro h
46+
apply_fun ENNReal.toReal at h
47+
simp [hm, hk] at h
48+
· intro h
49+
apply_fun ENNReal.toReal at h
50+
simp [hk] at h
51+
· field_simp
52+
ring
53+
54+
variable {α : Type*} [Fintype α] [DecidableEq α]
55+
56+
instance : MeasurableSpace (Numbering α) := ⊤
57+
58+
theorem count_PrefixedNumbering (s : Finset α) :
59+
count (PrefixedNumbering s).toSet = ↑((#s).factorial * (card α - #s).factorial) := by
60+
rw [← card_PrefixedNumbering s, count_apply_finset]
61+
62+
theorem prob_PrefixedNumbering (s : Finset α) :
63+
uniformOn Set.univ (PrefixedNumbering s).toSet = 1 / (card α).choose #s := by
64+
rw [uniformOn_univ, count_PrefixedNumbering s, card_Numbering]
65+
apply auxLemma (Nat.factorial_pos (card α))
66+
rw [← mul_assoc]
67+
exact Nat.choose_mul_factorial_mul_factorial (Finset.card_le_univ s)
68+
69+
theorem disj_PrefixedNumbering {s t : Finset α} (h_st : ¬ s ⊆ t) (h_ts : ¬ t ⊆ s) :
70+
Disjoint (PrefixedNumbering s).toSet (PrefixedNumbering t).toSet := by
71+
refine Set.disjoint_iff.mpr ?_
72+
intro p
73+
simp only [mem_inter_iff, Finset.mem_coe, mem_empty_iff_false, imp_false, not_and]
74+
simp [PrefixedNumbering]
75+
intro h_s h_t
76+
rcases Nat.le_total #s t.card with h_st' | h_ts'
77+
· exact h_st (subset_IsPrefix_IsPrefix h_s h_t h_st')
78+
· exact h_ts (subset_IsPrefix_IsPrefix h_t h_s h_ts')
79+
80+
variable {𝓐 : Finset (Finset α)}
81+
82+
theorem prob_biUnion_antichain (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
83+
uniformOn Set.univ (⋃ s ∈ 𝓐, (PrefixedNumbering s).toSet) =
84+
∑ s ∈ 𝓐, uniformOn Set.univ (PrefixedNumbering s).toSet := by
85+
have hd : 𝓐.toSet.PairwiseDisjoint (fun s ↦ (PrefixedNumbering s).toSet) := by
86+
intro s h_s t h_t h_ne
87+
simp only [Function.onFun]
88+
have h_st := h𝓐 h_s h_t h_ne
89+
have h_ts := h𝓐 h_t h_s h_ne.symm
90+
exact disj_PrefixedNumbering h_st h_ts
91+
have hm : ∀ s ∈ 𝓐, MeasurableSet (PrefixedNumbering s).toSet := by
92+
intro s h_s ; exact trivial
93+
rw [measure_biUnion_finset hd hm (μ := uniformOn Set.univ)]
94+
95+
theorem LYM_inequality (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
96+
∑ s ∈ 𝓐, ((1 : ENNReal) / (card α).choose #s) ≤ 1 := by
97+
have h1 s (hs : s ∈ 𝓐) :
98+
(1 : ENNReal) / (card α).choose #s = uniformOn Set.univ (PrefixedNumbering s).toSet := by
99+
rw [prob_PrefixedNumbering]
100+
rw [Finset.sum_congr (rfl : 𝓐 = 𝓐) h1, ← prob_biUnion_antichain h𝓐]
101+
exact prob_le_one
102+
103+
end

‎LeanCamCombi/PlainCombi/ProbLYM.lean‎

Lines changed: 3 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Ching-Tsun Chou, Chris Wong
55
-/
66
import LeanCamCombi.Mathlib.Data.Fintype.Card
7+
import Mathlib.Data.Fintype.Prod
78
import Mathlib.Data.Fintype.Perm
8-
import Mathlib.Probability.UniformOn
99

1010
/-!
1111
# The LYM inequality using probability theory
@@ -29,15 +29,13 @@ The proof of Theorem 1.10, Lecture 3 in the Cambridge lecture notes on combinato
2929
is basically the same proof, except without using probability theory.
3030
-/
3131

32-
open BigOperators Fintype Finset Set MeasureTheory ProbabilityTheory
33-
open MeasureTheory.Measure
34-
open scoped ENNReal
32+
open Fintype Finset Set
3533

3634
noncomputable section
3735

3836
/-- A numbering is a bijective map from a finite type or set to a Fin type
3937
of the same cardinality. We cannot use the existing notion of permutations
40-
in mathlib because we need the special property `set_prefix_subset` below. -/
38+
in mathlib because we need the special property `subset_IsPrefix_IsPrefix` below. -/
4139

4240
@[reducible]
4341
def Numbering (α : Type*) [Fintype α] := α ≃ Fin (card α)
@@ -134,67 +132,4 @@ theorem card_PrefixedNumbering (s : Finset α) :
134132
rw [Fintype.card_subtype] at h_eq
135133
simp [PrefixedNumbering, h_eq, card_Numbering]
136134

137-
private lemma auxLemma {k m n : ℕ} (hn : 0 < n) (heq : k * m = n) :
138-
(↑ m : ENNReal) / (↑ n : ENNReal) = 1 / (↑ k : ENNReal) := by
139-
-- The following proof is due to Aaron Liu.
140-
subst heq
141-
have hm : m ≠ 0 := by rintro rfl ; simp at hn
142-
have hk : k ≠ 0 := by rintro rfl ; simp at hn
143-
refine (ENNReal.toReal_eq_toReal ?_ ?_).mp ?_
144-
· intro h
145-
apply_fun ENNReal.toReal at h
146-
simp [hm, hk] at h
147-
· intro h
148-
apply_fun ENNReal.toReal at h
149-
simp [hk] at h
150-
· field_simp
151-
ring
152-
153-
instance : MeasurableSpace (Numbering α) := ⊤
154-
155-
theorem count_PrefixedNumbering (s : Finset α) :
156-
count (PrefixedNumbering s).toSet = ↑((#s).factorial * (card α - #s).factorial) := by
157-
rw [← card_PrefixedNumbering s, count_apply_finset]
158-
159-
theorem prob_PrefixedNumbering (s : Finset α) :
160-
uniformOn Set.univ (PrefixedNumbering s).toSet = 1 / (card α).choose #s := by
161-
rw [uniformOn_univ, count_PrefixedNumbering s, card_Numbering]
162-
apply auxLemma (Nat.factorial_pos (card α))
163-
rw [← mul_assoc]
164-
exact Nat.choose_mul_factorial_mul_factorial (Finset.card_le_univ s)
165-
166-
theorem disj_PrefixedNumbering {s t : Finset α} (h_st : ¬ s ⊆ t) (h_ts : ¬ t ⊆ s) :
167-
Disjoint (PrefixedNumbering s).toSet (PrefixedNumbering t).toSet := by
168-
refine Set.disjoint_iff.mpr ?_
169-
intro p
170-
simp only [mem_inter_iff, Finset.mem_coe, mem_empty_iff_false, imp_false, not_and]
171-
simp [PrefixedNumbering]
172-
intro h_s h_t
173-
rcases Nat.le_total #s t.card with h_st' | h_ts'
174-
· exact h_st (subset_IsPrefix_IsPrefix h_s h_t h_st')
175-
· exact h_ts (subset_IsPrefix_IsPrefix h_t h_s h_ts')
176-
177-
variable {𝓐 : Finset (Finset α)}
178-
179-
theorem prob_biUnion_antichain (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
180-
uniformOn Set.univ (⋃ s ∈ 𝓐, (PrefixedNumbering s).toSet) =
181-
∑ s ∈ 𝓐, uniformOn Set.univ (PrefixedNumbering s).toSet := by
182-
have hd : 𝓐.toSet.PairwiseDisjoint (fun s ↦ (PrefixedNumbering s).toSet) := by
183-
intro s h_s t h_t h_ne
184-
simp only [Function.onFun]
185-
have h_st := h𝓐 h_s h_t h_ne
186-
have h_ts := h𝓐 h_t h_s h_ne.symm
187-
exact disj_PrefixedNumbering h_st h_ts
188-
have hm : ∀ s ∈ 𝓐, MeasurableSet (PrefixedNumbering s).toSet := by
189-
intro s h_s ; exact trivial
190-
rw [measure_biUnion_finset hd hm (μ := uniformOn Set.univ)]
191-
192-
theorem LYM_inequality (h𝓐 : IsAntichain (· ⊆ ·) 𝓐.toSet) :
193-
∑ s ∈ 𝓐, ((1 : ENNReal) / (card α).choose #s) ≤ 1 := by
194-
have h1 s (hs : s ∈ 𝓐) :
195-
(1 : ENNReal) / (card α).choose #s = uniformOn Set.univ (PrefixedNumbering s).toSet := by
196-
rw [prob_PrefixedNumbering]
197-
rw [Finset.sum_congr (rfl : 𝓐 = 𝓐) h1, ← prob_biUnion_antichain h𝓐]
198-
exact prob_le_one
199-
200135
end

0 commit comments

Comments
 (0)