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 (fun (x : Fin p.m) => inferInstance) 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 (fun (x : Fin p.m × Fin p.m) => inferInstance) 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 \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 ${\mathcal I} \leq 4 m^2 \eta k.$