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

67 declarations, 0 contain sorry, 0 declared as axioms

Ruzsa distance

Here we define Ruzsa distance and establish its basic properties.

Main definitions

rdist: The Ruzsa distance $d[X ; Y]$ between two random variables
condRuzsaDist: The conditional Ruzsa distance $d[X | Z ; Y | W]$ (or $d[X ; Y | W]$) between two random variables, conditioned on additional random variables

Main results

rdist_triangle: The Ruzsa triangle inequality for three random variables.
kaimanovich_vershik. $$H[X + Y + Z] - H[X + Y] \leq H[Y+ Z] - H[Y]$$
ent_bsg: If $Z=A+B$, then $$\sum_{z} P[Z=z] d[(A | Z = z) ; (B | Z = z)] \leq 3 I[A :B] + 2 H[Z] - H[A] - H[B]$$

Imports (5)

Imported by 6 files

lemma continuous_measureEntropy_probabilityMeasure Entropy depends continuously on the measure line 43 source
Source documentation
Entropy depends continuously on the measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Finite, TopologicalSpace, DiscreteTopology, MeasurableSpace, OpensMeasurableSpace, Continuous, MeasureTheory.ProbabilityMeasure, Real, ProbabilityTheory.measureEntropy
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, id, Eq.mpr, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, MeasureTheory.Measure, Inv.inv, Set, Set.univ, Singleton.singleton, SummationFilter.unconditional, Finset.sum, Finset.univ and 17 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma continuous_measureEntropy_probabilityMeasure {Ω : Type*} [Finite Ω]
    [TopologicalSpace Ω] [DiscreteTopology Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] :
    Continuous (fun (μ : ProbabilityMeasure Ω) ↦ measureEntropy (S := Ω) μ) := by
