More results about Ruzsa distance

More facts about Ruzsa distance and related inequalities, for use in the m-torsion version of PFR.

Main definitions

• multiDist: An analogue of rdist for the m-torsion version of PFR.
• condMultiDist: A conditional analogue of multiDist

Main results

• kvm_ineq_I, kvm_ineq_II, kvm_ineq_III: Variants of the Kaimonovich-Versik-Madiman inequality
• multiDist_chainRule: A chain rule for multiDist
• cor_multiDist_chainRule: The corollary of the chain rule needed for the m-torsion version of PFR
• ent_of_sub_smul_le: Controlling H[X - aY] in terms of H[X] and d[X ; Y].

theorem ProbabilityTheory.mutual_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [Countable U] [Nonempty S] [Nonempty T] [Nonempty U] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] {X : Ω → S} {Y : Ω → T} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → U) [FiniteRange X] [FiniteRange Y] : I[f ∘ X : Y ; μ] ≤ I[X : Y ; μ]

Let X, Ybe random variables. For any function f, g on the range of X, we have I[f(X) : Y] ≤ I[X : Y].

theorem ProbabilityTheory.mutual_comp_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} {V : Type uV} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [Countable U] [Countable V] [Nonempty S] [Nonempty T] [Nonempty U] [Nonempty V] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSpace V] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [MeasurableSingletonClass V] {X : Ω → S} {Y : Ω → T} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : S → U) (g : T → V) (hg : Measurable g) [FiniteRange X] [FiniteRange Y] : I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ]

Let X, Y be random variables. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ].

theorem ProbabilityTheory.condMutual_comp_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} {V : Type uV} {W : Type uW} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [Countable V] [Countable W] [Nonempty S] [Nonempty T] [Nonempty V] [Nonempty W] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSpace V] [MeasurableSpace W] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [MeasurableSingletonClass V] [MeasurableSingletonClass W] {X : Ω → S} {Y : Ω → T} {Z : Ω → U} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (f : S → V) (g : T → W) (hg : Measurable g) [FiniteRange X] [FiniteRange Y] [FiniteRange Z] : I[f ∘ X : g ∘ Y|Z;μ] ≤ I[X : Y|Z;μ]

Let X, Y, Z. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ].

