Documentation

PFR.MoreRuzsaDist

More results about Ruzsa distance #

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

Main definitions #

Main results #

theorem ProbabilityTheory.mutual_comp_le {Ω : Type uΩ} {S : Type uS} {T : Type uT} {U : Type uU} [mΩ : MeasurableSpace Ω] [Countable S] [Countable T] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] {X : ΩS} {Y : ΩT} [Countable U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : SU) [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 V] [MeasurableSpace S] [MeasurableSpace T] [MeasurableSpace U] [MeasurableSpace V] [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U] [MeasurableSingletonClass V] {X : ΩS} {Y : ΩT} [Countable U] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : SU) (g : TV) (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] [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 : SV) (g : TW) (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 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] [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] [Countable G] {I : Type u_8} {i₀ : I} {s : Finset I} (hs : i₀s) {Y : IΩG} [∀ (i : I), FiniteRange (Y i)] (hY : ∀ (i : I), Measurable (Y i)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) :
H[Y i₀ + is, Y i ; μ] - H[Y i₀ ; μ] is, (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] [Countable G] {I : Type u_8} {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)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) :
d[Y i₀ ; μ # is, Y i ; μ] 2 * is, 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] [Countable G] {X : ΩG} {Y : ΩG} {Z : ΩG} [FiniteRange X] [FiniteRange Y] [FiniteRange Z] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h_indep : 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] [Countable G] {I : Type u_8} {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)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : I) => hG) Y μ) :
d[Y i₀ ; μ # Y i₁ + is, Y i ; μ] d[Y i₀ ; μ # Y i₁ ; μ] + 2⁻¹ * (H[Y i₁ + is, 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] [MeasurableSingletonClass G] [AddCommGroup G] [Countable G] [MeasureTheory.IsProbabilityMeasure μ] {I : Type u_8} {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)) (h_indep : ProbabilityTheory.iIndepFun (fun (i : I) => hG) X μ) (f : II) (hf : Finset.image f t s) :
H[it, X i ; μ] H[is, X i ; μ] + it, (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] [Countable G] {X : ΩG} {Y : ΩG} {X' : ΩG} [FiniteRange X] [FiniteRange Y] [FiniteRange X'] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (h_indep : 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] [Countable G] {X : ΩG} {Y : ΩG} {X' : ΩG} [FiniteRange X] [FiniteRange Y] [FiniteRange X'] [MeasureTheory.IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (h_indep : 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] [Countable G] {X : ΩG} {Y : ΩG} [MeasureTheory.IsProbabilityMeasure μ] [Fintype G] (hX : Measurable X) (hY : Measurable Y) (h_indep : 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_8} [hG : MeasurableSpace G] [AddCommGroup G] {m : } {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω iG) :

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
Instances For

    Pretty printer defined by notation3 command.

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

      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.
      Instances For
        theorem multiDist_copy {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] {m : } {Ω : Fin mType u_9} {Ω' : Fin mType u_10} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hΩ' : (i : Fin m) → MeasureTheory.MeasureSpace (Ω' i)) (X : (i : Fin m) → Ω iG) (X' : (i : Fin m) → Ω' iG) (hident : ∀ (i : Fin m), ProbabilityTheory.IdentDistrib (X i) (X' i) MeasureTheory.volume MeasureTheory.volume) :
        D[X ; ] = 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_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } {Ω : Type u_9} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin mΩG) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) :
        D[X ; fun (x : Fin m) => ] = H[i : Fin m, X i] - (∑ 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_of_indep {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] [Fintype G] {m : } {Ω : Type u_9} (hΩ : MeasureTheory.MeasureSpace Ω) (hprob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (X : Fin mΩG) (hX : ∀ (i : Fin m), Measurable (X i)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => inferInstance) X MeasureTheory.volume) :
        0 D[X ; fun (x : Fin m) => ]
        theorem multiDist_nonneg {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] [Fintype G] {m : } {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hprob : ∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (X : (i : Fin m) → Ω iG) (hX : ∀ (i : Fin m), Measurable (X i)) :
        0 D[X ; ]

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

        theorem multiDist_of_perm {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hΩprob : ∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (X : (i : Fin m) → Ω iG) (φ : Equiv.Perm (Fin m)) :
        D[fun (i : Fin m) => X (φ i) ; fun (i : Fin m) => (φ i)] = D[X ; ]

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

        theorem multidist_ruzsa_I {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } (hm : m 2) {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω iG) :
        (∑ j : Fin m, k : Fin m, if j = k then 0 else d[X j # X k]) m * (m - 1) * D[X ; ]

        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_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } (hm : m 2) {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω iG) :
        j : Fin m, d[X j # X j] 2 * m * D[X ; ]

        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_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } (hm : m 2) {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω iG) (hidenT : ∀ (j k : Fin m), ProbabilityTheory.IdentDistrib (X j) (X k) MeasureTheory.volume MeasureTheory.volume) (i : Fin m) :
        D[X ; ] 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_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } (hm : m 2) {Ω : Type u_9} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin mΩG) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) :
        d[i : Fin m, X i # i : Fin m, X i] 2 * D[X ; fun (x : Fin m) => ]

        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_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } (hm : m 2) {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin m) → Ω iG) (hvanish : D[X ; ] = 0) (i : Fin m) :
        ∃ (H : AddSubgroup G) (U : Ω iG), 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_8} [hG : MeasurableSpace G] [AddCommGroup G] {m : } {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) {S : Type u_10} [Fintype S] (X : (i : Fin m) → Ω iG) (Y : (i : Fin m) → Ω iS) :

        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]] = ∑_{(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.

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

          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.
          Instances For

            Pretty printer defined by notation3 command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem condMultiDist_of_inj {G : Type u_9} [hG : MeasurableSpace G] [AddCommGroup G] {m : } {Ω : Fin mType u_10} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) {S : Type u_11} [Fintype S] {T : Type u_12} [Fintype T] (X : (i : Fin m) → Ω iG) (Y : (i : Fin m) → Ω iS) {f : ST} (hf : Function.Injective f) :
              D[X | fun (i : Fin m) => f Y i ; ] = D[X | fun (i : Fin m) => Y i ; ]

              Conditional multidistance is unchanged if we apply an injection to the conditioned variables

              theorem condMultiDist_of_const {G : Type u_9} [hG : MeasurableSpace G] [AddCommGroup G] {m : } {Ω : Fin mType u_10} [hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)] [hprob : ∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {S : Type u_11} [Fintype S] (c : Fin mS) (X : (i : Fin m) → Ω iG) :
              D[X | fun (i : Fin m) (x : Ω i) => c i ; ] = D[X ; ]

              Conditional multidistance against a constant is just multidistance

              theorem condMultiDist_nonneg {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] [Fintype G] {m : } {Ω : Fin mType u_9} (hΩ : (i : Fin m) → MeasureTheory.MeasureSpace (Ω i)) (hprob : ∀ (i : Fin m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {S : Type u_10} [Fintype S] (X : (i : Fin m) → Ω iG) (Y : (i : Fin m) → Ω iS) (hX : ∀ (i : Fin m), Measurable (X i)) :
              0 D[X | Y ; ]

              Conditional multidistance is nonnegative.

              theorem condMultiDist_eq {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } {Ω : Type u_9} [hΩ : MeasureTheory.MeasureSpace Ω] {S : Type u_10} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S] {X : Fin mΩG} (hX : ∀ (i : Fin m), Measurable (X i)) {Y : Fin mΩS} (hY : ∀ (i : Fin m), Measurable (Y i)) (h_indep : 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[fun (ω : Ω) => i : Fin m, X i ω | fun (ω : Ω) (i : Fin m) => Y i ω] - (∑ i : Fin m, H[X i | Y i]) / m

              If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = H[∑ i, X_i | (Y_1, ..., Y_m)] - 1/m * ∑ i, H[X_i | Y_i]

              theorem condMultiDist_eq' {G : Type u_8} [hG : MeasurableSpace G] [AddCommGroup G] [MeasurableSingletonClass G] [Countable G] {m : } {Ω : Type u_9} [hΩ : MeasureTheory.MeasureSpace Ω] {S : Type u_10} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S] {X : Fin mΩG} (hX : ∀ (i : Fin m), Measurable (X i)) {Y : Fin mΩS} (hY : ∀ (i : Fin m), Measurable (Y i)) (h_indep : 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) => ] = y : Fin mS, (MeasureTheory.volume (⋂ (i : Fin m), Y i ⁻¹' {y i})).toReal * D[X ; fun (x : Fin m) => MeasureTheory.MeasureSpace.mk (ProbabilityTheory.cond MeasureTheory.volume (⋂ (i : Fin m), Y i ⁻¹' {y i}))]

              If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = ∑_{(y_i)_{1 ≤ i ≤ m}} P(Y_i=y_i ∀ i) D[(X_i | Y_i=y_i ∀ i)_{i=1}^m]

              theorem multiDist_chainRule {G : Type u_8} {H : Type u_9} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [Fintype G] [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [Fintype H] (π : G →+ H) {m : } {Ω : Type u_10} (hΩ : MeasureTheory.MeasureSpace Ω) {X : Fin mΩG} (hmes : ∀ (i : Fin m), Measurable (X i)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG) X MeasureTheory.volume) :
              D[X ; fun (x : Fin m) => ] = D[X | fun (i : Fin m) => π X i ; fun (x : Fin m) => ] + D[fun (i : Fin m) => π X i ; fun (x : Fin m) => ] + I[i : Fin m, X i : fun (ω : Ω) (i : Fin m) => π (X i ω)|π 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_8} {H : Type u_9} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [AddCommGroup G] [Fintype G] [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H] [Fintype H] (π : G →+ H) {S : Type u_10} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S] {m : } {Ω : Type u_11} [hΩ : MeasureTheory.MeasureSpace Ω] {X : Fin mΩG} (hX : ∀ (i : Fin m), Measurable (X i)) {Y : Fin mΩS} (hY : ∀ (i : Fin m), Measurable (Y i)) (h_indep : 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) => ] = D[X | fun (i : Fin m) => π X i, Y i ; fun (x : Fin m) => ] + D[fun (i : Fin m) => π X i | Y ; fun (x : Fin m) => ] + I[i : Fin m, X i : fun (ω : Ω) (i : Fin m) => π (X i ω)|π 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 Iio_of_succ_eq_Iic_of_castSucc {N : } (n : Fin N) :
              Finset.Iio n.succ = Finset.Iic n.castSucc
              theorem iter_multiDist_chainRule {m : } {G : Fin (m + 1)Type u_8} [hG : (i : Fin (m + 1)) → MeasurableSpace (G i)] [hGs : ∀ (i : Fin (m + 1)), MeasurableSingletonClass (G i)] [(i : Fin (m + 1)) → AddCommGroup (G i)] [hGcounT : (i : Fin (m + 1)) → Fintype (G i)] {φ : (i : Fin m) → G i.succ →+ G i.castSucc} {π : (d : Fin (m + 1)) → G m →+ G d} (hcomp : ∀ (i : Fin m), (π i.castSucc) = (φ i) (π i.succ)) {Ω : Type u_9} [hΩ : MeasureTheory.MeasureSpace Ω] {X : Fin mΩG m} (hX : ∀ (i : Fin m), Measurable (X i)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG m) X MeasureTheory.volume) (n : Fin (m + 1)) :
              D[X | fun (i : Fin m) => (π 0) X i ; fun (x : Fin m) => ] = D[X | fun (i : Fin m) => (π n) X i ; fun (x : Fin m) => ] + dFinset.Iio n, (D[fun (i : Fin m) => (π (d + 1)) X i | fun (i : Fin m) => (π d) X i ; fun (x : Fin m) => ] + I[i : Fin m, X i : fun (ω : Ω) (i : Fin m) => (π (d + 1)) (X i ω)|(π (d + 1)) 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 Finset.map_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α β} (s₁ : Finset α) (s₂ : Finset α) :
              Finset.map f (s₁ \ s₂) = Finset.map f s₁ \ Finset.map f s₂
              theorem Finset.map_compl {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [DecidableEq β] {f : α β} (s : Finset α) :
              Finset.map f s = Finset.map f Finset.univ \ Finset.map f s
              theorem sum_of_iio_last (N : ) (f : Fin (N + 1)) :
              dFinset.Iio N, f d = d : Fin N, f d.castSucc
              theorem iter_multiDist_chainRule' {m : } (hm : m > 0) {G : Fin (m + 1)Type u_8} [hG : (i : Fin (m + 1)) → MeasurableSpace (G i)] [hGs : ∀ (i : Fin (m + 1)), MeasurableSingletonClass (G i)] [hGa : (i : Fin (m + 1)) → AddCommGroup (G i)] [hGcount : (i : Fin (m + 1)) → Fintype (G i)] {φ : (i : Fin m) → G i.succ →+ G i.castSucc} {π : (d : Fin (m + 1)) → G m →+ G d} (hπ0 : π 0 = 0) (hcomp : ∀ (i : Fin m), (π i.castSucc) = (φ i) (π i.succ)) {Ω : Type u_9} [hΩ : MeasureTheory.MeasureSpace Ω] {X : Fin mΩG m} (hX : ∀ (i : Fin m), Measurable (X i)) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin m) => hG m) X MeasureTheory.volume) :
              D[X ; fun (x : Fin m) => ] d : Fin m, D[fun (i : Fin m) => (π d.succ) X i | fun (i : Fin m) => (π d.castSucc) X i ; fun (x : Fin m) => ] + I[i : Fin m, X i : fun (ω : Ω) (i : Fin m) => (π 1) (X i ω)|(π 1) i : Fin m, X i]

              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] [MeasurableSingletonClass G] [AddCommGroup G] [Countable G] [Fintype G] {m : } (hm : m 1) {Ω : Type u_8} (hΩ : MeasureTheory.MeasureSpace Ω) (X : Fin (m + 1) × Fin (m + 1)ΩG) (h_indep : ProbabilityTheory.iIndepFun (fun (x : Fin (m + 1) × Fin (m + 1)) => hG) X MeasureTheory.volume) :
              I[fun (ω : Ω) (j : Fin (m + 1)) => i : Fin (m + 1), X (i, j) ω : fun (ω : Ω) (i : Fin (m + 1)) => j : Fin (m + 1), X (i, j) ω|p : Fin (m + 1) × Fin (m + 1), X p] j : Fin (m + 1), (D[fun (i : Fin (m + 1)) => X (i, j) ; fun (x : Fin (m + 1)) => ] - D[fun (i : Fin (m + 1)) => X (i, j) | fun (i : Fin (m + 1)) => kFinset.Ici j, X (i, k) ; fun (x : Fin (m + 1)) => ]) + D[fun (i : Fin (m + 1)) => X (i, m) ; fun (x : Fin (m + 1)) => ] - D[fun (i : Fin (m + 1)) => j : Fin (m + 1), X (i, j) ; fun (x : Fin (m + 1)) => ]

              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}.