Dealing with n-tuples of random variables

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

One difference between the m-torsion PFR proof and the already formalized 2-torsion PFR proof is that in the latter we only needed to deal with fixed tuples of random variables (e.g. two or three or four random variables), but now we need to deal with m random variables where m is a natural number not fixed in advance. This creates some potential "dependent type hell" issues, even with the basic issue of spelling some of the results we will need, so I wanted to ask advice on best practices here.

For now let's begin with an easy one (#5 on the outstanding tasks list). I would like to formalize the following statement (a version of the Kaimonovich--Vershik--Madiman inequality):

If $n \geq 1$ and $X, Y_1, \dots, Y_n$ are jointly independent $G$-valued random variables, then $H[X + \sum_{i=1}^n Y_i] - H[X] \leq \sum_{i=1}^n H[X+Y_i] - H[X].$

[The n=2 case of this inequality was already formalized here; the general case should then follow by a routine induction, modulo some tricky issues with the iIndepFun API that we strugged a bit with in previous stages of the project.]

In order to make the joint independence easier to state, I was thinking of renaming $X$ as $Y_0$, and spelling this as

import Mathlib

open Filter Function MeasureTheory Measure ProbabilityTheory

open scoped BigOperators

noncomputable def entropy {Ω S: Type*} [MeasurableSpace Ω] (X : Ω → S) (μ : Measure Ω := by volume_tac) : ℝ := sorry

notation3:max "H[" X " ; " μ "]" => entropy X μ

variable {Ω G : Type*} [mΩ : MeasurableSpace Ω] {μ : Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G]  [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G]

lemma kvm_ineq_I {n:ℕ} (Y: Fin (n+1) → Ω → G) (hY: (i:Fin (n+1)) → Measurable (Y i))
                 (hindep: iIndepFun (fun (i:Fin (n+1)) => hG) Y μ )
                : H[ ∑ i in Finset.univ, Y i; μ ] - H[ Y 0; μ ] ≤ ∑ i in Finset.Ioi 0, (H[ Y 0 + Y i; μ] - H[Y 0; μ]) := by sorry

I'm finding though that I'm quite rusty on Lean after a few months of inactivity, and was not sure whether this was a good (or correct) spelling or not. Any thoughts? [I'm realizing that the statement is vacuously true for n=0, so I didn't include the hypothesis $n \geq 1$ here.]

This situation is still relatively nice because all the random variables take values on the same probability space $\Omega$. Later on there are other results involving tuples $X_1,\dots,X_m$ of random variables that take values in different measure spaces $\Omega_1,\dots,\Omega_m$, which cause some annoying issues regarding how to describe the MeasurableSpace structure on the $\Omega_i$ as an instance, but perhaps I will talk more about that later when we get to it.

[Yaël Dillies]

∑ i : Fin n, f i is (usually) an anti-pattern. The better solution is ∑ i ∈ s, f i where s : Finset ι, f : ι → α, as then you can induct on s.

[Yaël Dillies]

In case this change makes proving hindep annoying, we could change its type to something like iIndepFun (fun _ ↦ hG) (fun i : s ↦ Y i) μ.

[Terence Tao]

OK, here is version 2.0 then:

open Classical in
/--  If $n \geq 1$ and $X, Y_1, \dots, Y_n$ are jointly independent $G$-valued random variables, then
  $$ H[X + \sum_{i=1}^n Y_i] - H[X] \leq \sum_{i=1}^n H[X+Y_i] - \bbH[X].$$ -/
lemma kvm_ineq_I {I:Type*} (i₀: I) (s: Finset I) (hs: i₀ ∈ s) (Y: I → Ω → G) (hY: (i:I) → Measurable (Y i))
                 (hindep: iIndepFun (fun (i:I) => hG) Y μ )
                : H[ ∑ i in s, Y i; μ ] - H[ Y i₀; μ ] ≤ ∑ i in (Finset.erase s i₀), (H[ Y i₀ + Y i; μ] - H[Y i₀; μ]) := by sorry

I guess I could add a note to whoever attempts to prove it that they are welcome to adjust the spelling if it makes it significantly easier to prove.

[Yaël Dillies]

Nit: Prefer adding elements to a finset over removing them. So here use s in place of erase s i₀. Eg

lemma kvm_ineq_I {I : Type*} (i₀ : I) (s : Finset I) (hi₀ : i₀ ∉ s) (Y : I → Ω → G)
    (hY : ∀ i, Measurable (Y i)) (hindep : iIndepFun (fun i ↦ hG) Y μ) :
    H[Y i₀ + ∑ i in s, Y i ; μ] - H[Y i₀ ; μ] ≤ ∑ i in s, (H[Y i₀ + Y i; μ] - H[Y i₀ ; μ]) :=
  sorry