theorem ProbabilityTheory.indepFun_of_identDistrib_pair {Ω : Type u_7} {Ω' : Type u_8} {α : Type u_9} {β : Type u_10} [MeasurableSpace Ω] [MeasurableSpace Ω'] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] {X : Ω → α} {X' : Ω' → α} {Y : Ω → β} {Y' : Ω' → β} (hX : AEMeasurable X μ) (hX' : AEMeasurable X' μ') (hY : AEMeasurable Y μ) (hY' : AEMeasurable Y' μ') (h_indep : ProbabilityTheory.IndepFun X Y μ) (h_ident : ProbabilityTheory.IdentDistrib (fun (ω : Ω) => (X ω, Y ω)) (fun (ω : Ω') => (X' ω, Y' ω)) μ μ') : ProbabilityTheory.IndepFun X' Y' μ'

theorem rdist_of_neg_le {Ω : Type u_1} {Ω' : Type u_2} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [mΩ' : MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] {X : Ω → G} {Y : Ω' → G} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] (hX : Measurable X) (hY : Measurable Y) [Fintype G] : d[X ; μ # -Y ; μ'] ≤ 3 * d[X ; μ # Y ; μ']

If X, Y are G-valued, then d[X;-Y] ≤ 3 d[X;Y].

theorem kvm_ineq_I {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableAdd₂ G] [Countable G] [MeasureTheory.IsProbabilityMeasure μ] {I : Type u_7} {i₀ : I} {s : Finset I} (hs : i₀ ∉ s) {Y : I → Ω → G} [∀ (i : I), FiniteRange (Y i)] (hY : ∀ (i : I), Measurable (Y i)) (hindep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) : H[Y i₀ + s.sum fun (i : I) => Y i ; μ] - H[Y i₀ ; μ] ≤ s.sum fun (i : I) => H[Y i₀ + Y i ; μ] - H[Y i₀ ; μ]

If n ≥ 0 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then H[Y i₀ + ∑ i in s, Y i; μ ] - H[Y i₀; μ ] ≤ ∑ i in s, (H[ Y i₀ + Y i; μ] - H[Y i₀; μ]). The spelling here is tentative. Feel free to modify it to make the proof easier, or the application easier.

theorem kvm_ineq_II {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] [MeasureTheory.IsProbabilityMeasure μ] {I : Type u_7} {i₀ : I} {s : Finset I} (hs : i₀ ∉ s) (hs' : s.Nonempty) {Y : I → Ω → G} [∀ (i : I), FiniteRange (Y i)] (hY : ∀ (i : I), Measurable (Y i)) (hindep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) : d[Y i₀ ; μ # s.sum fun (i : I) => Y i ; μ] ≤ 2 * s.sum fun (i : I) => d[Y i₀ ; μ # Y i ; μ]

If n ≥ 1 and X, Y₁, ..., Yₙ$ are jointly independent G-valued random variables, then d[Y i₀; μ # ∑ i in s, Y i; μ ] ≤ 2 * ∑ i in s, d[Y i₀; μ # Y i; μ].

theorem kvm_ineq_III_aux {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → G} {Y : Ω → G} {Z : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange Z] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X, Y, Z] μ) : d[X ; μ # Y + Z ; μ] ≤ d[X ; μ # Y ; μ] + 2⁻¹ * (H[Y + Z ; μ] - H[Y ; μ])

theorem kvm_ineq_III {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] [MeasureTheory.IsProbabilityMeasure μ] {I : Type u_7} {i₀ : I} {i₁ : I} {s : Finset I} (hs₀ : i₀ ∉ s) (hs₁ : i₁ ∉ s) (h01 : i₀ ≠ i₁) (Y : I → Ω → G) [∀ (i : I), FiniteRange (Y i)] (hY : ∀ (i : I), Measurable (Y i)) (hindep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) : d[Y i₀ ; μ # Y i₁ + s.sum fun (i : I) => Y i ; μ] ≤ d[Y i₀ ; μ # Y i₁ ; μ] + 2⁻¹ * (H[Y i₁ + s.sum fun (i : I) => Y i ; μ] - H[Y i₁ ; μ])

If n ≥ 1 and X, Y₁, ..., Yₙ$ are jointly independent G-valued random variables, then d[Y i₀, ∑ i, Y i] ≤ d[Y i₀, Y i₁] + 2⁻¹ * (H[∑ i, Y i] - H[Y i₁]).

theorem ent_of_sum_le_ent_of_sum {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [AddCommGroup G] [MeasureTheory.IsProbabilityMeasure μ] {I : Type u_7} {s : Finset I} {t : Finset I} (hdisj : Disjoint s t) (hs : s.Nonempty) (ht : t.Nonempty) (X : I → Ω → G) (hX : ∀ (i : I), Measurable (X i)) (hX' : ∀ (i : I), FiniteRange (X i)) (hindep : ProbabilityTheory.iIndepFun (fun (i : I) => hG) X μ) (f : I → I) (hf : Finset.image f t ⊆ s) : H[t.sum fun (i : I) => X i ; μ] ≤ H[s.sum fun (i : I) => X i ; μ] + t.sum fun (i : I) => H[X i - X (f i) ; μ] - H[X (f i) ; μ]

Let X₁, ..., Xₘ and Y₁, ..., Yₗ be tuples of jointly independent random variables (so the X's and Y's are also independent of each other), and let f: {1,..., l} → {1,... ,m} be a function, then H[∑ j, Y j] ≤ H[∑ i, X i] + ∑ j, H[Y j - X f(j)] - H[X_{f(j)}].

theorem ent_of_sub_smul {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] {X : Ω → G} [FiniteRange X] {Y : Ω → G} {X' : Ω → G} [FiniteRange Y] [FiniteRange X'] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X, Y, X'] μ) (hident : ProbabilityTheory.IdentDistrib X X' μ μ) {a : ℤ} : H[X - (a + 1) • Y ; μ] ≤ H[X - a • Y ; μ] + H[X - Y - X' ; μ] - H[X ; μ]

Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer. Then H[X - (a+1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]

theorem ent_of_sub_smul' {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] {X : Ω → G} [FiniteRange X] {Y : Ω → G} {X' : Ω → G} [FiniteRange Y] [FiniteRange X'] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (Nat.succ 0).succ.succ) => hG) ![X, Y, X'] μ) (hident : ProbabilityTheory.IdentDistrib X X' μ μ) {a : ℤ} : H[X - (a - 1) • Y ; μ] ≤ H[X - a • Y ; μ] + H[X - Y - X' ; μ] - H[X ; μ]

Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer. Then H[X - (a-1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]

theorem ent_of_sub_smul_le {Ω : Type u_1} {G : Type u_5} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] {X : Ω → G} {Y : Ω → G} [MeasureTheory.IsProbabilityMeasure μ] [Fintype G] (hX : Measurable X) (hY : Measurable Y) (hindep : ProbabilityTheory.IndepFun X Y μ) {a : ℤ} : H[X - a • Y ; μ] - H[X ; μ] ≤ 4 * ↑|a| * d[X ; μ # Y ; μ]

Let X,Y be independent G-valued random variables, and let a be an integer. Then H[X - aY] - H[X] ≤ 4 |a| d[X ; Y].

noncomputable def multiDist {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) : ℝ

Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i. Then we define D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i'], where the X_i' are independent copies of the X_i.

Equations

• One or more equations did not get rendered due to their size.

def «termD[_;_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «termD[_;_]» : Lean.ParserDescr

Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i. Then we define D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i'], where the X_i' are independent copies of the X_i.

Equations

• One or more equations did not get rendered due to their size.

theorem multiDist_copy {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} {Ω' : Fin m → Type u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hΩ' : (i : Fin m) → MeasureTheory.MeasureSpace (Ω' i)) (X : (i : Fin m) → Ω i → G) (X' : (i : Fin m) → Ω' i → G) (hident : ∀ (i : Fin m), ProbabilityTheory.IdentDistrib (X i) (X' i) MeasureTheory.volume MeasureTheory.volume) : D[X ; hΩ] = D[X' ; hΩ']

If X_i has the same distribution as Y_i for each i, then D[X_[m]] = D[Y_[m]].

theorem multiDist_indep {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Type u_8} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) : D[X ; fun (x : Fin m) => hΩ] = H[Finset.univ.sum fun (i : Fin m) => X i] - (Finset.univ.sum fun (i : Fin m) => H[X i]) / ↑m

If X_i are independent, then D[X_{[m]}] = H[∑_{i=1}^m X_i] - \frac{1}{m} \sum_{i=1}^m H[X_i].

theorem multiDist_nonneg {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) : D[X ; hΩ] ≥ 0

We have D[X_[m]] ≥ 0.

theorem multiDist_of_perm {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) (φ : Equiv.Perm (Fin m)) : D[X ; hΩ] = D[fun (i : Fin m) => X (φ i) ; fun (i : Fin m) => hΩ (φ i)]

If φ : {1, ..., m} → {1, ...,m} is a bijection, then D[X_[m]] = D[(X_φ(1), ..., X_φ(m))]

theorem multidist_ruzsa_I {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) : (Finset.univ.sum fun (j : Fin m) => Finset.univ.sum fun (k : Fin m) => if j = k then 0 else d[X j # X k]) ≤ ↑m * (↑m - 1) * D[X ; hΩ]

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Then ∑ (1 ≤ j, k ≤ m, j ≠ k), d[X_j; -X_k] ≤ m(m-1) D[X_[m]].

theorem multidist_ruzsa_II {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) : (Finset.univ.sum fun (j : Fin m) => d[X j # X j]) ≤ 2 * ↑m * D[X ; hΩ]

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Then ∑ j, d[X_j;X_j] ≤ 2 m D[X_[m]].

theorem multidist_ruzsa_III {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) (hident : ∀ (j k : Fin m), ProbabilityTheory.IdentDistrib (X j) (X k) MeasureTheory.volume MeasureTheory.volume) (i : Fin m) : D[X ; hΩ] ≤ ↑m * d[X i # X i]

Let I be an indexing set of size m ≥ 2, and let X_[m] be a tuple of G-valued random variables. If the X_i all have the same distribution, then D[X_[m]] ≤ m d[X_i;X_i] for any 1 ≤ i ≤ m.

theorem multidist_ruzsa_IV {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 2) {Ω : Type u_8} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) : d[Finset.univ.sum fun (i : Fin m) => X i # Finset.univ.sum fun (i : Fin m) => X i] ≤ 2 * D[X ; fun (x : Fin m) => hΩ]

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Let W := ∑ X_i. Then d[W;-W] ≤ 2 D[X_i].

theorem multidist_eq_zero {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω i → G) (hvanish : D[X ; hΩ] = 0) (i : Fin m) : ∃ (H : AddSubgroup G) (U : Ω i → G), Measurable U ∧ ProbabilityTheory.IsUniform (↑H) U MeasureTheory.volume ∧ d[X i # U] = 0

If D[X_[m]]=0, then for each i ∈ I there is a finite subgroup H_i ≤ G such that d[X_i; U_{H_i}] = 0.

noncomputable def condMultiDist {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) {S : Type u_9} (X : (i : Fin m) → Ω i → G) (Y : (i : Fin m) → Ω i → S) : ℝ

If X_[m] = (X_1, ..., X_m) and Y_[m] = (Y_1, ..., Y_m) are tuples of random variables, with the X_i being G-valued (but the Y_i need not be), then we define D[X_[m] | Y_[m]] := H[∑ i, X_i | (Y_1, ..., Y_m)] - 1/m * ∑ i, H[X_i' | Y_i'] where (X_i', Y_i), 1 ≤ i ≤ m are independent copies of (X_i,Y_i), 1 ≤ i ≤ m (but note here that we do not assume X_i are independent of Y_i, or X_i' independent of Y_i.

Equations

• One or more equations did not get rendered due to their size.

def «termD[_|_;_]».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «termD[_|_;_]» : Lean.ParserDescr

Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i. Then we define D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i'], where the X_i' are independent copies of the X_i.

Equations

• One or more equations did not get rendered due to their size.

theorem condMultiDist_eq {G : Type u_7} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} {Ω : Fin m → Type u_8} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) {S : Type u_9} (X : (i : Fin m) → Ω i → G) (Y : (i : Fin m) → Ω i → S) : D[X | Y ; hΩ] = ∑' (ω : Fin m → S), (Finset.univ.prod fun (i : Fin m) => (MeasureTheory.volume (Y i ⁻¹' {ω i})).toReal) * D[X ; fun (i : Fin m) => MeasureTheory.MeasureSpace.mk (ProbabilityTheory.cond MeasureTheory.volume (Y i ⁻¹' {ω i}))]

With the above notation, we have D[ X_[m] | Y_[m]] = ∑_{(y_i)_{1 \leq i \leq m}} (∏ i, p_{Y_i}(y_i)) D[(X_i | Y_i = y_i)_{i=1}^m] where each y_i ranges over the support of p_{Y_i} for 1 ≤ i ≤ m.

theorem multiDist_chainRule (G : Type u_7) (H : Type u_8) [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [MeasurableSub₂ H] [MeasurableAdd₂ H] [Countable H] (π : G →+ H) {m : ℕ} {Ω : Type u_9} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) : D[X ; fun (x : Fin m) => hΩ] = D[X | fun (i : Fin m) => ⇑π ∘ X i ; fun (x : Fin m) => hΩ] + D[fun (i : Fin m) => ⇑π ∘ X i ; fun (x : Fin m) => hΩ] + I[Finset.univ.sum fun (i : Fin m) => X i : fun (ω : Ω) (i : Fin m) => π (X i ω)|⇑π ∘ Finset.univ.sum fun (i : Fin m) => X i]

Let π : G → H be a homomorphism of abelian groups and let X_[m] be a tuple of jointly independent G-valued random variables. Then D[X_[m]] is equal to D[X_[m] | π(X_[m])] + D[π(X_[m])] + I[∑ i, X_i : π(X_[m]) ; | ; π(∑ i, X_i)] where π(X_[m]) := (π(X_1), ..., π(X_m)).

theorem cond_multiDist_chainRule (G : Type u_7) (H : Type u_8) [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [MeasurableSub₂ G] [MeasurableAdd₂ G] [Countable G] [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [MeasurableSub₂ H] [MeasurableAdd₂ H] [Countable H] (π : G →+ H) {S : Type u_9} [hS : MeasurableSpace S] {m : ℕ} {Ω : Type u_10} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G) (Y : Fin m → Ω → S) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG.prod hS) (fun (i : Fin m) => ⟨X i, Y i⟩) MeasureTheory.volume) : D[X | Y ; fun (x : Fin m) => hΩ] = D[X | fun (i : Fin m) => ⟨⇑π ∘ X i, Y i⟩ ; fun (x : Fin m) => hΩ] + D[fun (i : Fin m) => ⇑π ∘ X i | Y ; fun (x : Fin m) => hΩ] + I[Finset.univ.sum fun (i : Fin m) => X i : fun (ω : Ω) (i : Fin m) => π (X i ω)|⟨⇑π ∘ Finset.univ.sum fun (i : Fin m) => X i, fun (ω : Ω) (i : Fin m) => Y i ω⟩]

Let π : G → H be a homomorphism of abelian groups. Let I be a finite index set and let X_[m] be a tuple of G-valued random variables. Let Y_[m] be another tuple of random variables (not necessarily G-valued). Suppose that the pairs (X_i, Y_i) are jointly independent of one another (but X_i need not be independent of Y_i). Then D[X_[m] | Y_[m]] = D[X_[m] ,|, π(X_[m]), Y_[m]] + D[π(X_[m]) ,| , Y_[m]] + I[∑ i, X_i : π(X_[m]) ; | ; π(∑ i, X_i), Y_[m] ].

theorem iter_multiDist_chainRule {m : ℕ} (G : Fin (m + 1) → Type u_7) (hG : (i : Fin (m + 1)) → MeasurableSpace (G i)) (hGs : ∀ (i : Fin (m + 1)), MeasurableSingletonClass (G i)) (hGa : (i : Fin (m + 1)) → AddCommGroup (G i)) (hGsub : ∀ (i : Fin (m + 1)), MeasurableSub₂ (G i)) (hGadd : ∀ (i : Fin (m + 1)), MeasurableAdd₂ (G i)) (hGcount : ∀ (i : Fin (m + 1)), Countable (G i)) (φ : (i : Fin (m + 1)) → G (i + 1) →+ G i) (π : (d : Fin (m + 1)) → G ↑m →+ G d) (hcomp : ∀ i < m, ⇑(π ↑i) = ⇑(φ ↑i) ∘ ⇑(π (↑i + 1))) {Ω : Type u_8} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G ↑m) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG ↑m) X MeasureTheory.volume) : D[X ; fun (x : Fin m) => hΩ] = ((Finset.Iio m).sum fun (d : ℕ) => D[fun (i : Fin m) => ⇑(π (↑d + 1)) ∘ X i | fun (i : Fin m) => ⇑(π ↑d) ∘ X i ; fun (x : Fin m) => hΩ]) + (Finset.Iio m).sum fun (d : ℕ) => I[Finset.univ.sum fun (i : Fin m) => X i : fun (ω : Ω) (i : Fin m) => (π (↑d + 1)) (X i ω)|⟨⇑(π (↑d + 1)) ∘ Finset.univ.sum fun (i : Fin m) => X i, fun (ω : Ω) (i : Fin m) => (π ↑d) (X i ω)⟩]

Let m be a positive integer. Suppose one has a sequence G_m → G_{m-1} → ... → G_1 → G_0 = {0} of homomorphisms between abelian groups G_0, ...,G_m, and for each d=0, ...,m, let π_d : G_m → G_d be the homomorphism from G_m to G_d arising from this sequence by composition (so for instance π_m is the identity homomorphism and π_0 is the zero homomorphism). Let X_[m] = (X_1, ..., X_m) be a jointly independent tuple of G_m-valued random variables. Then D[X_[m]] = ∑ d, D[π_d(X_[m]) ,| , π_(d-1)(X_[m])] + ∑_{d=1}^{m-1}, I[∑ i, X_i : π_d(X_[m]) | π_d(∑ i, X_i), π_(d-1})(X_[m])].

theorem iter_multiDist_chainRule' {m : ℕ} (G : Fin (m + 1) → Type u_7) (hG : (i : Fin (m + 1)) → MeasurableSpace (G i)) (hGs : ∀ (i : Fin (m + 1)), MeasurableSingletonClass (G i)) (hGa : (i : Fin (m + 1)) → AddCommGroup (G i)) (hGsub : ∀ (i : Fin (m + 1)), MeasurableSub₂ (G i)) (hGadd : ∀ (i : Fin (m + 1)), MeasurableAdd₂ (G i)) (hGcount : ∀ (i : Fin (m + 1)), Countable (G i)) (φ : (i : Fin (m + 1)) → G (i + 1) →+ G i) (π : (d : Fin (m + 1)) → G ↑m →+ G d) (hcomp : ∀ i < m, ⇑(π ↑i) = ⇑(φ ↑i) ∘ ⇑(π (↑i + 1))) {Ω : Type u_8} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin m → Ω → G ↑m) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG ↑m) X MeasureTheory.volume) : D[X ; fun (x : Fin m) => hΩ] ≥ (Finset.Iio m).sum fun (d : ℕ) => D[fun (i : Fin m) => ⇑(π (↑d + 1)) ∘ X i | fun (i : Fin m) => ⇑(π ↑d) ∘ X i ; fun (x : Fin m) => hΩ]

Under the preceding hypotheses, D[ X_[m]] ≥ ∑ d, D[π_d(X_[m])| π_(d-1})(X_[m])] + I[∑ i, X_i : π_1(X_[m]) | π_1(∑ i, X_i)].

theorem cor_multiDist_chainRule {G : Type u_5} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ} (hm : m ≥ 1) {Ω : Type u_7} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin (m + 1) × Fin (m + 1) → Ω → G) (hindep : ProbabilityTheory.iIndepFun (fun (x : Fin (m + 1) × Fin (m + 1)) => hG) X MeasureTheory.volume) : I[fun (ω : Ω) (j : Fin (m + 1)) => Finset.univ.sum fun (i : Fin (m + 1)) => X (i, j) ω : fun (ω : Ω) (i : Fin (m + 1)) => Finset.univ.sum fun (j : Fin (m + 1)) => X (i, j) ω|Finset.univ.sum fun (p : Fin (m + 1) × Fin (m + 1)) => X p] ≤ (Finset.univ.sum fun (j : Fin (m + 1)) => D[fun (i : Fin (m + 1)) => X (i, j) ; fun (x : Fin (m + 1)) => hΩ] - D[fun (i : Fin (m + 1)) => X (i, j) | fun (i : Fin (m + 1)) => (Finset.Ici j).sum fun (k : Fin (m + 1)) => X (i, k) ; fun (x : Fin (m + 1)) => hΩ]) + D[fun (i : Fin (m + 1)) => X (i, ↑m) ; fun (x : Fin (m + 1)) => hΩ] - D[fun (i : Fin (m + 1)) => Finset.univ.sum fun (j : Fin (m + 1)) => X (i, j) ; fun (x : Fin (m + 1)) => hΩ]

Let G be an abelian group and let m ≥ 2. Suppose that X_{i,j}, 1 ≤ i, j ≤ m, are independent G-valued random variables. Then I[(∑ i, X_{i,j})_{j=1}^m : (∑ j, X_{i,j})_{i=1}^m | ∑ i j, X_{i,j}] is less than ∑_{j=1}^{m-1} (D[(X_{i, j})_{i=1}^m] - D[(X_{i, j})_{i = 1}^m | (X_{i,j} + ... + X_{i,m})_{i=1}^m]) + D[(X_{i,m})_{i=1}^m] - D[(∑ j, X_{i,j})_{i=1}^m], where all the multidistances here involve the indexing set {1, ..., m}.