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

29 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

Imported by 2 files

lemma ProbabilityTheory.entropy_mul_const line 22 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, Measurable, Eq, Real, ProbabilityTheory.entropy, HMul.hMul
Proof uses: ProbabilityTheory.entropy_comp_of_injective, mul_left_injective
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.entropy_mul_right H[X, X + Y] = H[X, Y] line 28 source
Source documentation
H[X, X + Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HMul.hMul
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodShear, Equiv.refl, Equiv.mulLeft, Equiv.injective
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_mul_right (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, X * Y⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_mul_right' H[X, Y + X] = H[X, Y] line 35 source
Source documentation
H[X, Y + X] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HMul.hMul
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodShear, Equiv.refl, Equiv.mulRight, Equiv.injective
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_mul_right' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, Y * X⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_mul_left H[Y + X, Y] = H[X, Y] line 42 source
Source documentation
H[Y + X, Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HMul.hMul
Proof uses: Eq.trans, ProbabilityTheory.entropy_comm, Measurable.mul, ProbabilityTheory.entropy_mul_right
20 instances, coercions and auxiliary constants left out.
```
lemma entropy_mul_left (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨Y * X, Y⟩; μ] = H[⟨X, Y⟩ ; μ] :=
…
```
lemma ProbabilityTheory.entropy_mul_left' H[X + Y, Y] = H[X, Y] line 48 source
Source documentation
H[X + Y, Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HMul.hMul
Proof uses: Eq.trans, ProbabilityTheory.entropy_comm, Measurable.mul, ProbabilityTheory.entropy_mul_right'
20 instances, coercions and auxiliary constants left out.
```
lemma entropy_mul_left' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X * Y, Y⟩; μ] = H[⟨X, Y⟩ ; μ] :=
…
```
lemma ProbabilityTheory.entropy_inv_right H[X, -Y] = H[X, Y] line 55 source
Source documentation
H[X, -Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, Inv.inv
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodCongr, Equiv.refl, Equiv.inv, Equiv.injective
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_inv_right (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, Y⁻¹⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_inv_left H[-X, Y] = H[X, Y] line 62 source
Source documentation
H[-X, Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, Inv.inv
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodCongr, Equiv.inv, Equiv.refl, Equiv.injective
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_inv_left (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X⁻¹, Y⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_div_right H[X, X - Y] = H[X, Y] line 69 source
Source documentation
H[X, X - Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HDiv.hDiv
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodShear, Equiv.refl, Equiv.divLeft, Equiv.injective
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_div_right (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, X / Y⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_div_right' H[X, Y - X] = H[X, Y] line 76 source
Source documentation
H[X, Y - X] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HDiv.hDiv
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Equiv, Equiv.prodShear, Equiv.refl, Equiv.divRight, Equiv.injective
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_div_right' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, Y / X⟩; μ] = H[⟨X, Y⟩ ; μ] := by
…
```
lemma ProbabilityTheory.entropy_div_left H[Y - X, Y] = H[X, Y] line 83 source
Source documentation
H[Y - X, Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HDiv.hDiv
Proof uses: Eq.trans, ProbabilityTheory.entropy_comm, Measurable.div, ProbabilityTheory.entropy_div_right
14 instances, coercions and auxiliary constants left out.
```
lemma entropy_div_left (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨Y / X, Y⟩; μ] = H[⟨X, Y⟩ ; μ] :=
…
```
lemma ProbabilityTheory.entropy_div_left' H[X - Y, Y] = H[X, Y] line 89 source
Source documentation
H[X - Y, Y] = H[X, Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HDiv.hDiv
Proof uses: Eq.trans, ProbabilityTheory.entropy_comm, Measurable.div, ProbabilityTheory.entropy_div_right'
14 instances, coercions and auxiliary constants left out.
```
lemma entropy_div_left' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X / Y, Y⟩; μ] = H[⟨X, Y⟩ ; μ] :=
…
```
lemma ProbabilityTheory.entropy_inv If X is G-valued, then H[-X]=H[X] line 96 source
Source documentation
If X is G-valued, then H[-X]=H[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, Measurable, Eq, Real, ProbabilityTheory.entropy, Inv.inv
Proof uses: ProbabilityTheory.entropy_comp_of_injective, inv_injective
10 instances, coercions and auxiliary constants left out.
```
lemma entropy_inv (hX : Measurable X) : H[X⁻¹ ; μ] = H[X ; μ] :=
…
```
lemma ProbabilityTheory.entropy_div_comm H[X - Y] = H[Y - X] line 101 source
Source documentation
H[X - Y] = H[Y - X]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, Measurable, Eq, Real, ProbabilityTheory.entropy, HDiv.hDiv
Proof uses: Eq.mpr, Inv.inv, id, congrArg, Eq.symm, inv_div, ProbabilityTheory.entropy_inv, Measurable.div, Prod
17 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_div_comm {Y : Ω → G} (hX : Measurable X) (hY : Measurable Y) :
    H[X / Y ; μ] = H[Y / X ; μ] := by rw [← inv_div]; exact entropy_inv (hY.div hX)
…
```
Mentions: ProbabilityTheory.entropy_inv
lemma ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_div max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X - Y | Z] line 107 source
Source documentation
max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X - Y | Z]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, FiniteRange, Measurable, MeasureTheory.IsProbabilityMeasure, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.condEntropy, ProbabilityTheory.condMutualInfo, HDiv.hDiv
Proof uses: Eq.mpr, id, Eq, congrArg, ProbabilityTheory.condMutualInfo_comm, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, ProbabilityTheory.condEntropy_eq_kernel_entropy, ProbabilityTheory.Kernel.mutualInfo, Prod, prod, ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo, Measurable.div, ProbabilityTheory.Kernel.snd, Prod.mk, ProbabilityTheory.Kernel.entropy_congr, Filter.EventuallyEq.symm, ProbabilityTheory.Kernel, MeasureTheory.ae and 22 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma max_condEntropy_sub_condMutualInfo_le_condEntropy_div [FiniteRange X] [FiniteRange Y]
    {Z : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [IsProbabilityMeasure μ] [FiniteRange Z] :
    (max H[X | Z ; μ] H[Y | Z ; μ]) - I[X : Y | Z ; μ] ≤ H[X / Y | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_mul_left H[Y + X | Y] = H[X | Y] line 132 source
Source documentation
H[Y + X | Y] = H[X | Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Measurable, Eq, Real, ProbabilityTheory.condEntropy, HMul.hMul
Proof uses: ProbabilityTheory.condEntropy_of_injective, mul_right_injective
17 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_mul_left (hX : Measurable X) (hY : Measurable Y) :
     H[Y * X | Y ; μ] = H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.condEntropy_mul_right H[X + Y | Y] = H[X | Y] line 138 source
Source documentation
H[X + Y | Y] = H[X | Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Measurable, Eq, Real, ProbabilityTheory.condEntropy, HMul.hMul
Proof uses: ProbabilityTheory.condEntropy_of_injective, mul_left_injective
17 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_mul_right (hX : Measurable X) (hY : Measurable Y) :
    H[X * Y | Y ; μ] = H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.condEntropy_div_left H[Y - X | Y] = H[X | Y] line 144 source
Source documentation
H[Y - X | Y] = H[X | Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Measurable, Eq, Real, ProbabilityTheory.condEntropy, HDiv.hDiv
Proof uses: ProbabilityTheory.condEntropy_of_injective, div_right_injective
7 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_div_left (hX : Measurable X) (hY : Measurable Y) :
    H[Y / X | Y ; μ] = H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.condEntropy_div_right H[X - Y | Y] = H[X | Y] line 150 source
Source documentation
H[X - Y | Y] = H[X | Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Measurable, Eq, Real, ProbabilityTheory.condEntropy, HDiv.hDiv
Proof uses: ProbabilityTheory.condEntropy_of_injective, div_left_injective
7 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_div_right (hX : Measurable X) (hY : Measurable Y) :
    H[X / Y | Y ; μ] = H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.mutualInfo_mul_right I[X : X + Y] = H[X + Y] - H[Y] iff X, Y are independent line 162 source
Source documentation
I[X : X + Y] = H[X + Y] - H[Y] iff X, Y are independent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, FiniteRange, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Eq, Real, ProbabilityTheory.mutualInfo, HMul.hMul, HSub.hSub, ProbabilityTheory.entropy
Proof uses: Eq.mpr, HAdd.hAdd, Prod, prod, id, congrArg, ProbabilityTheory.mutualInfo_def, ProbabilityTheory.entropy_mul_right, ProbabilityTheory.IndepFun.entropy_pair_eq_add
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_mul_right (hX : Measurable X) (hY : Measurable Y) {μ : Measure Ω}
    [IsProbabilityMeasure μ] (h : IndepFun X Y μ) :
    I[X : X * Y ; μ] = H[X * Y ; μ] - H[Y ; μ] := by
…
```
lemma ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul H[X] - I[X : Y] ≤ H[X + Y] line 175 source
Source documentation
H[X] - I[X : Y] ≤ H[X + Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HMul.hMul
Proof uses: Eq.mpr, ProbabilityTheory.condEntropy, id, Eq, congrArg, ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy, Eq.symm, ProbabilityTheory.condEntropy_mul_right, ProbabilityTheory.condEntropy_le_entropy, Measurable.mul, Prod
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_le_entropy_mul (hX : Measurable X) (hY : Measurable Y) :
    H[X ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ] := by
…
```
lemma ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul' H[Y] - I[X : Y] ≤ H[X + Y] line 182 source
Source documentation
H[Y] - I[X : Y] ≤ H[X + Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HMul.hMul
Proof uses: Eq.mpr, ProbabilityTheory.condEntropy, id, Eq, congrArg, ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy', Eq.symm, ProbabilityTheory.condEntropy_mul_left, ProbabilityTheory.condEntropy_le_entropy, Measurable.mul, Prod
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_le_entropy_mul' (hX : Measurable X) (hY : Measurable Y) :
    H[Y ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ] := by
…
```
lemma ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div H[X] - I[X : Y] ≤ H[X - Y] line 189 source
Source documentation
H[X] - I[X : Y] ≤ H[X - Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HDiv.hDiv
Proof uses: Eq.mpr, ProbabilityTheory.condEntropy, id, Eq, congrArg, ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy, Eq.symm, ProbabilityTheory.condEntropy_div_right, ProbabilityTheory.condEntropy_le_entropy, Measurable.div, Prod
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_le_entropy_div (hX : Measurable X) (hY : Measurable Y) :
    H[X ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ] := by
…
```
lemma ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div' H[Y] - I[X : Y] ≤ H[X - Y] line 196 source
Source documentation
H[Y] - I[X : Y] ≤ H[X - Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HDiv.hDiv
Proof uses: Eq.mpr, id, Eq, congrArg, ProbabilityTheory.mutualInfo_comm, ProbabilityTheory.condEntropy, ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy, Eq.symm, ProbabilityTheory.condEntropy_div_left, ProbabilityTheory.condEntropy_le_entropy, Measurable.div, Prod
22 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_le_entropy_div' (hX : Measurable X) (hY : Measurable Y) :
    H[Y ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ] := by
…
```
lemma ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_mul max(H[X], H[Y]) - I[X : Y] ≤ H[X + Y] line 204 source
Source documentation
max(H[X], H[Y]) - I[X : Y] ≤ H[X + Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, max_sub_sub_right, And, propext, max_le_iff, And.intro, ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul, ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_mul'
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma max_entropy_sub_mutualInfo_le_entropy_mul (hX : Measurable X) (hY : Measurable Y) :
    max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X * Y ; μ] := by
…
```
lemma ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_div max(H[X], H[Y]) - I[X : Y] ≤ H[X - Y] line 211 source
Source documentation
max(H[X], H[Y]) - I[X : Y] ≤ H[X - Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, HDiv.hDiv
Proof uses: Eq.mpr, id, Eq, congrArg, Eq.symm, max_sub_sub_right, And, propext, max_le_iff, And.intro, ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div, ProbabilityTheory.entropy_sub_mutualInfo_le_entropy_div'
30 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma max_entropy_sub_mutualInfo_le_entropy_div (hX : Measurable X) (hY : Measurable Y) :
    max H[X ; μ] H[Y ; μ] - I[X : Y ; μ] ≤ H[X / Y ; μ] := by
…
```
lemma ProbabilityTheory.max_condEntropy_sub_condMutualInfo_le_condEntropy_mul max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X + Y | Z] line 218 source
Source documentation
max(H[X | Z], H[Y | Z]) - I[X : Y | Z] ≤ H[X + Y | Z]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, LE.le, Real, HSub.hSub, Max.max, ProbabilityTheory.condEntropy, ProbabilityTheory.condMutualInfo, HMul.hMul
Proof uses: Eq.mpr, id, Eq, congrArg, ProbabilityTheory.condMutualInfo_comm, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, ProbabilityTheory.condEntropy_eq_kernel_entropy, ProbabilityTheory.Kernel.mutualInfo, Prod, prod, ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo, Measurable.mul, ProbabilityTheory.Kernel.snd, Prod.mk, ProbabilityTheory.Kernel.entropy_congr, Filter.EventuallyEq.symm, ProbabilityTheory.Kernel, MeasureTheory.ae and 21 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma max_condEntropy_sub_condMutualInfo_le_condEntropy_mul {Z : Ω → T} [FiniteRange Z]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) :
    max H[X | Z ; μ] H[Y | Z ; μ] - I[X : Y | Z ; μ] ≤ H[X * Y | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.max_entropy_le_entropy_mul If X, Y are independent, then max(H[X], H[Y]) ≤ H[X + Y] line 236 source
Source documentation
If X, Y are independent, then max(H[X], H[Y]) ≤ H[X + Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, ProbabilityTheory.IndepFun, LE.le, Real, Max.max, ProbabilityTheory.entropy, HMul.hMul
Proof uses: Eq.mpr, And, id, Eq, Eq.mp, HSub.hSub, ProbabilityTheory.mutualInfo, Eq.trans, congrFun', congrArg, OfNat.ofNat, ProbabilityTheory.IndepFun.mutualInfo_eq_zero, sub_zero, ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_mul
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma max_entropy_le_entropy_mul (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) :
    max H[X ; μ] H[Y ; μ] ≤ H[X * Y ; μ] := by
…
```
lemma ProbabilityTheory.max_entropy_le_entropy_div If X, Y are independent, then max(H[X], H[Y]) ≤ H[X - Y] line 242 source
Source documentation
If X, Y are independent, then max(H[X], H[Y]) ≤ H[X - Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Group, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Measurable, ProbabilityTheory.IndepFun, LE.le, Real, Max.max, ProbabilityTheory.entropy, HDiv.hDiv
Proof uses: Eq.mpr, And, id, Eq, Eq.mp, HSub.hSub, ProbabilityTheory.mutualInfo, Eq.trans, congrFun', congrArg, OfNat.ofNat, ProbabilityTheory.IndepFun.mutualInfo_eq_zero, sub_zero, ProbabilityTheory.max_entropy_sub_mutualInfo_le_entropy_div
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma max_entropy_le_entropy_div (hX : Measurable X) (hY : Measurable Y) (h : IndepFun X Y μ) :
    max H[X ; μ] H[Y ; μ] ≤ H[X / Y ; μ] := by
…
```
lemma ProbabilityTheory.max_entropy_le_entropy_prod line 250 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Countable, MeasurableSingletonClass, CommGroup, MeasurableMul₂, Finset, Membership.mem, FiniteRange, Measurable, ProbabilityTheory.iIndepFun, LE.le, Real, ProbabilityTheory.entropy, Finset.prod
Proof uses: Finset.Nonempty, Exists.intro, Finset.Nonempty.cons_induction, Singleton.singleton, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', autoParam, id, Eq, Eq.mp, Finset.prod_singleton, Not, Finset.cons, Eq.mpr, HMul.hMul, Finset.prod_cons and 16 more
39 instances, coercions and auxiliary constants left out.

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