another stub

PFR/BoundingMutual.lean

@@ -12,16 +12,23 @@ import PFR.MultiTauFunctional
 
 -/
 
-open MeasureTheory ProbabilityTheory
+open MeasureTheory ProbabilityTheory BigOperators
 
-/-- 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$ coincide in distribution with some permutation of $X_{[m]}$.
+-- Spelling here is *very* janky.  Feel free to respell
+/-- 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$
+coincide in distribution with some permutation of $X_{[m]}$.
   Write
-  \[
-    {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m} : \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m \; \big| \; \sum_{i=1}^m \sum_{j = 1}^m  X_{i,j} ].
-  \]
-Then
-  \begin{equation}\label{I-ineq}
-    {\mathcal I} \leq 4 m^2 \eta k.
-  \end{equation}
+$$    {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m}
+: \bigl(\sum_{j=1}^m X_{i,j}\bigr)_{i = 1}^m
+\; \big| \; \sum_{i=1}^m \sum_{j = 1}^m  X_{i,j} ].
+ $$
+ Then ${\mathcal I} \leq 4 m^2 \eta k.$
 -/
-lemma mutual_information_le : 0 = 1 := sorry
+lemma mutual_information_le  (p : multiRefPackage) (Ω : Type*) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → p.G) (hindep:
+  iIndepFun (fun _ ↦ p.hGm) X)
+  (hmin : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω'] (X': Fin p.m × Fin p.m → Ω' → p.G) (hindep': iIndepFun (fun _ ↦ p.hGm) X') (hperm:
+  have _ := p.hGm
+  ∀ j, ∃ e : Fin p.m ≃ Fin p.m, IdentDistrib (fun ω ↦ (fun i ↦ X' (i, j) ω) ) (fun ω ↦ (fun i ↦ X (e i) ω))) :
+  have _ := p.hG
+  have _ := p.hGm
+  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

blueprint/src/chapter/torsion.tex

@@ -476,7 +476,7 @@ \section{Bounding the mutual information}
 
 As before, $G$ is an abelian group, and $m\geq 2$.  We let $X_{[m]} = (X_i)_{i =1}^m$ be a $\tau$-minimizer.
 
-\begin{proposition}[Bounding mutual information]\label{key}\lean{mutual_information_le}
+\begin{proposition}[Bounding mutual information]\label{key}\lean{mutual_information_le}\leanok
 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$ coincide in distribution with some permutation of $X_{[m]}$.
   Write
   \[