h2 done. 5 more to go!

Author: teorth

PFR/BoundingMutual.lean

@@ -72,19 +72,20 @@ $$ {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m}
 lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ]
   {p : multiRefPackage G Ωₒ} {Ω : Type u} [hΩ : MeasureSpace Ω] [IsProbabilityMeasure hΩ.volume]
   {X : ∀ i, Ω → G} (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X)
-  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) {Ω' : Type*} [hΩ': MeasureSpace Ω']
+  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) {Ω' : Type u} [hΩ': MeasureSpace Ω']
   [IsProbabilityMeasure hΩ'.volume]
   {X' : Fin p.m × Fin p.m → Ω' → G} (hX' : ∀ i j, Measurable (X' (i, j)))
   (h_indep': iIndepFun X')
   (hperm : ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω))
     (fun ω ↦ (fun i ↦ X (e i) ω))) :
   I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) |
-    fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 2 * p.m * (2*p.m + 1) * p.η * D[ X; (fun _ ↦ hΩ)] := by
+    fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ p.m * (4*p.m+1) * p.η * D[ X; (fun _ ↦ hΩ)] := by
     have hm := p.hm
     have hη := p.hη
     set I₀ := I[ fun ω ↦ ( fun j ↦ ∑ i, X' (i, j) ω) : fun ω ↦ ( fun i ↦ ∑ j, X' (i, j) ω) |
     fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ]
     set k := D[X ; fun x ↦ hΩ]
+    have hk: 0 ≤ k := multiDist_nonneg _ inferInstance _ (by fun_prop)
     set one : Fin p.m := ⟨ 1, by omega ⟩
     set last : Fin p.m := ⟨ p.m-1, by omega ⟩
     set column : Fin p.m → Fin p.m → Ω' → G := fun j i ω ↦ X' (i, j) ω
@@ -143,9 +144,24 @@ lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureS
       apply ProbabilityTheory.iIndepFun.precomp _ h_indep'
       intro ⟨ i, j ⟩ ⟨ i', j' ⟩ h; simpa using h
 
