`PFR/MoreRuzsaDist.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 9 curated AI-written annotations and 485 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

60 declarations, 0 contain sorry, 0 declared as axioms

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 Kaimanovich-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_sub_zsmul_sub_ent_le: Controlling H[X - aY] in terms of H[X] and d[X ; Y].

Imports (6)

Imported by 2 files

lemma rdist_of_neg_le If X, Y are G-valued, then d[X;-Y] ≤ 3 d[X;Y] line 55 source
Source documentation
If X, Y are G-valued, then d[X;-Y] ≤ 3 d[X;Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, MeasureTheory.IsProbabilityMeasure, Measurable, Finite, LE.le, Real, rdist, Neg.neg, HMul.hMul, OfNat.ofNat, Nat
Proof uses: Prod, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies, Eq.mpr, id, Eq, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.neg, ProbabilityTheory.CondIndepFun, prod, HSub.hSub, ProbabilityTheory.condIndep_copies, Measurable.prodMk, Measurable.sub, Prod.fst and 157 more
172 instances, coercions and auxiliary constants left out.

Tactic trace: 183 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_of_neg_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (hX : Measurable X)
    (hY : Measurable Y) [Finite G] :
    d[X ; μ # -Y ; μ'] ≤ 3 * d[X ; μ # Y ; μ'] := by
…
```
lemma kvm_ineq_I If n ≥ 0 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then H[Y i₀ + ∑ i ∈ s, Y i; μ] - H[Y i₀; μ] ≤ ∑ i ∈ s, (H[Y i₀ + Y i; μ] - H[Y i₀; μ]) line 301 source
Source documentation
If n ≥ 0 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then H[Y i₀ + ∑ i ∈ s, Y i; μ] - H[Y i₀; μ] ≤ ∑ i ∈ s, (H[Y i₀ + Y i; μ] - H[Y i₀; μ]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, Finset, Not, Membership.mem, FiniteRange, Measurable, ProbabilityTheory.iIndepFun, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HAdd.hAdd, Finset.sum
Proof uses: Finset.induction_on, Classical.propDecidable, Eq, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, OfNat.ofNat, True, congr, congrArg, congrFun', autoParam, add_zero, sub_self, Finset.sum_sub_distrib, HSMul.hSMul, Nat, Finset.card, Finset.sum_const, zero_nsmul and 95 more
118 instances, coercions and auxiliary constants left out.

Tactic trace: 37 steps
Open to load the checked before-and-after goal states.
```
lemma kvm_ineq_I {I : Type*} {i₀ : I} {s : Finset I} (hs : ¬ i₀ ∈ s)
    {Y : I → Ω → G} [∀ i, FiniteRange (Y i)] (hY : ∀ i, Measurable (Y i))
    (h_indep : iIndepFun Y μ) :
    H[Y i₀ + ∑ i ∈ s, Y i ; μ] - H[Y i₀ ; μ] ≤ ∑ i ∈ s, (H[Y i₀ + Y i ; μ] - H[Y i₀ ; μ]) := by
…
```
Mentions: FiniteRange
lemma kvm_ineq_II If n ≥ 1 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ] line 342 source
Source documentation
If n ≥ 1 and X, Y₁, ..., Yₙ are jointly independent G-valued random variables, then d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, Finset, Not, Membership.mem, Finset.Nonempty, FiniteRange, Measurable, ProbabilityTheory.iIndepFun, LE.le, Real, rdist, Finset.sum, HMul.hMul, OfNat.ofNat, Nat
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, ite, Eq, Classical.propDecidable, id, Neg.neg, Measurable.of_discrete, Function.comp, Measurable.comp, ProbabilityTheory.IndepFun, ProbabilityTheory.IndepFun.symm, ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem, Prod, HAdd.hAdd, HDiv.hDiv, HSub.hSub, ProbabilityTheory.entropy, Trans.trans, Eq.mpr and 189 more
214 instances, coercions and auxiliary constants left out.

