Bounding the mutual information

theorem multiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type u_1} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hΩfin : ∀ (i : Fin m), MeasureTheory.IsFiniteMeasure MeasureTheory.volume) {G : Type u_2} [MeasurableFinGroup G] (X : (i : Fin m) → Ω i → G) : D[fun (i : Fin m') => X (Fin.cast h i) ; fun (i : Fin m') => hΩ (Fin.cast h i)] = D[X ; hΩ]

theorem ProbabilityTheory.iIndepFun.sum_elim {Ω : Type u_1} {I : Type u_2} {J : Type u_3} {G : Type u_4} [MeasurableSpace Ω] [hG : MeasurableSpace G] (μ : MeasureTheory.Measure Ω) {f : I → Ω → G} {g : J → Ω → G} (hf_indep : iIndepFun f μ) (hg_indep : iIndepFun g μ) (hindep : IndepFun (fun (ω : Ω) (x : I) => f x ω) (fun (ω : Ω) (y : J) => g y ω) μ) : iIndepFun (Sum.elim f g) μ

For Mathlib?

theorem condMultiDist_of_cast {m m' : ℕ} (h : m' = m) {Ω : Fin m → Type u_1} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) {G : Type u_2} {S : Type u_3} [MeasurableFinGroup G] [Fintype S] (X : (i : Fin m) → Ω i → G) (Y : (i : Fin m) → Ω i → S) : D[fun (i : Fin m') => X (Fin.cast h i) | fun (i : Fin m') => Y (Fin.cast h i) ; fun (i : Fin m') => hΩ (Fin.cast h i)] = D[X | Y ; hΩ]

theorem mutual_information_le {G Ωₒ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] {p : multiRefPackage G Ωₒ} {Ω : Type u} [hΩ : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X : Fin p.m → Ω → G} (hX : ∀ (i : Fin p.m), Measurable (X i)) (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} [hΩ' : MeasureTheory.MeasureSpace Ω'] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {X' : Fin p.m × Fin p.m → Ω' → G} (hX' : ∀ (i j : Fin p.m), Measurable (X' (i, j))) (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) ω] ≤ ↑p.m * (4 * ↑p.m + 1) * 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.$