Skip to content

Commit d6b25d1

Browse files
teorthteorth
committed
key estimate done!
1 parent 9abe53e commit d6b25d1

File tree

2 files changed

+109
-4
lines changed

2 files changed

+109
-4
lines changed

‎PFR/BoundingMutual.lean‎

Lines changed: 108 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,42 @@ lemma multiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}
4040
. rw [h]
4141
convert Finset.sum_bijective _ (Fin.cast_bijective h) ?_ ?_ using 1 <;> simp
4242

43+
/-- For Mathlib? -/
44+
lemma ProbabilityTheory.iIndepFun.sum_elim {Ω I J G:Type*} [MeasurableSpace Ω] [hG: MeasurableSpace G] (μ: Measure Ω) {f: (x:I) → Ω → G} {g: (y:J) → Ω → G} (hf_indep: iIndepFun f μ) (hg_indep: iIndepFun g μ)
45+
(hindep: IndepFun (fun ω x ↦ f x ω) (fun ω y ↦ g y ω) μ) : iIndepFun (Sum.elim f g) μ := by
46+
rw [iIndepFun_iff] at hf_indep hg_indep ⊢
47+
intro s E hE
48+
have : s.toLeft.disjSum s.toRight = s := Finset.toLeft_disjSum_toRight
49+
rw [←this, Finset.prod_disjSum,←hf_indep,←hg_indep]
50+
. simp_rw [MeasurableSpace.measurableSet_comap] at hE
51+
choose F hF using hE
52+
let S := ⋂ (i:s.toLeft), {x: I → G | x i ∈ F (Sum.inl i) (Finset.mem_toLeft.mp i.property)}
53+
let T := ⋂ (j:s.toRight), {y: J → G | y j ∈ F (Sum.inr j) (Finset.mem_toRight.mp j.property)}
54+
convert hindep.measure_inter_preimage_eq_mul S T _ _
55+
. ext ω; simp [S,T]; apply and_congr <;> {
56+
apply forall_congr'; intro i
57+
constructor
58+
. intro h hi; simp [←(hF _ hi).2, hi] at h; convert h
59+
intro h hi; specialize h hi; simp [←(hF _ hi).2]; convert h
60+
}
61+
. ext ω; simp [S]; apply forall_congr'; intro i
62+
constructor
63+
. intro h hi; simp [←(hF _ hi).2, hi] at h; convert h
64+
intro h hi; specialize h hi; simp [←(hF _ hi).2]; convert h
65+
. ext ω; simp [T]; apply forall_congr'; intro i
66+
constructor
67+
. intro h hi; simp [←(hF _ hi).2, hi] at h; convert h
68+
intro h hi; specialize h hi; simp [←(hF _ hi).2]; convert h
69+
all_goals {
70+
apply MeasurableSet.iInter; intro ⟨ i, hi ⟩
71+
simp only
72+
convert measurableSet_preimage (measurable_pi_apply i) _
73+
apply (hF _ _).1
74+
}
75+
. intro i hi; apply hE; exact Finset.mem_toRight.mp hi
76+
intro j hj; apply hE; exact Finset.mem_toLeft.mp hj
77+
78+
4379
lemma condMultiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}
4480
(hΩ : ∀ i, MeasureSpace (Ω i))
4581
{G S: Type*} [MeasureableFinGroup G] [Fintype S] (X : ∀ i, (Ω i) → G) (Y : ∀ i, (Ω i) → S) :
@@ -59,6 +95,7 @@ lemma condMultiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type*}
5995
. simp; congr
6096
intros; simp; infer_instance
6197