+    have hD (j: Fin p.m) : D[column j ; fun x ↦ hΩ'] = k := by
+      obtain ⟨ e, he ⟩ := hperm j
+      calc
+        _ = D[fun i ω ↦ X (e i) ω; fun x ↦ hΩ] := by
+          apply multiDist_copy _ _ _ _ _
+          intro i; exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
+        _ = _ := by
+          convert multiDist_of_perm (fun _ ↦ hΩ) _ _ e <;> try infer_instance
+
     have h2 {j : Fin p.m} (hj: j ∈ Finset.Iio last)
-      : A j ≤ p.η * (k + ∑ i, d[ X' (i,j) # X' (i,j) | S i j ]) := by
-        sorry
+      : A j ≤ p.η * ∑ i, d[ X' (i,j) # X' (i,j) | S i j ] := by
+        obtain ⟨ e, he ⟩ := hperm j
+        simp only [A, hD]
+        convert sub_condMultiDistance_le' p (fun _ ↦ Ω) (fun _ ↦ hΩ) inferInstance X hX h_min (fun _ ↦ Ω') (fun _ ↦ hΩ') inferInstance (fun i ↦ X' (i, j)) _ _ _ e using 3 with i _ <;> try infer_instance
+        all_goals try fun_prop
+        apply condRuzsaDist'_of_copy <;> try fun_prop
+        . exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
+        apply IdentDistrib.refl; fun_prop
 
     have h3 : B ≤ p.η * ∑ i, d[ X' (i, last) # V i ] := by
       sorry
@@ -188,50 +204,47 @@ lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureS
         + (H[V i] - H[X' (i, last)]) / 2 := by
         sorry
 
-    have h7 : I₀/p.η ≤ p.m * k + p.m * ∑ i, d[X i # X i] + ∑ i, H[V i] - ∑ i, H[X i] := by
+    have h7 : I₀/p.η ≤ p.m * ∑ i, d[X i # X i] + ∑ i, H[V i] - ∑ i, H[X i] := by
       rw [div_le_iff₀' hη]
       apply h1.trans
       calc
-        _ ≤ ∑ j ∈ .Iio last, (p.η * (k + ∑ i, d[ X' (i,j) # X' (i,j) | S i j ])) + p.η * ∑ i, d[ X' (i, last) # V i ] := by gcongr with j hj; exact h2 hj
-        _ ≤ p.η * (↑↑last * k + ∑ i, (∑ j ∈ .Iio last, d[ X' (i,j) # X' (i,j) ] + (H[V i] - H[X' (i, last)]) / 2)) +
+        _ ≤ ∑ j ∈ .Iio last, (p.η * (∑ i, d[ X' (i,j) # X' (i,j) | S i j ])) + p.η * ∑ i, d[ X' (i, last) # V i ] := by gcongr with j hj; exact h2 hj
+        _ ≤ p.η * (∑ i, (∑ j ∈ .Iio last, d[ X' (i,j) # X' (i,j) ] + (H[V i] - H[X' (i, last)]) / 2)) +
         p.η * ∑ i, (d[ X' (i, last) # X' (i, last) ] + (H[V i] - H[X' (i, last)]) / 2) := by
           simp [←Finset.mul_sum, Finset.sum_add_distrib]; rw [Finset.sum_comm]; gcongr
           . rw [←Finset.sum_add_distrib]; apply Finset.sum_le_sum; intro i _; exact h5 i
           rw [←Finset.sum_add_distrib]; apply Finset.sum_le_sum; intro i _; exact h6 i
-        _ = p.η * (↑↑last * k + ∑ i, (∑ j ∈ .Iio last, d[ X' (i,j) # X' (i,j) ] + d[ X' (i, last) # X' (i, last) ]) + ∑ i, H[V i] - ∑ i, H[X' (i, last)]) := by
+        _ = p.η * (∑ i, (∑ j ∈ .Iio last, d[ X' (i,j) # X' (i,j) ] + d[ X' (i, last) # X' (i, last) ]) + ∑ i, H[V i] - ∑ i, H[X' (i, last)]) := by
           simp_rw [Finset.sum_add_distrib, ←Finset.sum_div, Finset.sum_sub_distrib]; ring
-        _ = p.η * (↑↑last * k + ∑ j, (∑ i, d[ X' (i,j) # X' (i,j) ]) + ∑ i, H[V i] - ∑ i, H[X' (i, last)]) := by
+        _ = p.η * (∑ j, (∑ i, d[ X' (i,j) # X' (i,j) ]) + ∑ i, H[V i] - ∑ i, H[X' (i, last)]) := by
           rw [Finset.sum_comm]
           rcongr i
           convert Finset.sum_erase_add _ _ _ using 3
           . ext ⟨ j, hj ⟩; simp [last]; omega
           . infer_instance
           simp
-        _ = p.η * (↑↑last * k + (∑ j:Fin p.m, (∑ i, d[ X i # X i ])) + ∑ i, H[V i] - ∑ i, H[X i]) := by
+        _ = p.η * ((∑ j:Fin p.m, (∑ i, d[ X i # X i ])) + ∑ i, H[V i] - ∑ i, H[X i]) := by
           congr 2
           . congr; ext j; obtain ⟨ e, he ⟩ := hperm j
             convert Equiv.sum_comp e _ with i _
             apply IdentDistrib.rdist_congr <;> exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
           obtain ⟨ e, he ⟩ := hperm last
           convert Equiv.sum_comp e _ with i _
-          apply IdentDistrib.entropy_congr <;> exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
-        _ ≤ _ := by
-          simp [last]; gcongr
-          . apply multiDist_nonneg _ inferInstance _ (by fun_prop)
-          omega
+          apply IdentDistrib.entropy_congr; exact IdentDistrib.comp (u := fun x ↦ x i) he (by fun_prop)
+        _ ≤ _ := by simp
 
     have h8 (i: Fin p.m) : H[V i] ≤ H[ ∑ j, X j] + ∑ j, d[X' (i,j) # X' (i,j)] := by
       sorry
 
     have h9 : ∑ i, H[V i] - ∑ i, H[X i] ≤ p.m * ∑ i, d[X i # X i] + p.m * k := by
       sorry
 
-    have h10 : I₀/p.η ≤ 2 * p.m * ∑ i, d[X i # X i] + 2 * p.m * k := by linarith
+    have h10 : I₀/p.η ≤ 2 * p.m * ∑ i, d[X i # X i] + p.m * k := by linarith
 
     have h11 : ∑ i, d[X i # X i] ≤ 2 * p.m * k := by
       convert multidist_ruzsa_II hm _ _ _ hX _ <;> try infer_instance
 
     calc
-       _ ≤ p.η * (2 * p.m * ∑ i, d[X i # X i] + 2 * p.m * k) := by rwa [←div_le_iff₀' (by positivity)]
-      _ ≤ p.η * (2 * p.m * (2 * p.m * k) + 2 * p.m * k) := by gcongr
+       _ ≤ p.η * (2 * p.m * ∑ i, d[X i # X i] + p.m * k) := by rwa [←div_le_iff₀' (by positivity)]
+      _ ≤ p.η * (2 * p.m * (2 * p.m * k) + p.m * k) := by gcongr
       _ = _ := by ring

PFR/TorsionEndgame.lean

@@ -60,7 +60,7 @@ lemma indep_yj (j : Fin p.m) : iIndepFun (fun i ↦ Y (i, j)) := by
 include h_mes h_indep hident h_min in
 /-- We have `I[Z_1 : Z_2 | W], I[Z_2 : Z_3 | W], I[Z_1 : Z_3 | W] ≤ 4m^2 η k`.
 -/
-lemma mutual_information_le_t_12 : I[Z1 : Z2 | W] ≤ 2 * p.m * (2 * p.m + 1) * p.η * k := by
+lemma mutual_information_le_t_12 : I[Z1 : Z2 | W] ≤ p.m * (4*p.m+1) * p.η * k := by
   have hm := p.hm
   let zero : Fin p.m := ⟨ 0, by linarith [hm]⟩
   have hindep_j (j: Fin p.m) : iIndepFun (fun i ↦ Y (i, j)) := indep_yj h_mes h_indep j
@@ -89,7 +89,7 @@ lemma torsion_mul_eq {i j:ℤ} (x:G) (h: i ≡ j [ZMOD p.m]) : i • x = j • x
   simp [add_smul, mul_comm, mul_zsmul, p.htorsion]
 
 include h_mes h_indep hident h_min in
-lemma mutual_information_le_t_23 : I[Z2 : Z3 | W] ≤ 2 * p.m * (2 * p.m + 1) * p.η * k := by
+lemma mutual_information_le_t_23 : I[Z2 : Z3 | W] ≤ p.m * (4*p.m+1) * p.η * k := by
   have hm := p.hm
   have _ : NeZero p.m := by rw [neZero_iff]; linarith
   let zero : Fin p.m := ⟨ 0, by linarith [hm]⟩
@@ -140,7 +140,7 @@ lemma mutual_information_le_t_23 : I[Z2 : Z3 | W] ≤ 2 * p.m * (2 * p.m + 1) *
   exact (hident (i-j) j).trans (hident (i-j) zero).symm
 
 include h_mes h_indep hident h_min in
-lemma mutual_information_le_t_21 : I[Z1 : Z3 | W] ≤ 2 * p.m * (2 * p.m + 1) * p.η * k := by
+lemma mutual_information_le_t_21 : I[Z1 : Z3 | W] ≤ p.m * (4*p.m+1) * p.η * k := by
   have hm := p.hm
   have _ : NeZero p.m := by rw [neZero_iff]; linarith
   let zero : Fin p.m := ⟨ 0, by linarith [hm]⟩

blueprint/src/chapter/torsion.tex

@@ -491,7 +491,7 @@ \section{Bounding the mutual information}
   \]
 Then
   \begin{equation}\label{I-ineq}
-    {\mathcal I} \leq 2 m(2m+1) \eta k.
+    {\mathcal I} \leq m(4m+1) \eta k.
   \end{equation}
 \end{proposition}
 
@@ -510,14 +510,14 @@ \section{Bounding the mutual information}
   B := D[ (X_{i,m})_{i=1}^m ] - D[ \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i=1}^m ].
 \]
 We first consider the $A_j$, for fixed $j \in \{1,\dots, m-1\}$.
-By \Cref{multidist-perm} and and our hypothesis on columns, we have
+By \Cref{multidist-perm} and our hypothesis on columns, we have
 \[
   D[ (X_{i, j})_{i = 1}^m ]= D[ (X_i)_{i=1}^m ] = k.
 \]
-Let $\sigma = \sigma_j \colon I \to I$ be a permutation such that $X_{i,j} = X_{\sigma(i)}$, and write $X'_i := X_{i,j}$ and $Y_i := X_{i,j} + \cdots + X_{i,m}$.
+Let $\sigma = \sigma_j \colon I \to I$ be a permutation such that $X_{i,j} \equiv X_{\sigma(i)}$, and write $X'_i := X_{i,j}$ and $Y_i := X_{i,j} + \cdots + X_{i,m}$.
 By \Cref{cond-multidist-lower-II}, we have
 \begin{align}
-  A_j & \leq \eta (k+\sum_{i = 1}^{m} d[X_{i,j}; X_{i, j}|X_{i, j} + \cdots + X_{i,m}]).\label{54a}
+  A_j & \leq \eta (\sum_{i = 1}^{m} d[X_{i,j}; X_{i, j}|X_{i, j} + \cdots + X_{i,m}]).\label{54a}
 \end{align}
 We similarly consider $B$.  By \Cref{multidist-perm} applied to the $m$-th column,
 \[
@@ -554,7 +554,7 @@ \section{Bounding the mutual information}
 Combining~\eqref{441},~\eqref{54a} and~\eqref{55a} with~\eqref{eq:distbnd1} and~\eqref{eq:distbnd2} (the latter two summed over $i$), we get
 \begin{align}
   \nonumber
-  \frac1{\eta} {\mathcal I} &\leq mk + \sum_{i,j=1}^m d[X_{i,j};X_{i,j}] + \sum_{i=1}^m (\bbH[V_i] - \bbH[X_{i,m}]) \\
+  \frac1{\eta} {\mathcal I} &\leq \sum_{i,j=1}^m d[X_{i,j};X_{i,j}] + \sum_{i=1}^m (\bbH[V_i] - \bbH[X_{i,m}]) \\
       &= m \sum_{i=1}^m d[X_i; X_i] + \sum_{i=1}^m \bbH[V_i] - \sum_{i=1}^m \bbH[X_i].
       \label{eq:distbnd3}
 \end{align}
@@ -568,7 +568,7 @@ \section{Bounding the mutual information}
 \end{align*}
 where in the second step we used the permutation hypothesis. Combining this with~\eqref{eq:distbnd3} gives the
 $$
-{\mathcal I} \leq 2\eta m \biggl( \sum_{i=1}^m d[X_i;X_i] \biggr).$$
+{\mathcal I} \leq 2\eta m \biggl( \sum_{i=1}^m d[X_i;X_i] \biggr) + mk.$$
 The claim \eqref{I-ineq} is now immediate from \Cref{multidist-ruzsa-II}.
 \end{proof}
 
@@ -614,7 +614,7 @@ \section{Endgame}
   \]
   where
   \begin{equation}\label{t-def}
-    t :=  2m(2m+1) \eta k.
+    t :=  m(4m+1) \eta k.
   \end{equation}
 \end{proposition}