Tactic trace: 53 steps
Open to load the checked before-and-after goal states.
```
lemma kvm_ineq_II {I : Type*} {i₀ : I} {s : Finset I} (hs : ¬ i₀ ∈ s)
    (hs' : Finset.Nonempty s) {Y : I → Ω → G} [∀ i, FiniteRange (Y i)]
    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :
    d[Y i₀; μ # ∑ i ∈ s, Y i; μ] ≤ 2 * ∑ i ∈ s, d[Y i₀; μ # Y i; μ] := by
…
```
Mentions: FiniteRange
lemma kvm_ineq_III_aux line 422 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, FiniteRange, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real, rdist, HAdd.hAdd, HMul.hMul, Inv.inv and 2 more
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, ProbabilityTheory.IndepFun, Eq.mpr, eq_of_heq, Eq, autoParam, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HAdd, ProbabilityTheory.iIndepFun.indepFun_add_right, Prod, List, List.Mem, List.finRange, Membership.mem, Finset and 111 more
141 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma kvm_ineq_III_aux' strengthen the above lemma by not requiring X to be independent of Y, Z line 438 source
Source documentation
strengthen the above lemma by not requiring X to be independent of Y, Z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, FiniteRange, Measurable, ProbabilityTheory.IndepFun, MeasureTheory.IsProbabilityMeasure, LE.le, Real, rdist, HAdd.hAdd, HMul.hMul, Inv.inv, OfNat.ofNat, Nat, HSub.hSub, ProbabilityTheory.entropy
Proof uses: Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies3_nondep_finiteRange, Prod, prod, ProbabilityTheory.IdentDistrib.mk, AEMeasurable.prodMk, Measurable.aemeasurable, ProbabilityTheory.iIndepFun.indepFun, Ne, of_eq_true, Not, Eq, Eq.trans and 31 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma kvm_ineq_III_aux' {X Y Z : Ω → G} [FiniteRange X] [FiniteRange Y]
    [FiniteRange Z] (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (h_indep : IndepFun Y Z μ) [IsProbabilityMeasure μ] :
  d[X; μ # Y + Z; μ] ≤ d[X; μ # Y; μ] + (2 : ℝ)⁻¹ * (H[Y + Z; μ] - H[Y; μ]) := by
…
```
Mentions: FiniteRange
lemma kvm_ineq_III 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₁]) line 464 source
Source documentation
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₁]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, Finset, Not, Membership.mem, Ne, FiniteRange, Measurable, ProbabilityTheory.iIndepFun, LE.le, Real, rdist, HAdd.hAdd, Finset.sum, HMul.hMul, Inv.inv, OfNat.ofNat and 3 more
Proof uses: Fin, Matrix.vecCons, Singleton.singleton, Matrix.vecEmpty, Set.PairwiseDisjoint, Set.univ, Set, id, Function.onFun, Disjoint, List, List.Mem, Eq, List.finRange, HEq, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk and 48 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma kvm_ineq_III {I : Type*} {i₀ i₁ : I} {s : Finset I}
    (hs₀ : ¬ i₀ ∈ s) (hs₁ : ¬ i₁ ∈ s) (h01 : i₀ ≠ i₁)
    (Y : I → Ω → G) [∀ i, FiniteRange (Y i)]
    (hY : ∀ i, Measurable (Y i)) (h_indep : iIndepFun Y μ) :
    d[Y i₀; μ # Y i₁ + ∑ i ∈ s, Y i; μ]
      ≤ d[Y i₀; μ # Y i₁; μ] + (2 : ℝ)⁻¹ * (H[Y i₁ + ∑ i ∈ s, Y i; μ] - H[Y i₁; μ]) := by
…
```
Mentions: FiniteRange
theorem entropy_kvm_step line 490 source
theorem entropy_sum_le_entropy_neg_add line 538 source
theorem kvm_decomposition_indep_helper line 549 source
theorem entropy_kvm_decomposition line 592 source
lemma ent_of_sum_le_ent_of_sum 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, line 633 source
Source documentation
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)}].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, Finset, Disjoint, Measurable, FiniteRange, ProbabilityTheory.iIndepFun, LE.le, Finset.image, Classical.propDecidable, Eq, Real, ProbabilityTheory.entropy, Finset.sum, HAdd.hAdd, HSub.hSub
Proof uses: Eq.mpr, id, congrArg, rfl, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, of_eq_true, Eq.trans, True, congrFun', Finset.sum_apply, eq_self, Finset.measurable_sum, Prod, Membership.mem, Trans.trans and 16 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
```
lemma ent_of_sum_le_ent_of_sum {I : Type*} {s t : Finset I} (hdisj : Disjoint s t)
    (X : I → Ω → G) (hX : ∀ i, Measurable (X i)) [∀ i, FiniteRange (X i)]
    (hindep : iIndepFun X μ) (f : I → I) (hf : Finset.image f t ⊆ s) :
    H[∑ i ∈ t, X i; μ] ≤ H[∑ i ∈ s, X i; μ] + ∑ i ∈ t, (H[ X i - X (f i); μ] - H[X (f i); μ]) := by
…
```
Mentions: FiniteRange
lemma ent_sub_zsmul_le Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer line 686 source
Source documentation
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]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, Int, LE.le, Real, ProbabilityTheory.entropy and 3 more
Proof uses: Eq.mpr, id, Eq, congrArg, add_smul, one_smul, add_comm, sub_add_eq_sub_sub, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_eq_true, Not, Eq.trans, False, True, eq_false_of_decide, Eq.refl, Bool, Bool.false and 43 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma ent_sub_zsmul_le {Y : Ω → G} {X' : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange X']
    [IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X')
    (h_indep : iIndepFun ![X, Y, X'] μ) (hident : IdentDistrib X X' μ μ) {a : ℤ} :
    H[X - (a+1) • Y; μ] ≤ H[X - a • Y; μ] + H[X - Y - X'; μ] - H[X; μ] := by
…
```
Mentions: FiniteRange
lemma ent_sub_nsmul_le Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer line 712 source
Source documentation
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]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, LE.le, Real, ProbabilityTheory.entropy, HSub.hSub and 2 more
Proof uses: cast, Int, Eq.trans, congrFun', congrArg, autoParam, Eq.symm, Nat.cast_one, congr, Nat.cast_smul_eq_nsmul, ent_sub_zsmul_le
50 instances, coercions and auxiliary constants left out.
```
lemma ent_sub_nsmul_le {Y : Ω → G} {X' : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange X']
    [IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X')
    (h_indep : iIndepFun ![X, Y, X'] μ) (hident : IdentDistrib X X' μ μ) {a : ℕ} :
    H[X - (a + 1) • Y; μ] ≤ H[X - a • Y; μ] + H[X - Y - X'; μ] - H[X; μ] :=
…
```
Mentions: FiniteRange
lemma ent_of_sub_smul' Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer line 720 source
Source documentation
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]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, Int, LE.le, Real, ProbabilityTheory.entropy and 3 more
Proof uses: Eq.mpr, id, Eq, congrArg, sub_smul, one_smul, Neg.neg, sub_eq_add_neg, neg_sub, add_sub, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, Ne, of_eq_true, Not, Eq.trans, False, True, eq_false_of_decide, Eq.refl and 53 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
```
lemma ent_of_sub_smul' {Y : Ω → G} {X' : Ω → G} [FiniteRange X] [FiniteRange Y] [FiniteRange X']
    [IsProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X')
    (h_indep : iIndepFun ![X, Y, X'] μ) (hident : IdentDistrib X X' μ μ) {a : ℤ} :
    H[X - (a-1) • Y; μ] ≤ H[X - a • Y; μ] + H[X - Y - X'; μ] - H[X; μ] := by
…
```
Mentions: FiniteRange
lemma ent_sub_zsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be an integer line 762 source
Source documentation
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].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, MeasureTheory.IsProbabilityMeasure, Finite, Measurable, ProbabilityTheory.IndepFun, Int, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HSMul.hSMul, HMul.hMul, OfNat.ofNat, Nat, abs, rdist
Proof uses: Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies3_nondep, ProbabilityTheory.iIndepFun.indepFun, Ne, of_eq_true, Not, Eq, Eq.trans, False, True, congrArg, not_false_eq_true, eq_false_of_decide and 185 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 92 steps
Open to load the checked before-and-after goal states.
```
lemma ent_sub_zsmul_sub_ent_le {Y : Ω → G} [IsProbabilityMeasure μ] [Finite G]
    (hX : Measurable X) (hY : Measurable Y) (h_indep : IndepFun X Y μ) {a : ℤ} :
    H[X - a • Y; μ] - H[X; μ] ≤ 4 * |a| * d[X ; μ # Y ; μ] := by
…
```
lemma ent_sub_nsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be a natural number line 869 source
Source documentation
Let X,Y be independent G-valued random variables, and let a be a natural number. Then H[X - aY] - H[X] ≤ 4 a d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, MeasureTheory.IsProbabilityMeasure, Finite, Measurable, ProbabilityTheory.IndepFun, Nat, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HSMul.hSMul, HMul.hMul, OfNat.ofNat, rdist
Proof uses: Eq.mpr, HAdd.hAdd, id, Eq, Eq.mp, Int, abs, Eq.trans, congr, congrArg, congrFun', autoParam, natCast_zsmul, Nat.abs_cast, Int.cast_natCast, ent_sub_zsmul_sub_ent_le
68 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma ent_sub_nsmul_sub_ent_le {Y : Ω → G} [IsProbabilityMeasure μ] [Finite G]
    (hX : Measurable X) (hY : Measurable Y) (h_indep : IndepFun X Y μ) {a : ℕ} :
    H[X - a • Y ; μ] - H[X ; μ] ≤ 4 * a * d[X ; μ # Y ; μ] := by
…
```
lemma ent_add_nsmul_sub_ent_le Let X,Y be independent G-valued random variables, and let a be a natural number line 876 source
Source documentation
Let X,Y be independent G-valued random variables, and let a be a natural number. Then H[X + aY] - H[X] ≤ 4 a d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, AddCommGroup, Countable, MeasureTheory.IsProbabilityMeasure, Finite, Measurable, ProbabilityTheory.IndepFun, Nat, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HAdd.hAdd, HSMul.hSMul, HMul.hMul, OfNat.ofNat, rdist
Proof uses: Eq.mpr, id, Eq, Eq.mp, Int, Neg.neg, abs, Eq.trans, congr, congrArg, congrFun', autoParam, neg_smul, natCast_zsmul, sub_neg_eq_add, abs_neg, Nat.abs_cast, Int.cast_natCast, ent_sub_zsmul_sub_ent_le
97 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma ent_add_nsmul_sub_ent_le {Y : Ω → G} [IsProbabilityMeasure μ] [Finite G]
    (hX : Measurable X) (hY : Measurable Y) (h_indep : IndepFun X Y μ) {a : ℕ} :
    H[X + a • Y ; μ] - H[X ; μ] ≤ 4 * a * d[X ; μ # Y ; μ] := by
…
```
def multiDist Let X_[m] = (X₁, ..., Xₘ) be a non-empty finite tuple of G-valued random variables X_i line 890 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, Real
Proof uses: HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, MeasureTheory.MeasureSpace.volume, HMul.hMul, Inv.inv
12 instances, coercions and auxiliary constants left out.
```
@[expose] noncomputable def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, Ω i → G) : ℝ :=
…
```
lemma multiDist_copy If X_i has the same distribution as Y_i for each i, then D[X_[m]] = D[Y_[m]] line 897 source
Source documentation
If X_i has the same distribution as Y_i for each i, then D[X_[m]] = D[Y_[m]].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, Eq, Real, multiDist
Proof uses: id, Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, HMul.hMul, Inv.inv, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, ProbabilityTheory.IdentDistrib.entropy_congr, of_eq_true, Eq.trans, True and 4 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩ' : ∀ i, MeasureSpace (Ω' i))
    (X : ∀ i, Ω i → G) (X' : ∀ i, (Ω' i) → G)
    (hident : ∀ i, IdentDistrib (X i) (X' i)) :
    D[X ; hΩ] = D[X' ; hΩ'] := by
…
```
theorem MeasureTheory.Measure.map_of_pi Move to Mathlib? line 908 source
Source documentation
Move to Mathlib?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, Eq, MeasureTheory.Measure.map, MeasureTheory.Measure.pi
Proof uses: Eq.symm, MeasureTheory.Measure.pi_eq, Set, MeasurableSet, Eq.mpr, ENNReal, Set.pi, Set.univ, Finset.prod, Finset.univ, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Measurable.of_eval, Measurable.fun_comp, measurable_pi_apply, MeasurableSet.univ_pi, Eq.refl, congrFun' and 10 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem MeasureTheory.Measure.map_of_pi {ι : Type*} [Fintype ι]
    {α : ι → Type*} [∀ i, MeasurableSpace (α i)]
    {β : ι → Type*} [∀ i, MeasurableSpace (β i)]
    (μ : ∀ i, Measure (α i)) [∀ i, IsProbabilityMeasure (μ i)]
    {f : ∀ i, α i → β i} (hf : ∀ i, Measurable (f i)) :
  map (fun x i => f i (x i)) (.pi μ) =
    Measure.pi (fun i => map (f i) (μ i)) := by
…
```
lemma multiDist_indep 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] line 925 source
Source documentation
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].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fin, Measurable, ProbabilityTheory.iIndepFun, Eq, Real, multiDist, HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, HDiv.hDiv
Proof uses: Eq.mpr, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, MeasureTheory.Measure.pi, id, Eq.trans, congrFun', congrArg, HMul.hMul, Inv.inv, inv_mul_eq_div, MeasureTheory.Measure, Eq.rec, Eq.refl, Eq.symm, Eq.mp, propext, ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map, Measurable.aemeasurable, Function.comp and 17 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma multiDist_indep {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) [IsProbabilityMeasure hΩ.volume]
    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) :
    D[X ; fun _ ↦ hΩ] = H[∑ i, X i] - (∑ i, H[X i]) / m := by
…
```
lemma multiDist_nonneg_of_indep line 936 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Finite, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fin, Measurable, ProbabilityTheory.iIndepFun, LE.le, Real, OfNat.ofNat, multiDist
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, HDiv.hDiv, id, Eq, congrArg, multiDist_indep, ProbabilityTheory.iIndepFun.isProbabilityMeasure, dite, Eq.trans, congr, congrFun', MeasureTheory.Measure, autoParam, Finset.sum_congr, EmptyCollection.emptyCollection, Finset and 71 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma multiDist_nonneg We have D[X_[m]] ≥ 0 line 957 source
Source documentation
We have D[X_[m]] ≥ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Finite, Nat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, LE.le, Real, OfNat.ofNat, multiDist
Proof uses: Exists, MeasureTheory.Measure, And, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies', Eq.mpr, MeasureTheory.MeasureSpace.mk, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, multiDist_copy, ProbabilityTheory.IdentDistrib.symm, And.right, multiDist_nonneg_of_indep, And.left
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma multiDist_nonneg [Finite G] {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (hprob : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) (X : ∀ i, Ω i → G)
    (hX : ∀ i, Measurable (X i)) :
    0 ≤ D[X ; hΩ] := by
…
```
lemma multiDist_of_perm If φ : {1, ..., m} → {1, ...,m} is a bijection, then D[X_[m]] = D[(X_φ(1), ..., X_φ(m))] line 967 source
Source documentation
If φ : {1, ..., m} → {1, ...,m} is a bijection, then D[X_[m]] = D[(X_φ(1), ..., X_φ(m))].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Equiv.Perm, Eq, Real, multiDist
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, HMul.hMul, Inv.inv, id, congrFun', congrArg, Finset.sum_congr, Eq.refl, Finset, Membership.mem, HSub, Eq.rec, ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.mk and 36 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 43 steps
Open to load the checked before-and-after goal states.
```
lemma multiDist_of_perm {m : ℕ} {Ω : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i)) (hΩprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)
    (X : ∀ i, Ω i → G) (φ : Equiv.Perm (Fin m)) :
    D[fun i ↦ X (φ i); fun i ↦ hΩ (φ i)] = D[X ; hΩ] := by
…
```
abbrev offDiag_sum The sum of f away from the diagonal line 1016 source
Source documentation
The sum of f away from the diagonal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real
Proof uses: Finset.sum, Finset.univ, ite, Eq, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
```
abbrev offDiag_sum {m : ℕ} (f : Fin m → Fin m → ℝ) := ∑ j, ∑ k, (if j = k then (0:ℝ) else f j k)
```
lemma offDiag_sum_left line 1018 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Fin, Real, Eq, offDiag_sum, HMul.hMul, HSub.hSub, Finset.sum, Finset.univ
Proof uses: Eq.mpr, id, congrArg, Finset.mul_sum, Finset.sum_congr, ite, Eq.refl, Finset, Membership.mem, Or, Finset.card, Finset.filter, Not, Eq.trans, congrFun', HAdd.hAdd, ite_congr, Finset.sum_ite, congr, Finset.sum_const_zero and 33 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_right line 1030 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Fin, Real, Eq, offDiag_sum, HMul.hMul, HSub.hSub, Finset.sum, Finset.univ
Proof uses: Eq.mpr, id, congrArg, Eq.symm, offDiag_sum_left, ite, eq_of_heq, HEq, Eq.refl, HEq.refl, Finset.sum_congr, Finset, Membership.mem, congr, ite_congr, Not, dite, congrFun', ite_eq_left, of_eq_true and 10 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_const line 1036 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GE.ge, OfNat.ofNat, Real, Eq, offDiag_sum, Fin, HMul.hMul, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.univ, id, congrArg, offDiag_sum_left, congrFun', Eq.trans, HSMul.hSMul, Finset.card, Finset.sum_const, Fintype.card_fin, nsmul_eq_mul, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring and 36 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_add line 1042 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, offDiag_sum, HAdd.hAdd
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, OfNat.ofNat, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true and 7 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_sub line 1049 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, offDiag_sum, HSub.hSub
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, OfNat.ofNat, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true and 7 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_div line 1056 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, offDiag_sum, HDiv.hDiv
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, OfNat.ofNat, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true and 7 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma offDiag_mul_sum line 1063 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Eq, offDiag_sum, HMul.hMul
Proof uses: Eq.mpr, Finset.sum, Finset.univ, ite, OfNat.ofNat, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma offDiag_sum_le line 1070 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, Real, Ne, LE.le, offDiag_sum
Proof uses: Finset.sum_le_sum, Finset.sum, Finset.univ, ite, Eq, OfNat.ofNat, Membership.mem, Finset, dite, of_eq_true, Eq.trans, True, congr, congrArg, ite_eq_left_of_eq_true, congrFun', eq_self, Not, ite_eq_right_of_eq_false, eq_false and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma multidist_ruzsa_I_indep To prove multidist_ruzsa_I, we first establish a special case when the random variables are defined on the same space and are jointly independent line 1081 source
Source documentation
To prove multidist_ruzsa_I, we first establish a special case when the random variables are defined on the same space and are jointly independent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fin, ProbabilityTheory.iIndepFun, Measurable, FiniteRange, LE.le, Real, Finset.sum, Finset.univ, ite, Eq and 5 more
Proof uses: Ne, ProbabilityTheory.entropy, HAdd.hAdd, Compl.compl, Finset, Insert.insert, Singleton.singleton, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_compl_add_sum, add_comm, HAdd, Eq.rec, Eq.refl, of_eq_true, Eq.trans, True, congrFun' and 204 more
223 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_I_indep {m : ℕ} (hm : m ≥ 1) {Ω : Type*} (hΩ : MeasureSpace Ω)
    [IsProbabilityMeasure (hΩ.volume)] (X : Fin m → Ω → G) (h_indep : iIndepFun X)
    (hmes : ∀ j, Measurable (X j)) (hfin : ∀ j, FiniteRange (X j)) :
    ∑ j, ∑ k, (if j = k then (0:ℝ) else d[X j # -X k]) ≤ m * (m - 1) * D[X; fun _ ↦ hΩ] := by
…
```
Mentions: FiniteRange
lemma multidist_ruzsa_I Let m ≥ 1, and let X_[m] be a tuple of G-valued random variables line 1140 source
Source documentation
Let m ≥ 1, 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]].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, Fin, MeasureTheory.MeasureSpace, Measurable, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, FiniteRange, LE.le, Real, Finset.sum, Finset.univ, ite, Eq, rdist and 4 more
Proof uses: Exists, MeasureTheory.Measure, And, ProbabilityTheory.iIndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies'_finiteRange, Eq.mpr, MeasureTheory.MeasureSpace.mk, eq_of_heq, LE, HEq, Eq.refl, HEq.refl, Eq.symm, Finset.sum_congr, Finset, Membership.mem, ite_congr, Not, ProbabilityTheory.IdentDistrib.rdist_congr and 10 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_I {m : ℕ} (hm : m ≥ 1) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    {X : ∀ i, Ω i → G} (hmes : ∀ j, Measurable (X j))
    (hprob : ∀ j, IsProbabilityMeasure (hΩ j).volume) (hfin : ∀ j, FiniteRange (X j)) :
    ∑ j, ∑ k, (if j = k then (0:ℝ) else d[X j # -X k]) ≤ m * (m - 1) * D[X; hΩ] := by
…
```
Mentions: FiniteRange
lemma multidist_ruzsa_II Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables line 1157 source
Source documentation
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]].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, FiniteRange, LE.le, Real, Finset.sum, Finset.univ, rdist, HMul.hMul, multiDist
Proof uses: Ne, Neg.neg, Trans.trans, Eq, HAdd.hAdd, rdist_triangle, Measurable.neg, HAdd, Eq.rec, Eq.refl, rdist_symm, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg and 125 more
170 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_II {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) (X : ∀ i, Ω i → G)
    (hmes : ∀ i, Measurable (X i)) (hfin : ∀ i, FiniteRange (X i)) :
    ∑ j, d[X j # X j] ≤ 2 * m * D[X; hΩ] := by
…
```
Mentions: FiniteRange
lemma multidist_ruzsa_III' A version of multidist_ruzsa_III assuming independence line 1184 source
Source documentation
A version of multidist_ruzsa_III assuming independence.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, MeasureTheory.MeasureSpace, Fin, HAdd.hAdd, Measurable, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.iIndepFun, FiniteRange, MeasureTheory.IsProbabilityMeasure, LE.le, Real, multiDist, Fin.init and 3 more
Proof uses: Fin.last, Finset.sum, Finset.univ, Eq, ProbabilityTheory.entropy, ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun, of_eq_true, Not, Eq.trans, False, True, congrArg, not_false_eq_true, Finset, Finset.Iio, Singleton.singleton, Disjoint, Membership.mem and 190 more
189 instances, coercions and auxiliary constants left out.

Tactic trace: 93 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_III' {m : ℕ} (hm : m ≥ 2) {Ω : Type*} {hΩ : MeasureSpace Ω}
    {X : Fin (m + 1) → Ω → G} (hmes : ∀ i, Measurable (X i))
    (hident : ∀ j k, IdentDistrib (X j) (X k)) (hindep : iIndepFun X)
    (hfin : ∀ i, FiniteRange (X i)) [IsProbabilityMeasure (ℙ : Measure Ω)] (i₀ : Fin m) :
    D[Fin.init X ; fun _ ↦ hΩ] ≤ m * d[X i₀.castSucc # X i₀.castSucc] := by
…
```
Mentions: FiniteRange
lemma multidist_ruzsa_III Let I be an indexing set of size m ≥ 2, and let X_[m] be a tuple of G-valued random variables line 1265 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, Fin, MeasureTheory.MeasureSpace, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, Measurable, MeasureTheory.IsProbabilityMeasure, FiniteRange, LE.le, Real, multiDist, HMul.hMul, rdist
Proof uses: NeZero, Eq.mpr, Ne, id, Eq, congrArg, propext, neZero_iff, Not.intro, Mathlib.Tactic.Linarith.lt_irrefl, Int, Eq.mp, LT.lt, HAdd.hAdd, Neg.neg, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast and 69 more
91 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_III {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (X : ∀ i, Ω i → G) (hident : ∀ j k, IdentDistrib (X j) (X k)) (hmes : ∀ i, Measurable (X i))
    (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume) (hfin : ∀ i, FiniteRange (X i)) (i₀ : Fin m) :
    D[X; hΩ] ≤ m * d[X i₀ # X i₀] := by
…
```
Mentions: FiniteRange
lemma multidist_ruzsa_IV Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables line 1288 source
Source documentation
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].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, GE.ge, OfNat.ofNat, MeasureTheory.MeasureSpace, Fin, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, Measurable, MeasureTheory.IsProbabilityMeasure, FiniteRange, LE.le, Real, rdist, Finset.sum, Finset.univ, Neg.neg and 3 more
Proof uses: Prod, Exists, MeasureTheory.Measure, And, ProbabilityTheory.IdentDistrib, Prod.snd, ProbabilityTheory.independent_copies'_finiteRange, And.left, MeasureTheory.MeasureSpace.mk, Prod.mk, ProbabilityTheory.IdentDistrib.iprodMk, And.right, ProbabilityTheory.iIndepFun.precomp, Prod.mk_right_injective, Eq.mpr, Function.comp, eq_of_heq, Eq, autoParam, HEq and 275 more
287 instances, coercions and auxiliary constants left out.

Tactic trace: 238 steps (first 200 of 238)
Open to load the checked before-and-after goal states.
```
lemma multidist_ruzsa_IV {m : ℕ} (hm : m ≥ 2) {Ω : Type u} [MeasureSpace Ω] (X : Fin m → Ω → G)
    (h_indep : iIndepFun X) (hmes : ∀ i, Measurable (X i)) [IsProbabilityMeasure (ℙ : Measure Ω)]
    (hfin : ∀ i, FiniteRange (X i)) :
    d[∑ i, X i # - ∑ i, X i] ≤ 2 * D[X; fun _ ↦ inferInstance] := by
…
```
Mentions: FiniteRange
lemma multidist_eq_zero 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 line 1507 source
Source documentation
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.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Finite, Nat, GE.ge, OfNat.ofNat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Eq, Real, multiDist, Measurable, FiniteRange, Exists, AddSubgroup, And and 2 more
Proof uses: Finset.sum, Finset.univ, le_antisymm, LE.le, HMul.hMul, multidist_ruzsa_II, Eq.mpr, id, Eq.mp, congrArg, Eq.trans, MulZeroClass.mul_zero, Finset.sum_nonneg, Membership.mem, Finset, rdist_nonneg, exists_isUniform_of_rdist_eq_zero, Prod, propext, Finset.sum_eq_zero_iff_of_nonneg and 3 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma multidist_eq_zero [Finite G] {m : ℕ} (hm : m ≥ 2) {Ω : Fin m → Type*}
    (hΩ : ∀ i, MeasureSpace (Ω i)) (hprob : ∀ i, IsProbabilityMeasure (hΩ i).volume)
    (X : ∀ i, Ω i → G) (hvanish : D[X; hΩ] = 0) (hmes : ∀ i, Measurable (X i))
    (hfin : ∀ i, FiniteRange (X i)) (i) :
    ∃ (H : AddSubgroup G) (U : Ω i → G), Measurable U ∧ IsUniform H U ∧ d[X i # U] = 0 := by
…
```
Mentions: FiniteRange
def condMultiDist line 1535 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, Fintype, Real
Proof uses: Finset.sum, Finset.univ, HMul.hMul, Finset.prod, MeasureTheory.Measure.real, MeasureTheory.MeasureSpace.volume, Set.preimage, Singleton.singleton, Set, multiDist, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond
9 instances, coercions and auxiliary constants left out.
theorem condMultiDist_of_inj Conditional multidistance is unchanged if we apply an injection to the conditioned variables line 1543 source
Source documentation
Conditional multidistance is unchanged if we apply an injection to the conditioned variables

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, Fintype, Function.Injective, Eq, Real, condMultiDist, Function.comp
Proof uses: Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, Finset.prod, MeasureTheory.Measure.real, MeasureTheory.MeasureSpace.volume, Set.preimage, Singleton.singleton, Set, multiDist, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, Fintype.sum_of_injective, Function.Injective.comp_left and 44 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
theorem condMultiDist_of_inj {G : Type*} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ}
    {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i)) {S : Type*} [Fintype S] {T : Type*}
    [Fintype T] (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) {f : S → T} (hf : Injective f) :
    D[X | fun i ↦ f ∘ (Y i); hΩ] = D[X | fun i ↦ Y i; hΩ] := by
…
```
theorem condMultiDist_of_const Conditional multidistance against a constant is just multidistance line 1567 source
Source documentation
Conditional multidistance against a constant is just multidistance

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fintype, Eq, Real, condMultiDist, multiDist
Proof uses: id, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, Finset.prod, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond, congrArg, Finset.sum_eq_single, Membership.mem, Finset, Ne, OfNat.ofNat, eq_of_heq, HEq and 37 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
theorem condMultiDist_of_const {G : Type*} [hG : MeasurableSpace G] [AddCommGroup G] {m : ℕ}
    {Ω : Fin m → Type*} [hΩ : ∀ i, MeasureSpace (Ω i)] [∀ i, IsProbabilityMeasure (hΩ i).volume]
    {S : Type*} [Fintype S] (c : Fin m → S) (X : ∀ i, Ω i → G) :
    D[X | fun i ↦ fun _ ↦ c i; hΩ] = D[X ; hΩ] := by
…
```
theorem condMultiDist_nonneg Conditional multidistance is nonnegative line 1591 source
Source documentation
Conditional multidistance is nonnegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Finite, Nat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Fintype, Measurable, LE.le, Real, OfNat.ofNat, condMultiDist
Proof uses: id, Finset.sum_nonneg, HMul.hMul, Finset.prod, Finset.univ, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, multiDist, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond, Membership.mem, Finset, dite, Ne, ENNReal, MeasureTheory.Measure, Eq, mul_nonneg and 27 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem condMultiDist_nonneg [Finite G] {m : ℕ} {Ω : Fin m → Type*} (hΩ : ∀ i, MeasureSpace (Ω i))
    (hprob : ∀ i, IsProbabilityMeasure (ℙ : Measure (Ω i))) {S : Type*} [Fintype S]
    (X : ∀ i, Ω i → G) (Y : ∀ i, Ω i → S) (hX : ∀ i, Measurable (X i)) : 0 ≤ D[X | Y; hΩ] := by
…
```

lemma Finset.prod_mul A technical lemma: can push a constant into a product at a specific term line 1613 source

Source documentation

A technical lemma: can push a constant into a product at a specific term

private lemma Finset.prod_mul {α β : Type*} [Fintype α] [DecidableEq α] [CommMonoid β] (f : α → β)
    (c : β) (i₀ : α) : (∏ i, f i) * c = ∏ i, if i = i₀ then f i * c else f i := calc
…

lemma mes_of_comap line 1626 source

lemma ident_of_cond_of_indep A technical lemma: two different ways of conditioning independent variables gives identical distributions line 1633 source

Source documentation

A technical lemma: two different ways of conditioning independent variables gives identical distributions

private lemma ident_of_cond_of_indep
    {G : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G] [Countable G]
    {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Finite 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 : iIndepFun (fun i ↦ ⟨X i, Y i⟩))
    (y : Fin m → S) (i : Fin m) (hy : ∀ i, ℙ (Y i ⁻¹' {y i}) ≠ 0) :
    IdentDistrib (X i) (X i) (cond ℙ (Y i ⁻¹' {y i})) (cond ℙ (⋂ i, Y i ⁻¹' {y i})) where
…

lemma prob_nonzero_of_prod_prob_nonzero A technical lemma: if a product of probabilities is nonzero, then each probability is individually non-zero line 1658 source

Source documentation

A technical lemma: if a product of probabilities is nonzero, then each probability is individually non-zero

private lemma prob_nonzero_of_prod_prob_nonzero {m : ℕ}
    {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Finite S] [MeasurableSpace S] [MeasurableSingletonClass S]
    {Y : Fin m → Ω → S} {y : Fin m → S} (hf : ∏ i, (ℙ (Y i ⁻¹' {y i})).toReal ≠ 0) :
    ∀ i, ℙ (Y i ⁻¹' {y i}) ≠ 0 := by
…

lemma condMultiDist_eq 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] line 1670 source
Source documentation
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]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, MeasureTheory.MeasureSpace, Fintype, Fin, Measurable, ProbabilityTheory.iIndepFun, Prod, prod, MeasureTheory.MeasureSpace.volume, Eq, Real, condMultiDist, HSub.hSub, ProbabilityTheory.condEntropy, Finset.sum, Finset.univ and 1 more
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, Set, Set.preimage, Singleton.singleton, Set.iInter, Finset.prod, MeasureTheory.Measure.real, ENNReal.toReal, MeasureTheory.Measure, ENNReal, Trans.trans, Eq.mpr, id, congrArg, ENNReal.toReal_prod, Eq.refl, Eq.rec, Eq.symm, ProbabilityTheory.iIndepFun.meas_iInter and 77 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 73 steps
Open to load the checked before-and-after goal states.
```
lemma condMultiDist_eq {m : ℕ}
    {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]
    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i))
    {Y : Fin m → Ω → S} (hY : ∀ i, Measurable (Y i))
    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :
    D[X | Y ; fun _ ↦ hΩ] =
      H[fun ω ↦ ∑ i, X i ω | fun ω ↦ (fun i ↦ Y i ω)] - (∑ i, H[X i | Y i])/m := by
…
```
lemma condMultiDist_eq' 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] line 1756 source
Source documentation
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].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Countable, Nat, MeasureTheory.MeasureSpace, Fintype, Fin, Measurable, ProbabilityTheory.iIndepFun, Prod, prod, MeasureTheory.MeasureSpace.volume, Eq, Real, condMultiDist, Finset.sum, Finset.univ, HMul.hMul, ENNReal.toReal and 9 more
Proof uses: Eq.mpr, Finset.prod, MeasureTheory.Measure.real, id, congrArg, condMultiDist.eq_1, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, ProbabilityTheory.iIndepFun.meas_iInter, MeasurableSet.singleton, ENNReal.toReal_prod, dite, OfNat.ofNat, of_eq_true, Eq.trans, True, congr and 6 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma condMultiDist_eq' {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]
    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]
    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i)) {Y : Fin m → Ω → S}
    (hY : ∀ i, Measurable (Y i))
    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :
    D[X | Y ; fun _ ↦ hΩ] =
      ∑ y : Fin m → S, (ℙ (⋂ i, (Y i) ⁻¹' {y i})).toReal
        * D[X; fun _ ↦ ⟨cond ℙ (⋂ i, Y i ⁻¹' {y i})⟩] := by
…
```
lemma multiDist_chainRule Let π : G → H be a homomorphism of abelian groups and let X_[m] be a tuple of jointly independent G-valued random variables line 1784 source
Source documentation
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)).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Finite, Fintype, AddMonoidHom, Nat, MeasureTheory.MeasureSpace, Fin, Measurable, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, Eq, Real, multiDist, HAdd.hAdd, condMultiDist, Function.comp, ProbabilityTheory.condMutualInfo, Finset.sum and 1 more
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, Eq.mpr, id, congrArg, rfl, HDiv.hDiv, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, Finset.measurable_sum'', Prod, Membership.mem, Finset, Measurable.fun_comp, Prod.snd, Measurable.snd, measurable_id', propext, measurable_pi_iff, Measurable.comp and 103 more
127 instances, coercions and auxiliary constants left out.

Tactic trace: 57 steps
Open to load the checked before-and-after goal states.
```
lemma multiDist_chainRule {G H : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G]
    [AddCommGroup G] [Finite G] [hH : MeasurableSpace H]
    [MeasurableSingletonClass H] [AddCommGroup H]
    [Fintype H] (π : G →+ H) {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)
    {X : Fin m → Ω → G} (hmes : ∀ i, Measurable (X i))
    (h_indep : iIndepFun X) :
    D[X; fun _ ↦ hΩ] = D[X | fun i ↦ π ∘ X i; fun _ ↦ hΩ]
      + D[fun i ↦ π ∘ X i; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) | π ∘ (∑ i, X i)] := by
…
```
lemma cond_multiDist_chainRule Let π : G → H be a homomorphism of abelian groups line 1854 source
Source documentation
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]].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Finite, Fintype, AddMonoidHom, Nat, MeasureTheory.MeasureSpace, Fin, Measurable, ProbabilityTheory.iIndepFun, Prod, prod, MeasureTheory.MeasureSpace.volume, Eq, Real, condMultiDist, HAdd.hAdd, Function.comp, ProbabilityTheory.condMutualInfo and 2 more
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, Set, Set.iInter, Set.preimage, Singleton.singleton, ENNReal.toReal, MeasureTheory.Measure, ENNReal, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond, Trans.trans, HMul.hMul, multiDist, condMultiDist_eq', Eq.mpr, id, congrArg, Eq.trans, congrFun' and 99 more
111 instances, coercions and auxiliary constants left out.

Tactic trace: 147 steps
Open to load the checked before-and-after goal states.
```
lemma cond_multiDist_chainRule {G H : Type*} [hG : MeasurableSpace G] [MeasurableSingletonClass G]
    [AddCommGroup G] [Finite G]
    [hH : MeasurableSpace H] [MeasurableSingletonClass H] [AddCommGroup H]
    [Fintype H] (π : G →+ H)
    {S : Type*} [Fintype S] [hS : MeasurableSpace S] [MeasurableSingletonClass S]
    {m : ℕ} {Ω : Type*} [hΩ : MeasureSpace Ω]
    {X : Fin m → Ω → G} (hX : ∀ i, Measurable (X i))
    {Y : Fin m → Ω → S} (hY : ∀ i, Measurable (Y i))
    (h_indep : iIndepFun (fun i ↦ ⟨X i, Y i⟩)) :
    D[X | Y; fun _ ↦ hΩ] = D[X | fun i ↦ ⟨π ∘ X i, Y i⟩; fun _ ↦ hΩ]
      + D[fun i ↦ π ∘ X i | Y; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ π (X i ω)) |
…
```
lemma iter_multiDist_chainRule Let m be a positive integer line 2016 source
Source documentation
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])].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Fin, HAdd.hAdd, OfNat.ofNat, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Fintype, AddMonoidHom, Fin.succ, Fin.castSucc, Top.top, Eq, Function.comp, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, Real, condMultiDist and 6 more
Proof uses: Eq.mpr, id, congrArg, rfl, Finset, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', Finset.sum_congr, Membership.mem, Eq.refl, eq_self, LT.lt, LE.le, Finset.erase, Eq.symm, Finset.add_sum_erase, Finset.Iic and 28 more
103 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma iter_multiDist_chainRule {m : ℕ}
    {G : Fin (m + 1) → Type*}
    [hG : ∀ i, MeasurableSpace (G i)] [hGs : ∀ i, MeasurableSingletonClass (G i)]
    [∀ i, AddCommGroup (G i)] [hGcount : ∀ i, Fintype (G i)]
    {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc} {π : ∀ d, G ⊤ →+ G d}
    (hcomp: ∀ i : Fin m, π i.castSucc = (φ i) ∘ (π i.succ))
    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → G ⊤}
    (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) (n : Fin (m + 1)) :
    D[X | fun i ↦ (π 0) ∘ X i; fun _ ↦ hΩ] = D[X | fun i ↦ (π n) ∘ X i; fun _ ↦ hΩ]
      + ∑ d ∈ Finset.Iio n, (D[fun i ↦ (π (d+1)) ∘ X i | fun i ↦ (π d) ∘ X i; fun _ ↦ hΩ]
      + I[∑ i, X i : fun ω ↦ (fun i ↦ (π (d+1)) (X i ω)) |
            ⟨(π (d+1)) ∘ ∑ i, X i, fun ω ↦ (fun i ↦ (π d) (X i ω))⟩]) := by
…
```
lemma iter_multiDist_chainRule' 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)] line 2063 source
Source documentation
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)].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, Fin, HAdd.hAdd, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Fintype, AddMonoidHom, Fin.succ, Fin.castSucc, Top.top, Eq, Function.comp, MeasureTheory.MeasureSpace, Measurable, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, GE.ge and 6 more
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, Trans.trans, Prod, prod, Finset.Iio, Fin.last, Eq.mpr, id, congrArg, Eq.symm, condMultiDist_of_const, iter_multiDist_chainRule, le_add_of_nonneg_left, condMultiDist_nonneg, Fin.sum_univ_castSucc', Finset.sum_congr, Eq.refl, Finset, Membership.mem and 48 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma iter_multiDist_chainRule' {m : ℕ} (hm : m > 0)
    {G : Fin (m + 1) → Type*} [hG : ∀ i, MeasurableSpace (G i)]
    [hGs : ∀ i, MeasurableSingletonClass (G i)] [hGa : ∀ i, AddCommGroup (G i)]
    [hGcount : ∀ i, Fintype (G i)] {φ : ∀ i : Fin m, G (i.succ) →+ G i.castSucc}
    {π : ∀ d, G ⊤ →+ G d} (hπ0 : π 0 = 0) (hcomp : ∀ i : Fin m, π i.castSucc = φ i ∘ π i.succ)
    {Ω : Type*} [hΩ : MeasureSpace Ω] {X : Fin m → Ω → G ⊤}
    (hX : ∀ i, Measurable (X i)) (h_indep : iIndepFun X) :
    D[X; fun _ ↦ hΩ] ≥
      ∑ d : Fin m, D[fun i ↦ π d.succ ∘ X i | fun i ↦ π d.castSucc ∘ X i; fun _ ↦ hΩ]
      + I[∑ i : Fin m, X i : fun ω i ↦ π 1 (X i ω)| π 1 ∘ ∑ i : Fin m, X i] := by
…
```
theorem multiDist_of_hom' line 2117 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Finite, AddMonoidHom, Function.Injective, Nat, Fin, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, multiDist, HAdd.hAdd
Proof uses: id, HSub, Eq.rec, HSub.hSub, Eq.refl, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, Eq.mpr, ProbabilityTheory.measureEntropy, congrArg, rfl, forall_congr, implies_congr, eq_of_heq, HEq, HEq.refl, Eq.symm and 33 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 38 steps
Open to load the checked before-and-after goal states.
theorem multiDist_of_hom line 2145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Finite, AddMonoidHom, Function.Injective, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Nat, Fin, Measurable, Eq, Real, multiDist
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, HAdd.hAdd, OfNat.ofNat, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, of_eq_true, Eq.trans, True, congrArg, add_zero, eq_self, multiDist_of_hom'
30 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem multiDist_congr line 2156 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Nat, Fin, MeasureTheory.MeasureSpace, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure, MeasureTheory.MeasureSpace.volume, Eq, Real, multiDist
Proof uses: id, HSub, Eq.rec, HSub.hSub, Eq.refl, ProbabilityTheory.entropy, Finset.sum, Finset.univ, MeasureTheory.Measure.pi, MeasureTheory.Measure.map, Fintype, funext, MeasureTheory.Measure.map_congr, HMul.hMul, Inv.inv, HMul, AddCommMonoid, Finset, ProbabilityTheory.entropy_congr
17 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem condMultiDist_of_hom line 2164 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Finite, AddMonoidHom, Function.Injective, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Nat, Fin, Measurable, Eq, Real, condMultiDist, HAdd.hAdd
Proof uses: Nonempty, nonempty_fintype, Nonempty.intro, id, Finset.sum_congr, Finset.univ, HMul.hMul, Finset.prod, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, multiDist, MeasureTheory.MeasureSpace.mk, ProbabilityTheory.cond, rfl, Finset, Membership.mem, dite, Ne and 45 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
lemma cond_entropy_indep line 2193 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, MeasurableSingletonClass, Finite, Measurable, MeasureTheory.IsZeroOrProbabilityMeasure, MeasureTheory.MeasureSpace.volume, ProbabilityTheory.IndepFun, Prod, prod, Eq, Real, ProbabilityTheory.condEntropy
Proof uses: HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.chain_rule'', Measurable.prodMk, ProbabilityTheory.entropy_of_comp_eq_of_comp, Prod.mk, Prod.fst, Prod.snd, Eq.refl, HAdd.hAdd, ProbabilityTheory.IndepFun.entropy_pair_eq_add, ProbabilityTheory.IndepFun.comp, id, Measurable.snd, measurable_id', Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat and 49 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma cor_multiDist_chainRule Let G be an abelian group and let m ≥ 2 line 2223 source
Source documentation
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}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, AddCommGroup, Countable, Fintype, Nat, MeasureTheory.MeasureSpace, Prod, Fin, HAdd.hAdd, OfNat.ofNat, Measurable, ProbabilityTheory.iIndepFun, MeasureTheory.MeasureSpace.volume, MeasureTheory.IsProbabilityMeasure, LE.le, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ and 7 more
Proof uses: Fin.succ, ite, Eq, Fin.mk, of_eq_true, LT.lt, Eq.trans, True, eq_self, Fin.isLt, id, Decidable.byContradiction, Not, AddMonoidHom, AddMonoidHom.mk, ZeroHom.mk, funext, congrFun', congrArg, congrFun and 223 more
314 instances, coercions and auxiliary constants left out.

Tactic trace: 392 steps (first 200 of 392)
Open to load the checked before-and-after goal states.
```
lemma cor_multiDist_chainRule [Fintype G] {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω)
    (X : Fin (m + 1) × Fin (m + 1) → Ω → G) (hmes : ∀ i, Measurable (X i)) (h_indep : iIndepFun X)
    [IsProbabilityMeasure (ℙ : Measure Ω)]:
    I[fun ω ↦ (fun j ↦ ∑ i, X ⟨i, j⟩ ω) : fun ω ↦ (fun i ↦ ∑ j, X ⟨i, j⟩ ω) | ∑ p, X p]
      ≤ ∑ j : Fin m, (D[fun i ↦ X ⟨i, j.castSucc⟩; fun _ ↦ hΩ] - D[fun i ↦ X ⟨i, j.castSucc⟩ |
        fun i ↦ ∑ k ∈ Finset.Ici j.castSucc, X ⟨i, k⟩; fun _ ↦ hΩ]) +
          D[fun i ↦ X ⟨i, ⊤⟩; fun _ ↦ hΩ]
         - D[fun i ↦ ∑ j, X ⟨i, j⟩; fun _ ↦ hΩ] := by
…
```