98+
set_option maxHeartbeats 300000 in
6299
-- Spelling here is *very* janky. Feel free to respell
63100
/-- Suppose that $X_{i,j}$, $1 \leq i,j \leq m$, are jointly independent $G$-valued random variables, such that for each $j = 1,\dots,m$, the random variables $(X_{i,j})_{i = 1}^m$
64101
coincide in distribution with some permutation of $X_{[m]}$.
@@ -274,14 +311,82 @@ lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureS
274311
congr 2
275312
. congr; ext j; obtain ⟨ e, he ⟩ := hperm j
276313
convert Equiv.sum_comp e _ with i _
277-
apply IdentDistrib.rdist_congr <;> exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
314+
apply IdentDistrib.rdist_congr <;> exact he.comp (u := fun x ↦ x i) (by fun_prop)
278315
obtain ⟨ e, he ⟩ := hperm last
279316
convert Equiv.sum_comp e _ with i _
280-
apply IdentDistrib.entropy_congr; exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
317+
apply IdentDistrib.entropy_congr; exact he.comp (u := fun x ↦ x i) (by fun_prop)
281318
_ ≤ _ := by simp
282319

283320
have h8 (i: Fin p.m) : H[V i] ≤ H[ ∑ j, X j] + ∑ j, d[X' (i,j) # X' (i,j)] := by
284-
sorry
321+
obtain ⟨ ν, XX, XX', hν, hXX, hXX', h_indep_XX_XX', hident_X, hident_X', hfin_XX, hfin_XX'⟩ := independent_copies_finiteRange (X := fun ω i ↦ X i ω) (Y := fun ω q ↦ X' q ω)
322+
(by fun_prop) (by fun_prop) ℙ ℙ
323+
let Ω'' := (Fin p.m → G) × (Fin p.m × Fin p.m → G)
324+
let _ : MeasureSpace (Ω'') := ⟨ ν ⟩
325+
let Z : Fin p.m → Ω'' → G := fun i ω ↦ XX ω i
326+
let Z' : Fin p.m × Fin p.m → Ω'' → G := fun i ω ↦ XX' ω i
327+
-- the claim below could be abstracted into a Mathlib lemma.
328+
have hindep_Z : iIndepFun Z ℙ := by
329+
rw [iIndepFun_iff_map_fun_eq_pi_map] at h_indep ⊢ <;> try fun_prop
330+
convert h_indep with i
331+
. exact IdentDistrib.map_eq hident_X
332+
apply IdentDistrib.map_eq
333+
exact hident_X.comp (u := fun x ↦ x i) (by fun_prop)
334+
have hindep_Z' : iIndepFun Z' ℙ := by
335+
rw [iIndepFun_iff_map_fun_eq_pi_map] at h_indep' ⊢ <;> try fun_prop
336+
convert h_indep' with i
337+
. exact IdentDistrib.map_eq hident_X'
338+
apply IdentDistrib.map_eq
339+
exact hident_X'.comp (u := fun x ↦ x i) (by fun_prop)
340+
have hindep_all : iIndepFun (Sum.elim Z Z') ℙ := iIndepFun.sum_elim ℙ hindep_Z hindep_Z' h_indep_XX_XX'
341+
342+
let s : Finset (Fin p.m ⊕ (Fin p.m × Fin p.m)) := Finset.image Sum.inl Finset.univ
343+
let t : Finset (Fin p.m ⊕ (Fin p.m × Fin p.m)) := Finset.image Sum.inr {q|q.1=i}
344+
have hdisj : Disjoint s t := by rw [Finset.disjoint_left]; simp [s,t]
345+
have hs: s.Nonempty := by use Sum.inl one; simp [s]
346+
have ht: t.Nonempty := by use Sum.inr (i,one); simp [t]
347+
choose e he using hperm
348+
let f : Fin p.m ⊕ (Fin p.m × Fin p.m) → Fin p.m ⊕ (Fin p.m × Fin p.m) := fun x ↦ match x with
349+
| Sum.inl i => Sum.inl i
350+
| Sum.inr (i,j) => Sum.inl ((e j) i)
351+
convert ent_of_sum_le_ent_of_sum hdisj hs ht _ _ _ hindep_all f _
352+
. apply IdentDistrib.entropy_congr
353+
convert hident_X'.symm.comp (u := fun x ↦ ∑ j:Fin p.m, x (i, j)) _ <;> try fun_prop
354+
ext ω; simp [Z, Z', t]
355+
apply Finset.sum_nbij' (Prod.snd) (fun j ↦ (i,j))
356+
on_goal 5 => simp; rintro a b rfl; rfl
357+
all_goals simp
358+
. apply IdentDistrib.entropy_congr
359+
convert hident_X.symm.comp (u := fun x ↦ ∑ j, x j) _ <;> try fun_prop
360+
all_goals ext ω; simp [Z, Z', s]
361+
. let g : Fin p.m ⊕ (Fin p.m × Fin p.m) → Fin p.m := fun x ↦ match x with
362+
| Sum.inl i => i
363+
| Sum.inr (i,j) => j
364+
apply Finset.sum_nbij' (fun j ↦ Sum.inr (i,j)) g <;> try simp [t,g,f]
365+
intro j
366+
have hident_1 : IdentDistrib (X' (i, j)) (Z' (i, j)) ℙ ℙ := by
367+
convert hident_X'.symm.comp (u := fun x ↦ x (i, j)) _; fun_prop
368+
have hident_2 : IdentDistrib (Z' (i, j)) (Z ((e j) i)) ℙ ℙ := by
369+
apply hident_1.symm.trans
370+
have h1 : IdentDistrib (X ((e j) i)) (Z ((e j) i)) ℙ ℙ := by
371+
convert hident_X.symm.comp (u := fun x ↦ x ((e j) i)) _; fun_prop
372+
have h2 : IdentDistrib (X' (i, j)) (X ((e j) i)) ℙ ℙ := by
373+
convert (he j).comp (u := fun x ↦ x i) _; fun_prop
374+
exact h2.trans h1
375+
calc
376+
_ = d[Z' (i, j) # Z ((e j) i)] :=
377+
IdentDistrib.rdist_congr hident_1 (hident_1.trans hident_2)
378+
_ = H[Z' (i, j) - Z ((e j) i)] - H[Z' (i,j)]/2 - H[Z ((e j) i)]/2 := by
379+
apply IndepFun.rdist_eq <;> try fun_prop
380+
symm
381+
apply h_indep_XX_XX'.comp (φ := fun x ↦ x ((e j) i)) (ψ := fun x ↦ x (i, j)) <;> fun_prop
382+
_ = H[Z' (i, j) - Z ((e j) i)] - H[Z ((e j) i)]/2 - H[Z ((e j) i)]/2 := by
383+
rw [IdentDistrib.entropy_congr hident_2]
384+
_ = _ := by ring
385+
. fun_prop
386+
. simp [Z,Z']; constructor
387+
. intros; infer_instance
388+
intro a b; infer_instance
389+
intro x; simp [f,t,s]; aesop
285390

286391
have h9 : ∑ i, H[V i] ≤ p.m * ∑ i, d[X i # X i] + ∑ i, H[X i] + p.m * k := calc
287392
_ ≤ ∑ i, (H[ ∑ j, X j] + ∑ j, d[X' (i,j) # X' (i,j)]) := by

‎blueprint/src/chapter/torsion.tex‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -496,7 +496,7 @@ \section{Bounding the mutual information}
496496
\end{proposition}
497497

498498

499-
\begin{proof}\uses{cor-multid, multidist-perm, cond-multidist-lower-II, first-useful, klm-3, sumset-lower, ruzsa-triangle, compare-sums, multidist-ruzsa-II}
499+
\begin{proof}\uses{cor-multid, multidist-perm, cond-multidist-lower-II, first-useful, klm-3, sumset-lower, ruzsa-triangle, compare-sums, multidist-ruzsa-II}\leanok
500500
For each $j \in \{1,\dots,m\}$ we call the tuple $(X_{i,j})_{i = 1}^m$ a \emph{column} and for each $i \in \{1,\dots, m\}$ we call the tuple $(X_{i,j})_{j = 1}^m$ a \emph{row}. Hence, by hypothesis, each column is a permutation of $X_{[m]} = (X_i)_{i=1}^m$.
501501

502502
From \Cref{cor-multid} we have

0 commit comments

Comments
 (0)