…
```
lemma continuous_entropy_restrict_probabilityMeasure line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Finite, TopologicalSpace, DiscreteTopology, BorelSpace, Continuous, MeasureTheory.ProbabilityMeasure, Real, ProbabilityTheory.entropy, id
Proof uses: Eq.mpr, ProbabilityTheory.measureEntropy, Eq, congrArg, funext, MeasureTheory.Measure.map, MeasureTheory.Measure, MeasureTheory.Measure.map_id, continuous_measureEntropy_probabilityMeasure
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def rdist line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, autoParam, MeasureTheory.Measure, Real
Proof uses: HSub.hSub, ProbabilityTheory.entropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, HDiv.hDiv, OfNat.ofNat
14 instances, coercions and auxiliary constants left out.
lemma rdist_def Explicit formula for the Ruzsa distance line 78 source
Source documentation
Explicit formula for the Ruzsa distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasureTheory.Measure, Eq, Real, rdist, HSub.hSub, ProbabilityTheory.entropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: rfl
14 instances, coercions and auxiliary constants left out.
```
lemma rdist_def (X : Ω → G) (Y : Ω' → G) (μ : Measure Ω) (μ' : Measure Ω') :
    d[X ; μ # Y ; μ']
      = H[fun x ↦ x.1 - x.2 ; (μ.map X).prod (μ'.map Y)] - H[X ; μ]/2 - H[Y ; μ']/2 := rfl
```
Mentions: prod
lemma rdist_eq_rdistm Ruzsa distance of random variables equals Ruzsa distance of the kernels line 83 source
Source documentation
Ruzsa distance of random variables equals Ruzsa distance of the kernels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Eq, Real, rdist, ProbabilityTheory.Kernel.rdistm, MeasureTheory.Measure.map
Proof uses: rfl
```
lemma rdist_eq_rdistm : d[X ; μ # Y ; μ'] = Kernel.rdistm (μ.map X) (μ'.map Y) := rfl
```
lemma continuous_rdist_restrict_probabilityMeasure Ruzsa distance depends continuously on the measure line 86 source
Source documentation
Ruzsa distance depends continuously on the measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Finite, TopologicalSpace, DiscreteTopology, BorelSpace, Continuous, Prod, MeasureTheory.ProbabilityMeasure, Real, rdist, id, Prod.fst, Prod.snd
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, MeasureTheory.Measure.prod, HDiv.hDiv, OfNat.ofNat, Nat, Eq, congrArg, funext, MeasureTheory.Measure.map, congrFun', MeasureTheory.Measure, congr, MeasureTheory.Measure.map_id, continuous_of_discreteTopology, MeasureTheory.ProbabilityMeasure.prod, MeasureTheory.ProbabilityMeasure.continuous_prod, MeasureTheory.ProbabilityMeasure.map, MeasureTheory.ProbabilityMeasure.continuous_map and 20 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma continuous_rdist_restrict_probabilityMeasure [Finite G]
    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] :
    Continuous
      (fun (μ : ProbabilityMeasure G × ProbabilityMeasure G) ↦
        d[id ; μ.1.toMeasure # id ; μ.2.toMeasure]) := by
…
```
lemma continuous_rdist_restrict_probabilityMeasure₁ line 109 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Finite, TopologicalSpace, DiscreteTopology, BorelSpace, autoParam, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, Continuous, MeasureTheory.ProbabilityMeasure, Real, rdist, id, MeasureTheory.Measure.map
Proof uses: MeasureTheory.IsProbabilityMeasure.mk, of_eq_true, Eq, ENNReal, Set, Set.univ, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, Set.preimage, MeasureTheory.Measure.map_apply, MeasurableSet.univ, MeasureTheory.IsProbabilityMeasure.measure_univ, eq_self, Prod, Prod.mk, Subtype.mk, Continuous.prodMk_right and 12 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma rdist_eq_rdist_id_map Ruzsa distance between random variables equals Ruzsa distance between their distributions line 122 source
Source documentation
Ruzsa distance between random variables equals Ruzsa distance between their distributions.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Eq, Real, rdist, id, MeasureTheory.Measure.map
Proof uses: of_eq_true, HSub.hSub, ProbabilityTheory.measureEntropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, HDiv.hDiv, OfNat.ofNat, Nat, Eq.trans, True, congrArg, congr, ProbabilityTheory.entropy, MeasureTheory.Measure.map_id, congrFun', eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_eq_rdist_id_map : d[X ; μ # Y ; μ'] = d[id ; μ.map X # id ; μ'.map Y] := by
…
```
lemma continuous_rdist_restrict_probabilityMeasure₁' Ruzsa distance depends continuously on the second measure line 126 source
Source documentation
Ruzsa distance depends continuously on the second measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Finite, TopologicalSpace, DiscreteTopology, BorelSpace, autoParam, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, Continuous, MeasureTheory.ProbabilityMeasure, Real, rdist, id
Proof uses: Eq.mpr, MeasureTheory.Measure.map, Eq, congrArg, funext, Eq.trans, rdist_eq_rdist_id_map, MeasureTheory.Measure.map_id, continuous_rdist_restrict_probabilityMeasure₁
13 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma continuous_rdist_restrict_probabilityMeasure₁' [Finite G]
    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]
    (X : Ω → G) (P : Measure Ω := by volume_tac) [IsProbabilityMeasure P] (X_mble : Measurable X) :
…
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y] line 135 source
Source documentation
If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, ProbabilityTheory.IdentDistrib, Eq, Real, rdist
Proof uses: of_eq_true, HSub.hSub, ProbabilityTheory.entropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, HDiv.hDiv, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, congr, ProbabilityTheory.IdentDistrib.map_eq, ProbabilityTheory.IdentDistrib.entropy_congr, eq_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr {X' : Ω'' → G} {Y' : Ω''' → G}
    (hX : IdentDistrib X X' μ μ'') (hY : IdentDistrib Y Y' μ' μ''') :
    d[X ; μ # Y ; μ'] = d[X' ; μ'' # Y' ; μ'''] := by
…
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr_left If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y] line 141 source
Source documentation
If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, AEMeasurable, ProbabilityTheory.IdentDistrib, Eq, Real, rdist
Proof uses: ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.refl
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr_left {X' : Ω'' → G}
    (hY : AEMeasurable Y μ') (hX : IdentDistrib X X' μ μ'') :
    d[X ; μ # Y ; μ'] = d[X' ; μ'' # Y ; μ'] := hX.rdist_congr <| .refl hY
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr_right If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y] line 146 source
Source documentation
If X', Y' are copies of X, Y respectively then d[X' ; Y'] = d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, AEMeasurable, ProbabilityTheory.IdentDistrib, Eq, Real, rdist
Proof uses: ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.refl
```
lemma ProbabilityTheory.IdentDistrib.rdist_congr_right {Y' : Ω''' → G}
    (hX : AEMeasurable X μ) (hY : IdentDistrib Y Y' μ' μ''') :
    d[X ; μ # Y ; μ'] = d[X ; μ # Y' ; μ'''] := (IdentDistrib.refl hX).rdist_congr hY
```
Mentions: ProbabilityTheory.IdentDistrib.rdist_congr
lemma tendsto_rdist_probabilityMeasure line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Filter, TopologicalSpace, BorelSpace, Finite, DiscreteTopology, Continuous, MeasureTheory.ProbabilityMeasure, Filter.Tendsto, nhds, Real, rdist
Proof uses: Eq, id, MeasureTheory.ProbabilityMeasure.map, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.mk, Continuous.aemeasurable, aemeasurable_id, of_eq_true, MeasureTheory.Measure, MeasureTheory.Measure.map, Eq.trans, True, congrArg, MeasureTheory.Measure.map_id, eq_self, Eq.mpr, congr, congrFun', funext, Prod and 8 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.IndepFun.rdist_eq If X, Y are independent G-random variables then d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2 line 177 source
Source documentation
If X, Y are independent G-random variables then d[X ; Y] = H[X - Y] - H[X]/2 - H[Y]/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IndepFun, Measurable, Eq, Real, rdist, HSub.hSub, ProbabilityTheory.entropy, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, id, congrArg, rdist_def, HSub, Eq.rec, Eq.refl, prod, Eq.symm, Prod.mk, Iff.mp, ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map, Measurable.aemeasurable, ProbabilityTheory.measureEntropy, ProbabilityTheory.entropy_def and 7 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma ProbabilityTheory.IndepFun.rdist_eq [IsFiniteMeasure μ]
    {Y : Ω → G} (h : IndepFun X Y μ) (hX : Measurable X) (hY : Measurable Y) :
    d[X ; μ # Y ; μ] = H[X - Y ; μ] - H[X ; μ]/2 - H[Y ; μ]/2 := by
…
```
lemma rdist_le_avg_ent d[X ; Y] ≤ H[X]/2 + H[Y]/2 line 188 source
Source documentation
d[X ; Y] ≤ H[X]/2 + H[Y]/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, Measurable, autoParam, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, LE.le, Real, rdist, HDiv.hDiv, HAdd.hAdd, ProbabilityTheory.entropy, OfNat.ofNat, Nat
Proof uses: Prod, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_finiteRange, Eq.mpr, id, Eq, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.entropy_congr, HSub.hSub, ProbabilityTheory.IndepFun.rdist_eq, LE.le.trans, Function.comp, Prod.fst, Prod.snd, prod and 81 more
102 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_le_avg_ent {X : Ω → G} {Y : Ω' → G} [FiniteRange X] [FiniteRange Y] (hX : Measurable X)
    (hY : Measurable Y) (μ : Measure Ω := by volume_tac) (μ' : Measure Ω' := by volume_tac)
…
```
Mentions: FiniteRange
lemma rdist_of_inj Applying an injective homomorphism does not affect Ruzsa distance line 202 source
Source documentation
Applying an injective homomorphism does not affect Ruzsa distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, AddMonoidHom, Function.Injective, MeasureTheory.IsProbabilityMeasure, Eq, Real, rdist, Function.comp
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, HDiv.hDiv, OfNat.ofNat, Nat, id, congrArg, rdist_def, HSub, Eq.rec, Eq.refl, Eq.symm, ProbabilityTheory.entropy_comp_of_injective, Measurable.fun_sub and 19 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_of_inj {H : Type*} [hH : MeasurableSpace H] [MeasurableSingletonClass H]
  [AddCommGroup H] [Countable H] (hX : Measurable X) (hY : Measurable Y)
  (φ : G →+ H) (hφ : Injective φ) [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    d[φ ∘ X ; μ # φ ∘ Y ; μ'] = d[X ; μ # Y ; μ'] := by
…
```
lemma rdist_zero_eq_half_ent d[X ; 0] = H[X] / 2 line 226 source
Source documentation
d[X ; 0] = H[X] / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsFiniteMeasure, MeasureTheory.IsProbabilityMeasure, Eq, Real, rdist, OfNat.ofNat, HDiv.hDiv, ProbabilityTheory.entropy, Nat
Proof uses: Prod, HSub.hSub, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, MeasureTheory.Measure.dirac, Eq.mpr, Prod.mk, id, congrArg, MeasureTheory.Measure.prod_dirac, Function.comp, MeasureTheory.Measure.map_map, Measurable.fun_sub, Measurable.fst, measurable_id', Measurable.snd, Measurable.prodMk, measurable_const and 73 more
105 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_zero_eq_half_ent [IsFiniteMeasure μ] [IsProbabilityMeasure μ'] :
    d[X ; μ # fun _ ↦ 0 ; μ'] = H[X ; μ]/2 := by
…
```
lemma rdist_symm d[X ; Y] = d[Y ; X] line 238 source
Source documentation
d[X ; Y] = d[Y ; X]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsFiniteMeasure, Eq, Real, rdist
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, HDiv.hDiv, OfNat.ofNat, Nat, id, congrArg, rdist_def, HAdd.hAdd, sub_sub, add_comm, HSub, Eq.rec, Eq.refl and 21 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_symm [IsFiniteMeasure μ] [IsFiniteMeasure μ'] :
    d[X ; μ # Y ; μ'] = d[Y ; μ' # X ; μ] := by
…
```
lemma continuous_rdist_restrict_probabilityMeasure₁_left Ruzsa distance depends continuously on the first measure line 250 source
Source documentation
Ruzsa distance depends continuously on the first measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, MeasurableSingletonClass, Finite, TopologicalSpace, DiscreteTopology, BorelSpace, autoParam, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, Continuous, MeasureTheory.ProbabilityMeasure, Real, rdist, id
Proof uses: Eq.mpr, eq_of_heq, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, funext, congrArg, rdist_symm, continuous_rdist_restrict_probabilityMeasure₁'
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma continuous_rdist_restrict_probabilityMeasure₁_left [Finite G]
    [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G]
    (X : Ω → G) (P : Measure Ω := by volume_tac) [IsProbabilityMeasure P] (X_mble : Measurable X) :
…
```
lemma diff_ent_le_rdist |H[X] - H[Y]| ≤ 2 d[X ; Y] line 261 source
Source documentation
|H[X] - H[Y]| ≤ 2 d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, Real, abs, HSub.hSub, ProbabilityTheory.entropy, HMul.hMul, OfNat.ofNat, Nat, rdist
Proof uses: Prod, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_finiteRange, Eq.mpr, id, Eq, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, HDiv.hDiv, ProbabilityTheory.IndepFun.rdist_eq, ProbabilityTheory.IdentDistrib.entropy_congr, Neg.neg, propext, abs_le, Max.max, ProbabilityTheory.max_entropy_le_entropy_sub and 82 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma diff_ent_le_rdist [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) :
    |H[X ; μ] - H[Y ; μ']| ≤ 2 * d[X ; μ # Y ; μ'] := by
…
```
lemma diff_ent_le_rdist' H[X - Y] - H[X] ≤ 2d[X ; Y] line 274 source
Source documentation
H[X - Y] - H[X] ≤ 2d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HMul.hMul, OfNat.ofNat, Nat, rdist
Proof uses: Eq.mpr, HDiv.hDiv, id, Eq, congrArg, ProbabilityTheory.IndepFun.rdist_eq, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Max.max, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast and 67 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma diff_ent_le_rdist' [IsProbabilityMeasure μ] {Y : Ω → G}
    (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) [FiniteRange Y] :
    H[X - Y ; μ] - H[X ; μ] ≤ 2 * d[X ; μ # Y ; μ] := by
…
```
Mentions: FiniteRange
lemma diff_ent_le_rdist'' H[X - Y] - H[Y] ≤ 2d[X ; Y] line 281 source
Source documentation
H[X - Y] - H[Y] ≤ 2d[X ; Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HMul.hMul, OfNat.ofNat, Nat, rdist
Proof uses: Eq.mpr, HDiv.hDiv, id, Eq, congrArg, ProbabilityTheory.IndepFun.rdist_eq, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Max.max, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast and 67 more
100 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma diff_ent_le_rdist'' [IsProbabilityMeasure μ] {Y : Ω → G}
    (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) [FiniteRange Y] :
    H[X - Y ; μ] - H[Y ; μ] ≤ 2 * d[X ; μ # Y ; μ] := by
…
```
Mentions: FiniteRange
lemma rdist_nonneg d[X ; Y] ≥ 0 line 288 source
Source documentation
d[X ; Y] ≥ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, LE.le, Real, OfNat.ofNat, rdist
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HMul.hMul, Nat, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 48 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) : 0 ≤ d[X ; μ # Y ; μ'] := by
…
```
lemma ent_of_proj_le Documented declaration: ent_of_proj_le line 295 source
Source documentation
If $G$ is an additive group and $X$ is a $G$-valued random variable and $H\leq G$ is a finite subgroup then, with $\pi:G\to G/H$ the natural homomorphism we have (where $U_H$ is uniform on $H$) $\mathbb{H}(\pi(X))\leq 2d[X;U_H].$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsProbabilityMeasure, Measurable, AddSubgroup, Set.Finite, ProbabilityTheory.IsUniform, LE.le, Real, ProbabilityTheory.entropy, HasQuotient.Quotient, Function.comp, AddMonoidHom, QuotientAddGroup.mk', HMul.hMul, OfNat.ofNat and 2 more
Proof uses: Prod, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_finiteRange, ProbabilityTheory.IsUniform.of_identDistrib, ProbabilityTheory.IdentDistrib.symm, MeasurableSet.of_discrete, Eq.mpr, id, Eq, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.comp, Measurable.of_discrete, ProbabilityTheory.IdentDistrib.rdist_congr, MeasureTheory.Measure.map, QuotientAddGroup.leftRel and 207 more
217 instances, coercions and auxiliary constants left out.

Tactic trace: 61 steps
Open to load the checked before-and-after goal states.
```
lemma ent_of_proj_le {UH : Ω' → G} [FiniteRange UH]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hU : Measurable UH) {H : AddSubgroup G} (hH : Set.Finite (H : Set G))
    -- TODO: infer from [FiniteRange UH]?
    (hunif : IsUniform H UH μ') :
    H[(QuotientAddGroup.mk' H) ∘ X; μ] ≤ 2 * d[X; μ # UH ; μ'] := by
…
```
Mentions: FiniteRange, hU
lemma rdist_add_const Adding a constant to a random variable does not change the Rusza distance line 378 source
Source documentation
Adding a constant to a random variable does not change the Rusza distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Eq, Real, rdist, HAdd.hAdd
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, Neg.neg, HDiv.hDiv, ProbabilityTheory.entropy, Nat, True, congr, congrArg, HSub.hSub, Prod, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, congrFun' and 28 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_add_const [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) {c} :
    d[X ; μ # Y + fun _ ↦ c; μ'] = d[X ; μ # Y ; μ'] := by
…
```
lemma rdist_add_const' A variant of rdist_add_const where one adds constants to both variables line 399 source
Source documentation
A variant of rdist_add_const where one adds constants to both variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, FiniteRange, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Eq, Real, rdist, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, rdist_add_const, Measurable.add, Prod, measurable_const, rdist_symm, Eq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_add_const' [IsZeroOrProbabilityMeasure μ] [IsZeroOrProbabilityMeasure μ']
    (c : G) (c' : G) (hX : Measurable X) (hY : Measurable Y) :
    d[X + fun _ ↦ c; μ # Y + fun _ ↦ c'; μ'] = d[X ; μ # Y ; μ'] := by
…
```
lemma ent_of_diff_le The improved entropic Ruzsa triangle inequality line 406 source
Source documentation
The improved entropic Ruzsa triangle inequality.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, ProbabilityTheory.IndepFun, Prod, prod, MeasureTheory.IsProbabilityMeasure, FiniteRange, LE.le, Real, ProbabilityTheory.entropy, HSub.hSub, HAdd.hAdd
Proof uses: ProbabilityTheory.entropy_triple_add_entropy_le, Measurable.sub, Trans.trans, Eq, Function.comp, Prod.mk, Prod.fst, Prod.snd, funext, of_eq_true, Eq.trans, True, congrArg, sub_sub_sub_cancel_right, eq_self, Eq.mpr, id, ProbabilityTheory.entropy_comp_le, Measurable.prodMk, OfNat.ofNat and 62 more
78 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma ent_of_diff_le (X : Ω → G) (Y : Ω → G) (Z : Ω → G)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (h : IndepFun (⟨X, Y⟩) Z μ)
    [IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[X - Y; μ] ≤ H[X - Z; μ] + H[Z - Y; μ] - H[Z; μ] := by
…
```
Mentions: FiniteRange
lemma rdist_triangle The entropic Ruzsa triangle inequality line 443 source
Source documentation
The entropic Ruzsa triangle inequality

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.IsProbabilityMeasure, FiniteRange, LE.le, Real, rdist, HAdd.hAdd
Proof uses: Exists, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies3_nondep_finiteRange, ProbabilityTheory.IndepFun, Prod, prod, ProbabilityTheory.iIndepFun.indepFun_prodMk, List, List.Mem, Eq, List.finRange, HEq and 94 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma rdist_triangle {X : Ω → G} {Y : Ω' → G} {Z : Ω'' → G}
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [hμ : IsProbabilityMeasure μ] [hμ' : IsProbabilityMeasure μ']
    [hμ'' : IsProbabilityMeasure μ''] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    d[X ; μ # Z ; μ''] ≤ d[X ; μ # Y ; μ'] + d[Y ; μ' # Z ; μ''] := by
…
```
Mentions: FiniteRange
def condRuzsaDist line 473 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, autoParam, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Real
Proof uses: ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map
4 instances, coercions and auxiliary constants left out.
lemma condRuzsaDist_def line 484 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Eq, Real, condRuzsaDist, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma condRuszaDist_zero_right line 489 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Eq, Real, condRuzsaDist, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, MeasureTheory.Measure.map_zero, ProbabilityTheory.Kernel.rdist_zero_right, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRuszaDist_zero_left line 494 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Eq, Real, condRuzsaDist, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, MeasureTheory.Measure.map_zero, ProbabilityTheory.Kernel.rdist_zero_left, eq_self
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_eq_sum' Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype line 502 source
Source documentation
Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ in a fintype.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Fintype, Eq, Real, condRuzsaDist, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rdist, ProbabilityTheory.cond
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id, congrArg, condRuzsaDist_def, MeasureTheory.integral, Prod, MeasureTheory.Measure.prod, ProbabilityTheory.Kernel.rdistm, ProbabilityTheory.Kernel, Prod.fst, Prod.snd, ProbabilityTheory.Kernel.rdist.eq_1, HSMul.hSMul, MeasureTheory.integral_fintype, MeasureTheory.Integrable.of_finite, congrFun', Finset.sum_congr and 32 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_eq_sum' {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) [IsFiniteMeasure μ] (μ' : Measure Ω') [IsFiniteMeasure μ']
    [Fintype S] [Fintype T] :
    d[X | Z ; μ # Y | W ; μ']
      = ∑ z, ∑ w, μ.real (Z ⁻¹' {z}) * μ'.real (W ⁻¹' {w})
          * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by
…
```
lemma condRuzsaDist_eq_sum Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$ line 529 source
Source documentation
Explicit formula for conditional Ruzsa distance $d[X|Z; Y|W]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Eq, Real, condRuzsaDist, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rdist, ProbabilityTheory.cond
Proof uses: Filter.Eventually, Prod, Membership.mem, Finset, SProd.sprod, MeasureTheory.ae, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, MeasureTheory.Measure.prod_of_full_measure_finset, Eq.mpr, ENNReal, Compl.compl, OfNat.ofNat, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet, Finset.measurableSet, EmptyCollection.emptyCollection, eq_of_heq and 55 more
75 instances, coercions and auxiliary constants left out.

Tactic trace: 24 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_eq_sum {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) [IsFiniteMeasure μ] (μ' : Measure Ω') [IsFiniteMeasure μ']
    [FiniteRange Z] [FiniteRange W] :
    d[X | Z ; μ # Y | W ; μ']
      = ∑ z ∈ FiniteRange.toFinset Z, ∑ w ∈ FiniteRange.toFinset W,
        μ.real (Z ⁻¹' {z}) * μ'.real (W ⁻¹' {w})
          * d[X ; (μ[|Z ← z]) # Y ; (μ'[|W ← w])] := by
…
```
Mentions: FiniteRange, FiniteRange.toFinset
lemma condRuzsaDist_symm $$ d[X|Z; Y|W] = d[Y|W; X|Z]$$ line 567 source
Source documentation
$$ d[X|Z; Y|W] = d[Y|W; X|Z]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, FiniteRange, Eq, Real, condRuzsaDist
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id, congrArg, condRuzsaDist_def, ProbabilityTheory.Kernel.rdist_symm, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_symm [Countable T]
    {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T} [IsProbabilityMeasure μ]
    [IsProbabilityMeasure μ'] [FiniteRange Z] [FiniteRange W] :
    d[X | Z ; μ # Y | W ; μ'] = d[Y | W ; μ' # X | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist_nonneg line 573 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, FiniteRange, MeasureTheory.IsProbabilityMeasure, LE.le, Real, OfNat.ofNat, condRuzsaDist
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id, Eq, congrArg, condRuzsaDist_def, ProbabilityTheory.Kernel.rdist_nonneg, ProbabilityTheory.Kernel.aefiniteKernelSupport_condDistrib
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
def condRuzsaDist' line 586 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, autoParam, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Real
Proof uses: ProbabilityTheory.Kernel.rdist, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map, ProbabilityTheory.condDistrib, MeasureTheory.Measure.dirac, Unit.unit
5 instances, coercions and auxiliary constants left out.
lemma condRuzsaDist'_def Conditional Ruzsa distance equals Ruzsa distance of associated kernels line 596 source
Source documentation
Conditional Ruzsa distance equals Ruzsa distance of associated kernels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Eq, Real, condRuzsaDist', ProbabilityTheory.Kernel.rdist, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map, ProbabilityTheory.condDistrib, MeasureTheory.Measure.dirac, Unit.unit
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
```
lemma condRuzsaDist'_def {T : Type*} [MeasurableSpace T]
    (X : Ω → G) (Y : Ω' → G) (W : Ω' → T) (μ : Measure Ω) (μ' : Measure Ω')
    [IsFiniteMeasure μ'] :
    d[X ; μ # Y | W ; μ'] =
      dk[Kernel.const Unit (μ.map X) ; Measure.dirac () # condDistrib Y W μ' ; μ'.map W] :=
…
```
lemma condRuzsaDist'_zero_right line 603 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Eq, Real, condRuzsaDist', OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.Kernel.rdist, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map, ProbabilityTheory.condDistrib, MeasureTheory.Measure.dirac, Unit.unit, MeasureTheory.Measure.map_zero, ProbabilityTheory.Kernel.rdist_zero_right, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist'_eq_sum Explicit formula for conditional Ruzsa distance d[X ; Y | W] line 609 source
Source documentation
Explicit formula for conditional Ruzsa distance d[X ; Y | W].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Eq, Real, condRuzsaDist', Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rdist, ProbabilityTheory.cond
Proof uses: Filter.Eventually, Prod, Unit, Membership.mem, Finset, SProd.sprod, Finset.univ, MeasureTheory.ae, MeasureTheory.Measure.prod, MeasureTheory.Measure.dirac, Unit.unit, MeasureTheory.Measure.map, MeasureTheory.Measure.prod_of_full_measure_finset, of_eq_true, ENNReal, Compl.compl, OfNat.ofNat, Eq.trans, True, congrFun' and 66 more
88 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist'_eq_sum {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y)
    (hW : Measurable W) (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [FiniteRange W] :
    d[X ; μ # Y | W ; μ']
      = ∑ w ∈ FiniteRange.toFinset W, μ'.real (W ⁻¹' {w}) * d[X ; μ # Y ; (μ'[|W ← w])] := by
…
```
Mentions: FiniteRange, FiniteRange.toFinset
lemma condRuzsaDist'_eq_sum' Alternate formula for conditional Ruzsa distance d[X ; Y | W] when T is a Fintype line 634 source
Source documentation
Alternate formula for conditional Ruzsa distance d[X ; Y | W] when T is a Fintype.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Fintype, Eq, Real, condRuzsaDist', Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rdist, ProbabilityTheory.cond
Proof uses: Eq.mpr, FiniteRange.toFinset, id, congrArg, condRuzsaDist'_eq_sum, Finset.sum_subset, of_eq_true, LE.le, Finset, Membership.mem, Not, EmptyCollection.emptyCollection, Set.ext, Iff, Eq.trans, False, True, congr, eq_false, Eq.mp and 8 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist'_eq_sum' {X : Ω → G} {Y : Ω' → G} {W : Ω' → T} (hY : Measurable Y)
    (hW : Measurable W) (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [Fintype T] :
    d[X ; μ # Y | W ; μ']
      = ∑ w, μ'.real (W ⁻¹' {w}) * d[X ; μ # Y ; (μ'[|W ← w])] := by
…
```
lemma condRuzsaDist'_prod_eq_sum line 649 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, MeasureTheory.IsFiniteMeasure, FiniteRange, Eq, Real, condRuzsaDist', Prod, prod, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set and 1 more
Proof uses: SProd.sprod, Finset, Prod.mk, rdist, Eq.mpr, id, congrArg, condRuzsaDist'_eq_sum, Measurable.prodMk, Finset.sum_subset, Membership.mem, And, Exists, Eq.trans, implies_congr, funext, Prod.mk.injEq, Prod.fst, Prod.snd, congr and 42 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 34 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist'_prod_eq_sum' Version of condRuzsaDist'_prod_eq_sum when W has finite codomain line 686 source
Source documentation
Version of condRuzsaDist'_prod_eq_sum when W has finite codomain.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, MeasureTheory.IsFiniteMeasure, Fintype, Eq, Real, condRuzsaDist', Prod, prod, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set and 1 more
Proof uses: Eq.mpr, FiniteRange.toFinset, id, congrArg, condRuzsaDist'_prod_eq_sum, Finset.sum_subset, of_eq_true, LE.le, Finset, Membership.mem, Not, EmptyCollection.emptyCollection, Set.ext, Iff, Eq.trans, False, True, congr, eq_false, Eq.mp and 11 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist'_prod_eq_sum' {X : Ω → G} {Y : Ω' → G} {W W' : Ω' → T}
    (μ : Measure Ω) (μ' : Measure Ω') (hY : Measurable Y) (hW' : Measurable W') (hW : Measurable W)
    [IsFiniteMeasure μ'] [Fintype T] :
    d[X ; μ # Y | ⟨W', W⟩; μ']
      = ∑ w, μ'.real (W ⁻¹' {w}) * d[X ; μ # Y | W' ; (μ'[|W ← w])] := by
…
```
lemma condRuzsaDist'_eq_integral Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form line 701 source
Source documentation
Explicit formula for conditional Ruzsa distance d[X ; Y | W], in integral form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Eq, Real, condRuzsaDist', MeasureTheory.integral, MeasureTheory.Measure.map, rdist, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
Proof uses: Eq.mpr, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, id, congrArg, condRuzsaDist'_eq_sum, HSMul.hSMul, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, Filter.Eventually, MeasureTheory.ae, propext, MeasureTheory.ae_map_iff, of_eq_true, AEMeasurable and 15 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist'_eq_integral (X : Ω → G) {Y : Ω' → G} {W : Ω' → T}
    (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) (μ' : Measure Ω') [IsFiniteMeasure μ'] [FiniteRange W] :
    d[X ; μ # Y | W ; μ']
      = (μ'.map W)[fun w ↦ d[X ; μ # Y ; (μ'[|W ← w])]] := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist_of_const Conditioning by a constant does not affect Ruzsa distance line 715 source
Source documentation
Conditioning by a constant does not affect Ruzsa distance.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.IsProbabilityMeasure, FiniteRange, Eq, Real, condRuzsaDist, condRuzsaDist'
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id, congrArg, condRuzsaDist_def, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Unit.unit, condRuzsaDist'_def, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_const, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul and 37 more
69 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_of_const {X : Ω → G} (hX : Measurable X)
    (Y : Ω' → G) (W : Ω' → T) (c : S)
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] [FiniteRange W] :
    d[X|(fun _ ↦ c) ; μ # Y | W ; μ'] = d[X ; μ # Y | W ; μ'] := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist_of_indep If $(X,Z)$ and $(Y,W)$ are independent, then d[X | Z ; Y | W] = H[X'- Y' | Z', W'] - H[X'|Z']/2 - H[Y'|W']/2 line 728 source
Source documentation
If $(X,Z)$ and $(Y,W)$ are independent, then d[X | Z ; Y | W] = H[X'- Y' | Z', W'] - H[X'|Z']/2 - H[Y'|W']/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Prod, prod, FiniteRange, Eq, Real, condRuzsaDist, HSub.hSub, ProbabilityTheory.condEntropy, HDiv.hDiv, OfNat.ofNat, Nat
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id, congrArg, condRuzsaDist_def, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, ProbabilityTheory.Kernel.prod, ProbabilityTheory.Kernel.prodMkRight, ProbabilityTheory.Kernel.prodMkLeft, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.Kernel.rdist_eq', Prod.mk, ProbabilityTheory.condEntropy_eq_kernel_entropy, Measurable.sub, Measurable.prodMk and 29 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_of_indep
    {X : Ω → G} {Z : Ω → S} {Y : Ω → G} {W : Ω → T}
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (h : IndepFun (⟨X, Z⟩) (⟨Y, W⟩) μ) [FiniteRange Z] [FiniteRange W] :
    d[X | Z ; μ # Y | W ; μ] = H[X - Y | ⟨Z, W⟩ ; μ] - H[X | Z ; μ]/2 - H[Y | W ; μ]/2 := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist'_of_indep Formula for conditional Ruzsa distance for independent sets of variables line 756 source
Source documentation
Formula for conditional Ruzsa distance for independent sets of variables.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Prod, prod, FiniteRange, Eq, Real, condRuzsaDist', HSub.hSub, ProbabilityTheory.condEntropy, HDiv.hDiv, ProbabilityTheory.entropy, OfNat.ofNat, Nat
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.rdist, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map, ProbabilityTheory.condDistrib, MeasureTheory.Measure.dirac, Unit.unit, id, congrArg, condRuzsaDist'_def, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, ProbabilityTheory.Kernel.prod, ProbabilityTheory.Kernel.prodMkRight, ProbabilityTheory.Kernel.prodMkLeft, Prod.fst, Prod.snd, MeasureTheory.Measure.prod, ProbabilityTheory.Kernel.rdist_eq' and 87 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 58 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist'_of_indep {X : Ω → G} {Y : Ω → G} {W : Ω → T}
    (hX : Measurable X) (hY : Measurable Y) (hW : Measurable W)
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (h : IndepFun X (⟨Y, W⟩) μ) [FiniteRange W] :
    d[X ; μ # Y | W ; μ] = H[X - Y | W ; μ] - H[X ; μ]/2 - H[Y | W ; μ]/2 := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist_of_copy The conditional Ruzsa distance is unchanged if the sets of random variables are replaced with copies line 821 source
Source documentation
The conditional Ruzsa distance is unchanged if the sets of random variables are replaced with copies.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IdentDistrib, Prod, prod, FiniteRange, Eq, Real, condRuzsaDist
Proof uses: Finset, Union.union, Classical.propDecidable, FiniteRange.toFinset, Filter.Eventually, Membership.mem, Set, SProd.sprod, MeasureTheory.ae, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, id, MeasureTheory.Measure.prod_of_full_measure_finset, Eq.mpr, ENNReal, Compl.compl, OfNat.ofNat, Set.preimage, congrArg, MeasureTheory.Measure.map_apply and 75 more
80 instances, coercions and auxiliary constants left out.

Tactic trace: 63 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_of_copy {X : Ω → G} (hX : Measurable X) {Z : Ω → S} (hZ : Measurable Z)
    {Y : Ω' → G} (hY : Measurable Y) {W : Ω' → T} (hW : Measurable W)
    {X' : Ω'' → G} (hX' : Measurable X') {Z' : Ω'' → S} (hZ' : Measurable Z')
    {Y' : Ω''' → G} (hY' : Measurable Y') {W' : Ω''' → T} (hW' : Measurable W')
    [IsFiniteMeasure μ] [IsFiniteMeasure μ'] [IsFiniteMeasure μ''] [IsFiniteMeasure μ''']
    (h1 : IdentDistrib (⟨X, Z⟩) (⟨X', Z'⟩) μ μ'') (h2 : IdentDistrib (⟨Y, W⟩) (⟨Y', W'⟩) μ' μ''')
    [FiniteRange Z] [FiniteRange W] [FiniteRange Z'] [FiniteRange W'] :
    d[X | Z ; μ # Y | W ; μ'] = d[X' | Z' ; μ'' # Y' | W' ; μ'''] := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist'_of_copy line 896 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.IdentDistrib, Prod, prod, FiniteRange, Eq, Real, condRuzsaDist'
Proof uses: Finset, Union.union, Classical.propDecidable, FiniteRange.toFinset, Filter.Eventually, Unit, Membership.mem, Set, SProd.sprod, Finset.univ, MeasureTheory.ae, MeasureTheory.Measure.prod, MeasureTheory.Measure.dirac, Unit.unit, MeasureTheory.Measure.map, MeasureTheory.Measure.prod_of_full_measure_finset, of_eq_true, ENNReal, Compl.compl, OfNat.ofNat and 88 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma condRuszaDist_prod_eq_of_indepFun line 947 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, ProbabilityTheory.IndepFun, Prod, prod, MeasureTheory.IsProbabilityMeasure, Finite, Eq, Real, condRuzsaDist'
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond, id, congrArg, condRuzsaDist'_prod_eq_sum', Eq.symm, Finset.sum_mul, Finset, MeasureTheory.sum_measureReal_preimage_singleton and 36 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_comp_right line 968 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Finite, MeasureTheory.IsFiniteMeasure, Measurable, Function.Injective, Eq, Real, condRuzsaDist', Function.comp
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, rdist, ProbabilityTheory.cond, id, congrArg, condRuzsaDist'_eq_sum', Measurable.comp, Set.ext, of_eq_true and 24 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_of_inj_map line 983 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Fin, OfNat.ofNat, Nat, ProbabilityTheory.IndepFun, Prod, prod, Measurable, AddMonoidHom, Function.Injective, Prod.mk, FiniteRange, Eq, Real, condRuzsaDist and 1 more
Proof uses: HSub.hSub, Prod.fst, Prod.snd, Measurable.of_discrete, Measurable.sub, Measurable.prodMk, Eq.mpr, ProbabilityTheory.condEntropy, HDiv.hDiv, id, congrArg, condRuzsaDist_of_indep, Measurable.fun_comp, ProbabilityTheory.IndepFun.comp, Eq.symm, ProbabilityTheory.condEntropy_of_injective, map_comp_sub, Eq.refl
49 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist'_of_inj_map line 1006 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Module, ZMod, OfNat.ofNat, Nat, Measurable, ProbabilityTheory.IndepFun, Prod, prod, FiniteRange, Eq, Real, condRuzsaDist', HAdd.hAdd
Proof uses: AddMonoidHom, AddMonoidHom.mk, ZeroHom.mk, HSub.hSub, Prod.snd, Prod.fst, of_eq_true, Eq.trans, True, congrFun', congrArg, sub_self, eq_self, Eq.mpr, id, congr, ZModModule.sub_eq_add, Fin, Matrix.vecCons, Neg.neg and 49 more
68 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist'_of_inj_map' line 1044 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, Eq, Real, condRuzsaDist', HAdd.hAdd
Proof uses: Prod, Function.comp, Prod.fst, rfl, Measurable.comp, measurable_fst, Prod.snd, measurable_snd, MeasureTheory.Measure.prod, inferInstance, condRuzsaDist'_of_copy, Measurable.add, ProbabilityTheory.IdentDistrib.mk, Measurable.aemeasurable, Eq.mpr, MeasureTheory.Measure.map, id, congrArg, Eq.symm, MeasureTheory.Measure.map_map and 25 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 86 steps
Open to load the checked before-and-after goal states.
lemma kaimanovich_vershik The Kaimanovich-Vershik inequality line 1105 source
Source documentation
The Kaimanovich-Vershik inequality. H[X + Y + Z] - H[X + Y] ≤ H[Y + Z] - H[Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, FiniteRange, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HAdd.hAdd
Proof uses: MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.iIndepFun.isProbabilityMeasure, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, eq_of_heq, List.Mem.tail, False.elim and 83 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
```
lemma kaimanovich_vershik {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    H[X + Y + Z ; μ] - H[X + Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by
…
```
Mentions: FiniteRange
lemma kaimanovich_vershik' A version of the Kaimanovich-Vershik inequality with some variables negated line 1137 source
Source documentation
A version of the Kaimanovich-Vershik inequality with some variables negated.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, Measurable, FiniteRange, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, HAdd.hAdd
Proof uses: Eq.mpr, Neg.neg, id, Eq, congrArg, Eq.symm, ProbabilityTheory.entropy_neg, Measurable.add, Prod, congr, Eq.trans, congrFun', autoParam, sub_eq_add_neg, neg_add, kaimanovich_vershik, Function.update, eq_of_heq, HEq, Eq.refl and 35 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma kaimanovich_vershik' {X Y Z : Ω → G} (h : iIndepFun ![X, Y, Z] μ)
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    H[X - (Y + Z) ; μ] - H[X - Y ; μ] ≤ H[Y + Z ; μ] - H[Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ent_bsg The entropic Balog-Szemerédi-Gowers inequality line 1157 source
Source documentation
The entropic Balog-Szemerédi-Gowers inequality. Let A, B be G-valued random variables on Ω, and set Z := A+B. Then ∑ z, P[Z=z] d[(A | Z = z) ; (B | Z = z)] ≤ 3 I[A :B] + 2 H[Z] - H[A] - H[B]. TODO: remove the hypothesis of Fintype G from here and from condIndep_copies'

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, Finite, LE.le, Real, MeasureTheory.integral, MeasureTheory.Measure.map, HAdd.hAdd, rdist, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, HSub.hSub, HMul.hMul and 4 more
Proof uses: Measurable.add, Prod, Exists, And, ProbabilityTheory.CondIndepFun, ProbabilityTheory.IdentDistrib, prod, Eq, ProbabilityTheory.condIndep_copies', Measurable.prodMk, Measurable.of_discrete, Function.uncurry, Filter.Eventually.of_forall, MeasureTheory.ae, rfl, Prod.fst, Prod.snd, funext, Measurable.fst, Measurable.snd and 134 more
159 instances, coercions and auxiliary constants left out.

Tactic trace: 77 steps
Open to load the checked before-and-after goal states.
```
lemma ent_bsg [IsProbabilityMeasure μ] {A B : Ω → G} (hA : Measurable A) (hB : Measurable B)
    [Finite G] :
    (μ.map (A + B))[fun z ↦ d[A ; μ[|(A + B) ⁻¹' {z}] # B ; μ[|(A + B) ⁻¹' {z}]]]
      ≤ 3 * I[A : B; μ] + 2 * H[A + B ; μ] - H[A ; μ] - H[B ; μ] := by
…
```
lemma condRuzsaDist_le Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group line 1282 source
Source documentation
Suppose that $(X, Z)$ and $(Y, W)$ are random variables, where $X, Y$ take values in an abelian group. Then $$d[X | Z ; Y | W] \leq d[X ; Y] + \tfrac{1}{2} I[X : Z] + \tfrac{1}{2} I[Y : W]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, condRuzsaDist, HAdd.hAdd, rdist, HDiv.hDiv, ProbabilityTheory.mutualInfo, OfNat.ofNat, Nat
Proof uses: Prod, prod, Measurable.prodMk, Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_finiteRange, Function.comp, Prod.fst, Prod.snd, Measurable.fst, Measurable.snd, ProbabilityTheory.IndepFun.comp, measurable_fst, Eq.mpr, id, Eq, congrArg, Eq.symm and 89 more
106 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma condRuzsaDist_le [Countable T] {X : Ω → G} {Z : Ω → S} {Y : Ω' → G} {W : Ω' → T}
    [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hZ : Measurable Z) (hY : Measurable Y) (hW : Measurable W)
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] [FiniteRange W] :
      d[X | Z ; μ # Y|W ; μ'] ≤ d[X ; μ # Y ; μ'] + I[X : Z ; μ]/2 + I[Y : W ; μ']/2 := by
…
```
Mentions: FiniteRange
lemma condRuzsaDist_le' line 1317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, condRuzsaDist', HAdd.hAdd, rdist, HDiv.hDiv, ProbabilityTheory.mutualInfo, OfNat.ofNat, Nat
Proof uses: Eq.mpr, condRuzsaDist, Fin, id, Eq, congrArg, Eq.symm, condRuzsaDist_of_const, LE.le.trans, condRuzsaDist_le, measurable_const, of_eq_true, Eq.trans, True, congrFun', MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.mutualInfo_const, zero_div, add_zero
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_le'_prod line 1327 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, condRuzsaDist', Prod, prod, HAdd.hAdd, HDiv.hDiv, ProbabilityTheory.condMutualInfo, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond, id, Eq, congrArg, condRuzsaDist'_prod_eq_sum, rdist, condRuzsaDist'_eq_sum, ProbabilityTheory.mutualInfo, ProbabilityTheory.condMutualInfo_eq_sum, Finset.sum_div, Eq.symm, Finset.sum_add_distrib and 20 more
70 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma comparison_of_ruzsa_distances line 1343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, And, LE.le, Real, HSub.hSub, rdist, HAdd.hAdd, HDiv.hDiv, ProbabilityTheory.entropy, OfNat.ofNat, Nat, Module and 2 more
Proof uses: Exists, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies3_nondep_finiteRange, ProbabilityTheory.iIndepFun.indepFun, Ne, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, ProbabilityTheory.IdentDistrib.add, Prod, List, List.Mem and 121 more
130 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_diff_le Let X, Y, Z be random variables taking values in some abelian group, and with Y, Z independent line 1379 source
Source documentation
Let X, Y, Z be random variables taking values in some abelian group, and with Y, Z independent. Then we have d[X ; Y + Z] - d[X ; Y] ≤ 1/2 (H[Y+ Z] - H[Y]) $$= \tfrac{1}{2} d[Y ; Z] + \tfrac{1}{4} H[Z] - \tfrac{1}{4} H[Y]$$ and $$d[X ; Y|Y+ Z] - d[X ; Y] \leq \tfrac{1}{2} \bigl(H[Y+ Z] - H[Z]\bigr)$$ $$= \tfrac{1}{2} d[Y ; Z] + \tfrac{1}{4} H[Y] - \tfrac{1}{4} H[Z]$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, LE.le, Real, HSub.hSub, rdist, HAdd.hAdd, HDiv.hDiv, ProbabilityTheory.entropy, OfNat.ofNat, Nat
Proof uses: And.left, Module, ZMod, Eq, comparison_of_ruzsa_distances
38 instances, coercions and auxiliary constants left out.
```
lemma condRuzsaDist_diff_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    {X : Ω → G} {Y : Ω' → G} {Z : Ω' → G}
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (h : IndepFun Y Z μ')
    [FiniteRange X] [FiniteRange Z] [FiniteRange Y] :
    d[X ; μ # Y+ Z ; μ'] - d[X ; μ # Y ; μ'] ≤ (H[Y + Z; μ'] - H[Y; μ']) / 2 :=
…
```
Mentions: FiniteRange
lemma entropy_sub_entropy_eq_condRuzsaDist_add line 1387 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, Eq, Real, HSub.hSub, ProbabilityTheory.entropy, HAdd.hAdd, rdist, HDiv.hDiv
Proof uses: And.right, LE.le, comparison_of_ruzsa_distances
41 instances, coercions and auxiliary constants left out.
lemma condRuzsaDist_diff_le' line 1395 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, LE.le, Real, HSub.hSub, rdist, HAdd.hAdd, HDiv.hDiv, ProbabilityTheory.entropy
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 67 more
108 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_diff_le'' line 1405 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, LE.le, Real, HSub.hSub, condRuzsaDist', HAdd.hAdd, rdist, HDiv.hDiv, ProbabilityTheory.entropy, OfNat.ofNat, Nat
Proof uses: Eq.mpr, ProbabilityTheory.mutualInfo, id, Eq, congrArg, Eq.symm, ProbabilityTheory.mutualInfo_add_right, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast and 64 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_diff_le''' line 1414 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IndepFun, FiniteRange, LE.le, Real, HSub.hSub, condRuzsaDist', HAdd.hAdd, rdist, HDiv.hDiv and 1 more
Proof uses: le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HMul.hMul, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Ring, Int.rawCast, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos and 67 more
112 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma condRuzsaDist_diff_ofsum_le line 1424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, AddCommGroup, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, FiniteRange, LE.le, Real, HSub.hSub, condRuzsaDist', HAdd.hAdd and 3 more
Proof uses: ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun_add_left, Prod, Fin.cases, Fin.succ, Fin.rec0, Ne, of_decide_eq_true, Eq, id, Bool, Decidable.decide, Bool.true, Eq.refl, condRuzsaDist_diff_le'', Measurable.add, condRuzsaDist_diff_le, ProbabilityTheory.iIndepFun.indepFun, le_of_not_gt, LT.lt and 74 more
115 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.