Bounding the mutual information

Main definitions:

Main results

theorem mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ : MeasureTheory.MeasureSpace Ω] (X : Fin p.m → Ω → G) (h_indep : ProbabilityTheory.iIndepFun X MeasureTheory.volume) (h_min : multiTauMinimizes p (fun (x : Fin p.m) => Ω) (fun (x : Fin p.m) => hΩ) X) (Ω' : Type u_1) [MeasureTheory.MeasureSpace Ω'] (X' : Fin p.m × Fin p.m → Ω' → G) (h_indep' : ProbabilityTheory.iIndepFun X' MeasureTheory.volume) (hperm : ∀ (j : Fin p.m), ∃ (e : Fin p.m ≃ Fin p.m), ProbabilityTheory.IdentDistrib (fun (ω : Ω') (i : Fin p.m) => X' (i, j) ω) (fun (ω : Ω) (i : Fin p.m) => X (e i) ω) MeasureTheory.volume MeasureTheory.volume) : I[fun (ω : Ω') (j : Fin p.m) => ∑ i : Fin p.m, X' (i, j) ω : fun (ω : Ω') (i : Fin p.m) => ∑ j : Fin p.m, X' (i, j) ω|fun (ω : Ω') => ∑ i : Fin p.m, ∑ j : Fin p.m, X' (i, j) ω] ≤ 4 * ↑p.m ^ 2 * p.η * D[X ; fun (x : Fin p.m) => hΩ]

Suppose that $X_{i,j}$, $1\le i,j\le 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}:=\text{bbI}[(\sum _{i=1}^m{X}_{i,j}{)}_{j=1}^m:(\sum _{j=1}^m{X}_{i,j}{)}_{i=1}^m|\sum _{i=1}^m\sum _{j=1}^m{X}_{i,j}].$$ Then $\mathcal{I}\le 4m^2\eta k.$