start on key estimate. Discovered a typo which propagated a little downstream, now fixed.

Author: teorth

PFR/BoundingMutual.lean

@@ -28,9 +28,63 @@ $$ {\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 Ω] (X : ∀ i, Ω → G)
   (h_indep : iIndepFun X)
-  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω']
+  (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [hΩ': MeasureSpace Ω']
+  [IsProbabilityMeasure hΩ'.volume]
   (X' : Fin p.m × Fin p.m → Ω' → G) (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) ω ] ≤ 4 * p.m^2 * p.η * D[ X; (fun _ ↦ hΩ)] := sorry
+    fun ω ↦ ∑ i, ∑ j, X' (i, j) ω ] ≤ 2 * p.m * (2*p.m + 1) * p.η * D[ X; (fun _ ↦ hΩ)] := by
+    have hm := p.hm
+    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Ω]
+    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) ω
+    set V : Fin p.m → Ω' → G := fun i ω ↦ ∑ j, X' (i, j) ω
+    set S : Fin p.m → Fin p.m → Ω' → G := fun i j ↦ ∑ k ∈ .Ici j, X' (i, k)
+    set A : Fin p.m → ℝ := fun j ↦ D[ column j; fun _ ↦ hΩ']
+      - D[ column j | fun i ↦ S i j; fun _ ↦ hΩ']
+    set B : ℝ := D[ column last; fun _ ↦ hΩ'] - D[ fun j ω ↦ ∑ i, X' (i, j) ω; fun _ ↦ hΩ']
+
+    have h1 : I₀ ≤ ∑ j ∈ .Iio last, A j + B := by
+      sorry
+
+    have h2 {j : Fin p.m} (hj: j ∈ Finset.Iio last)
+      : A j ≤ p.η * ∑ i, d[ X' (i,j) # X' (i,j) | S i j ] := by
+        sorry
+
+    have h3 : B ≤ p.η * ∑ i, d[ X' (i, last) # V i ] := by
+      sorry
+
+    have h4 (i: Fin p.m) {j : Fin p.m} (hj: j ∈ Finset.Iio last) :
+      d[ X' (i,j) # X' (i,j) | S i j ] ≤ d[ X' (i,j) # X' (i,j) ]
+        + (H[S i j] - H[S i (j+one)]) / 2 := by
+        sorry
+
+    have h5 (i: Fin p.m) :
+      ∑ j ∈ Finset.Iio last, d[ X' (i,j) # X' (i,j) | S i j ]
+        ≤ ∑ j ∈ Finset.Iio last, d[ X' (i,j) # X' (i,j) ] + (H[V i] - H[X' (i, last)]) / 2 := by
+        sorry
+
+    have h6 (i: Fin p.m) :
+      d[ X' (i, last) # V i ] ≤ d[ X' (i, last) # X' (i, last) ]
+        + (H[V i] - H[X' (i, last)]) / 2 := by
+        sorry
+
+    have h7 : I₀/p.η ≤ p.m * ∑ i, d[X i # X i] + ∑ i, H[V i] - ∑ i, H[X i] := by
+      sorry
+
+    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] + p.m * k := by linarith
+
+    have h11 : ∑ i, d[X i # X i] ≤ 2 * p.m * k := by
+      sorry
+
+    sorry

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] ≤ 4 * p.m ^ 2 * p.η * k := by
+lemma mutual_information_le_t_12 : I[Z1 : Z2 | W] ≤ 2 * p.m * (2 * 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] ≤ 4 * p.m ^ 2 * p.η * k := by
+lemma mutual_information_le_t_23 : I[Z2 : Z3 | W] ≤ 2 * p.m * (2 * 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] ≤ 4 * p.m ^ 2 * p.η * k :=
   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] ≤ 4 * p.m ^ 2 * p.η * k := by
+lemma mutual_information_le_t_21 : I[Z1 : Z3 | W] ≤ 2 * p.m * (2 * 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 4 m^2 \eta k.
+    {\mathcal I} \leq 2 m(2m+1) \eta k.
   \end{equation}
 \end{proposition}
 
@@ -515,9 +515,9 @@ \section{Bounding the mutual information}
   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}$.
-\Cref{cond-multidist-lower-II}, we have
+By \Cref{cond-multidist-lower-II}, we have
 \begin{align}
-  A_j & \leq \eta \sum_{i = 1}^{m-1} 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,
 \[
@@ -614,7 +614,7 @@ \section{Endgame}
   \]
   where
   \begin{equation}\label{t-def}
-    t :=  4m^2 \eta k.
+    t :=  2m(2m+1) \eta k.
   \end{equation}
 \end{proposition}
 
@@ -820,7 +820,7 @@ \section{Endgame}
     \label{eq:delta-w}
     \nonumber
     \delta_\ast := \sum_w p_W(w) \delta_w &= \bbI[Z_1 : Z_2 \,|\, W] + \bbI[Z_1 : Z_3 \,|\, W] + \bbI[Z_2 : Z_3 \,|\, W] \\
-                           & \leq 12 m^2 \eta k
+                           & \leq 6 m (2m+1) \eta k
   \end{align}
   by \Cref{prop:52}.
   Write $U_w$ for the random variable guaranteed to exist by \Cref{lem:get-better},
@@ -847,10 +847,10 @@ \section{Endgame}
   since the terms $d[X_i; U_w]$ cancel by our choice of $\alpha$.
   Substituting in \Cref{xi-z2-w-dist} and~\eqref{eq:delta-w}, and using the fact that $2 + \frac{\eta}{2} < 3$, we have
   \[
-    12 m^3 (2+\frac{\eta}{2}) \eta k + \eta 8(m^3-m^2) k \geq k.
+    6 m^2 (2m+1) (2+\frac{\eta}{2}) \eta k + \eta 8(m^3-m^2) k \geq k.
   \]
   From \Cref{eta-def-multi} we have we have
-  $$ 12 m^3 (2+\frac{\eta}{2}) \eta + \eta 8(m^3-m^2) < 1$$
+  $$ 6 m^2 (2m+1) (2+\frac{\eta}{2}) \eta + \eta 8(m^3-m^2) < 1$$
   and hence $k \leq 0$.  The claim now follows from \Cref{multidist-nonneg}.
 \end{proof}