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

98 declarations, 0 contain sorry, 0 declared as axioms

Entropy and conditional entropy

Main definitions

entropy: entropy of a random variable, defined as measureEntropy (volume.map X)
condEntropy: conditional entropy of a random variable X w.r.t. another one Y
mutualInfo: mutual information of two random variables

Main statements

chain_rule: $H[⟨X, Y⟩] = H[Y] + H[X | Y]$
entropy_cond_le_entropy: $H[X | Y] ≤ H[X]$. (Chain rule another way.)
entropy_triple_add_entropy_le (Submodularity of entropy.) : $H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z]$.

Notations

H[X] = entropy X
H[X | Y ← y] = Hm[(ℙ[|Y ← y]).map X]
H[X | Y] = condEntropy X Y, such that H[X | Y] = (volume.map Y)[fun y ↦ H[X | Y ← y]]
I[X : Y] = mutualInfo X Y

All notations have variants where we can specify the measure (which is otherwise supposed to be volume). For example H[X ; μ] and I[X : Y ; μ] instead of H[X] and I[X : Y] respectively.

Imports (4)

Imported by 3 files

def ProbabilityTheory.entropy line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map
1 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.entropy_def Entropy of a random variable agrees with entropy of its distribution line 58 source
Source documentation
Entropy of a random variable agrees with entropy of its distribution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map
Proof uses: rfl
```
lemma entropy_def (X : Ω → S) (μ : Measure Ω) : entropy X μ = Hm[μ.map X] := rfl
```
Mentions: ProbabilityTheory.entropy
lemma ProbabilityTheory.entropy_eq_kernel_entropy Entropy of a random variable is also the kernel entropy of the distribution over a Dirac mass line 62 source
Source documentation
Entropy of a random variable is also the kernel entropy of the distribution over a Dirac mass.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, ProbabilityTheory.Kernel.entropy, Unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map, MeasureTheory.Measure.dirac, Unit.unit
Proof uses: of_eq_true, ProbabilityTheory.measureEntropy, Eq.trans, True, congrArg, HMul.hMul, ENNReal.toReal, Set, ENNReal, Set.univ, ProbabilityTheory.Kernel.entropy_const, OfNat.ofNat, congrFun', MeasureTheory.IsProbabilityMeasure.measure_univ, one_mul, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_eq_kernel_entropy (X : Ω → S) (μ : Measure Ω) :
    H[X ; μ] = Hk[Kernel.const Unit (μ.map X), Measure.dirac ()] := by simp [entropy]
…
```
Mentions: ProbabilityTheory.entropy
lemma ProbabilityTheory.entropy_zero_measure Any variable on a zero measure space has zero entropy line 67 source
Source documentation
Any variable on a zero measure space has zero entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Eq, Real, ProbabilityTheory.entropy, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, MeasureTheory.Measure.map_zero, ProbabilityTheory.measureEntropy_zero, eq_self
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_zero_measure (X : Ω → S) : H[X ; (0 : Measure Ω)] = 0 := by simp [entropy]
```
Mentions: ProbabilityTheory.entropy
lemma ProbabilityTheory.entropy_congr Two variables that agree almost everywhere, have the same entropy line 70 source
Source documentation
Two variables that agree almost everywhere, have the same entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Filter.EventuallyEq, MeasureTheory.ae, Eq, Real, ProbabilityTheory.entropy
Proof uses: Eq.mpr, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, id, congrArg, ProbabilityTheory.entropy_def, MeasureTheory.Measure.map_congr, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_congr {X X' : Ω → S} (h : X =ᵐ[μ] X') : H[X ; μ] = H[X' ; μ] := by
…
```
lemma ProbabilityTheory.entropy_nonneg Entropy is always non-negative line 74 source
Source documentation
Entropy is always non-negative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, LE.le, Real, OfNat.ofNat, ProbabilityTheory.entropy
Proof uses: ProbabilityTheory.measureEntropy_nonneg, MeasureTheory.Measure.map
3 instances, coercions and auxiliary constants left out.
```
lemma entropy_nonneg (X : Ω → S) (μ : Measure Ω) : 0 ≤ entropy X μ := measureEntropy_nonneg _
```
Mentions: ProbabilityTheory.entropy, ProbabilityTheory.measureEntropy_nonneg
lemma ProbabilityTheory.IdentDistrib.entropy_congr Two variables that have the same distribution, have the same entropy line 77 source
Source documentation
Two variables that have the same distribution, have the same entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IdentDistrib, Eq, Real, ProbabilityTheory.entropy
Proof uses: of_eq_true, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.IdentDistrib.map_eq, eq_self

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma IdentDistrib.entropy_congr {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'} {X' : Ω' → S}
    (h : IdentDistrib X X' μ μ') : H[X ; μ] = H[X' ; μ'] := by
…
```
lemma ProbabilityTheory.entropy_le_log_card Entropy is at most the logarithm of the cardinality of the range line 82 source
Source documentation
Entropy is at most the logarithm of the cardinality of the range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Fintype, MeasurableSingletonClass, MeasureTheory.Measure, LE.le, Real, ProbabilityTheory.entropy, Real.log, Fintype.card
Proof uses: ProbabilityTheory.measureEntropy_le_log_card, MeasureTheory.Measure.map
3 instances, coercions and auxiliary constants left out.
```
lemma entropy_le_log_card [Fintype S] [MeasurableSingletonClass S]
    (X : Ω → S) (μ : Measure Ω) : H[X ; μ] ≤ log (Fintype.card S) :=
…
```
lemma ProbabilityTheory.entropy_le_log_card_of_mem Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in line 88 source
Source documentation
Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, DiscreteMeasurableSpace, Finset, MeasureTheory.Measure, Measurable, Filter.Eventually, Membership.mem, MeasureTheory.ae, LE.le, Real, ProbabilityTheory.entropy, Real.log, Finset.card
Proof uses: ProbabilityTheory.measureEntropy_le_log_card_of_mem, MeasureTheory.Measure.map, Eq.mpr, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.of_discrete
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_le_log_card_of_mem [DiscreteMeasurableSpace S]
    {A : Finset S} {μ : Measure Ω} {X : Ω → S}
    (hX : Measurable X) (h : ∀ᵐ ω ∂μ, X ω ∈ A) :
    H[X ; μ] ≤ log A.card :=
…
```
lemma ProbabilityTheory.entropy_le_log_card_of_mem_finite Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in line 96 source
Source documentation
Entropy is at most the logarithm of the cardinality of a set in which X almost surely takes values in.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, DiscreteMeasurableSpace, Set, MeasureTheory.Measure, Set.Finite, Measurable, Filter.Eventually, Membership.mem, MeasureTheory.ae, LE.le, Real, ProbabilityTheory.entropy, Real.log, Nat.card
Proof uses: Finset, Eq, Exists, CanLift.prf, Eq.mpr, Finset.card, id, congrArg, Nat, Eq.trans, Subtype, Fintype.card, Nat.card_eq_fintype_card, Fintype.card_coe, ProbabilityTheory.entropy_le_log_card_of_mem
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_le_log_card_of_mem_finite [DiscreteMeasurableSpace S]
    {A : Set S} {μ : Measure Ω} {X : Ω → S}
    (hA : A.Finite) (hX : Measurable X) (h : ∀ᵐ ω ∂μ, X ω ∈ A) :
    H[X ; μ] ≤ log (Nat.card A) := by
…
```
lemma ProbabilityTheory.entropy_eq_sum H[X] = ∑ₛ P[X=s] log 1 / P[X=s] line 104 source
Source documentation
H[X] = ∑ₛ P[X=s] log 1 / P[X=s].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, Real, ProbabilityTheory.entropy, tsum, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, SummationFilter.unconditional
Proof uses: Eq.mpr, ProbabilityTheory.measureEntropy, id, congrArg, ProbabilityTheory.entropy_def, ProbabilityTheory.measureEntropy_of_isProbabilityMeasure, Eq.refl
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_eq_sum (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] :
    entropy X μ = ∑' x, negMulLog ((μ.map X).real {x}) := by
…
```
Mentions: ProbabilityTheory.entropy
lemma ProbabilityTheory.entropy_eq_sum' line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, Real, ProbabilityTheory.entropy, tsum, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, SummationFilter.unconditional
Proof uses: of_eq_true, ENNReal.toReal, ENNReal, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.measureEntropy_of_isProbabilityMeasure, eq_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.entropy_eq_sum_finset line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Finset, Eq, ENNReal, Set, MeasureTheory.Measure.map, Compl.compl, OfNat.ofNat, Real, ProbabilityTheory.entropy, Finset.sum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton
Proof uses: Eq.mpr, tsum, SummationFilter.unconditional, id, congrArg, ProbabilityTheory.entropy_eq_sum, Eq.refl, tsum_eq_sum, Not, Membership.mem, eq_of_heq, HEq, HEq.refl, Eq.symm, ENNReal.toReal, MeasureTheory.Measure.real.eq_1, MeasureTheory.measure_mono_null, of_eq_true, LE.le, Eq.trans and 6 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.entropy_eq_sum_finset' line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Finset, Eq, ENNReal, Set, MeasureTheory.Measure.map, Compl.compl, OfNat.ofNat, Real, ProbabilityTheory.entropy, Finset.sum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton
Proof uses: ProbabilityTheory.entropy_eq_sum_finset
16 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.entropy_eq_sum_finiteRange line 130 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.entropy, Finset.sum, FiniteRange.toFinset, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set
Proof uses: ProbabilityTheory.entropy_eq_sum_finset, ProbabilityTheory.full_measure_of_finiteRange
2 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.entropy_eq_sum_finiteRange' line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.entropy, Finset.sum, FiniteRange.toFinset, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set
Proof uses: ProbabilityTheory.entropy_eq_sum_finiteRange
2 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.entropy_cond_eq_sum H[X | Y=y] = ∑_s P[X=s | Y=y] log 1/(P[X=s | Y=y]) line 141 source
Source documentation
H[X | Y=y] = ∑_s P[X=s | Y=y] log 1/(P[X=s | Y=y]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, tsum, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, SummationFilter.unconditional
Proof uses: dite, ENNReal, OfNat.ofNat, Eq.mpr, ProbabilityTheory.measureEntropy, id, congrArg, ProbabilityTheory.entropy_def, ProbabilityTheory.cond_eq_zero_of_meas_eq_zero, of_eq_true, Eq.trans, True, congr, MeasureTheory.Measure.map_zero, ProbabilityTheory.measureEntropy_zero, congrFun', SummationFilter, optParam, funext, Real.negMulLog_zero and 5 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_cond_eq_sum (μ : Measure Ω) (y : T) :
    H[X | Y ← y ; μ] = ∑' x, negMulLog (((μ[|Y ← y]).map X).real {x}) := by
…
```
lemma ProbabilityTheory.entropy_cond_eq_sum_finiteRange line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, FiniteRange, Eq, Real, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Finset.sum, FiniteRange.toFinset, Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map
Proof uses: dite, ENNReal, OfNat.ofNat, Eq.mpr, ProbabilityTheory.measureEntropy, id, congrArg, ProbabilityTheory.entropy_def, ProbabilityTheory.cond_eq_zero_of_meas_eq_zero, of_eq_true, Eq.trans, True, congr, MeasureTheory.Measure.map_zero, ProbabilityTheory.measureEntropy_zero, Finset.sum_congr, Eq.refl, Finset, Membership.mem, congrFun' and 5 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.entropy_comp_of_injective If X, Y are S-valued and T-valued random variables, and Y = f(X) for some injection f : S \to T, then H[Y] = H[X] line 160 source
Source documentation
If X, Y are S-valued and T-valued random variables, and Y = f(X) for some injection f : S \to T, then H[Y] = H[X]. One can also use entropy_of_comp_eq_of_comp as an alternative if verifying injectivity is fiddly. For the upper bound only, see entropy_comp_le.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, Function.Injective, Eq, Real, ProbabilityTheory.entropy, Function.comp
Proof uses: Measurable.of_discrete, Eq.mpr, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, id, congrArg, ProbabilityTheory.entropy_def, Eq.symm, MeasureTheory.Measure.map_map, ProbabilityTheory.measureEntropy_map_of_injective, Eq.refl
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_comp_of_injective [MeasurableSpace T] [Countable S] [MeasurableSingletonClass S]
    [MeasurableSingletonClass T]
    (μ : Measure Ω) (hX : Measurable X) (f : S → T) (hf : Function.Injective f) :
    H[f ∘ X ; μ] = H[X ; μ] := by
…
```
lemma ProbabilityTheory.entropy_const The entropy of any constant is zero line 169 source
Source documentation
The entropy of any constant is zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, Real, ProbabilityTheory.entropy, OfNat.ofNat
Proof uses: MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, MeasureTheory.Measure.map_zero, ProbabilityTheory.measureEntropy_zero, eq_self, Eq.symm, MeasureTheory.Measure.dirac, HSMul.hSMul, ENNReal, Set, Set.univ, MeasureTheory.Measure.map_const and 3 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
@[simp] lemma entropy_const [MeasurableSingletonClass S] [IsZeroOrProbabilityMeasure μ] (c : S) :
    H[fun _ ↦ c ; μ] = 0 := by
…
```
lemma ProbabilityTheory.IsUniform.entropy_eq If X is uniformly distributed on H, then H[X] = log |H| line 179 source
Source documentation
If X is uniformly distributed on H, then H[X] = log |H|.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, DiscreteMeasurableSpace, Finset, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, Eq, Real, ProbabilityTheory.entropy, Real.log, Nat.card, Subtype, Membership.mem
Proof uses: Real.negMulLog, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, HMul.hMul, dite, Classical.propDecidable, of_eq_true, Eq.trans, Inv.inv, Finset.card, True, congr, congrArg, Neg.neg, HDiv.hDiv, OfNat.ofNat, ProbabilityTheory.IsUniform.measureReal_preimage_of_mem', one_div and 38 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.entropy_eq [DiscreteMeasurableSpace S] {H : Finset S} {X : Ω → S} {μ : Measure Ω}
    [IsProbabilityMeasure μ] (hX : IsUniform H X μ) (hX' : Measurable X) :
    H[X ; μ] = log (Nat.card H) := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.IsUniform.entropy_eq' Variant of IsUniform.entropy_congr where H is a finite Set rather than Finset line 193 source
Source documentation
Variant of IsUniform.entropy_congr where H is a finite Set rather than Finset.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, DiscreteMeasurableSpace, Set, Set.Finite, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IsUniform, Measurable, Eq, Real, ProbabilityTheory.entropy, Real.log, Set.ncard
Proof uses: Finset, Set.Finite.toFinset, Eq.mpr, id, congrFun', autoParam, congrArg, Set.Finite.coe_toFinset, Eq.mp, Nat.card, Subtype, Membership.mem, Nat, funext, ProbabilityTheory.IsUniform.entropy_eq
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma IsUniform.entropy_eq' [DiscreteMeasurableSpace S]
    {A : Set S} (hA : A.Finite) {X : Ω → S} {μ : Measure Ω} [IsProbabilityMeasure μ]
    (hX : IsUniform A X μ) (hX' : Measurable X) : H[X ; μ] = log A.ncard := by
…
```
Mentions: ProbabilityTheory.IsUniform
lemma ProbabilityTheory.entropy_eq_log_card If X is S-valued random variable, then H[X] = log |S| if and only if X is uniformly distributed line 201 source
Source documentation
If X is S-valued random variable, then H[X] = log |S| if and only if X is uniformly distributed.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Fintype, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, NeZero, MeasureTheory.IsFiniteMeasure, Iff, Eq, Real, ProbabilityTheory.entropy, Real.log, Fintype.card, ENNReal, Set, MeasureTheory.Measure.map, Singleton.singleton, HDiv.hDiv, Set.univ
Proof uses: OfNat.ofNat, Or, eq_zero_or_neZero, LE.le, Set.preimage, MeasureTheory.Measure.le_map_apply, Measurable.aemeasurable, False.elim, Eq.mp, False, Eq.trans, congrArg, congrFun', Eq.mpr, ProbabilityTheory.measureEntropy, id, ProbabilityTheory.entropy_def, propext, ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq, MeasureTheory.Measure.map_apply and 3 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_eq_log_card {X : Ω → S} [Fintype S] [MeasurableSingletonClass S]
    (hX : Measurable X) (μ : Measure Ω) [hμ : NeZero μ]
    [IsFiniteMeasure μ] :
    entropy X μ = log (Fintype.card S) ↔ ∀ s, μ.map X {s} = μ Set.univ / Fintype.card S := by
…
```
Mentions: ProbabilityTheory.entropy
lemma ProbabilityTheory.prob_ge_exp_neg_entropy If X is an S-valued random variable, then there exists s ∈ S such that P[X = s] ≥ \exp(- H[X]) line 215 source
Source documentation
If X is an S-valued random variable, then there exists s ∈ S such that P[X = s] ≥ \exp(- H[X]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Nonempty, MeasureTheory.Measure, Measurable, FiniteRange, Exists, LE.le, ENNReal, HMul.hMul, Set, Set.univ, Real.toNNReal, Real.exp, Neg.neg, Real, ProbabilityTheory.entropy, MeasureTheory.Measure.map, Singleton.singleton
Proof uses: ProbabilityTheory.FiniteSupport, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, Finset.filter, Ne, OfNat.ofNat, Eq, rfl, HAdd.hAdd, Compl.compl, MeasureTheory.measure_add_measure_compl, Finset.measurableSet, id, of_eq_true, Eq.trans, True, congrFun' and 94 more
131 instances, coercions and auxiliary constants left out.

Tactic trace: 84 steps
Open to load the checked before-and-after goal states.
```
lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] [Nonempty S]
    (X : Ω → S) (μ : Measure Ω)
    (hX : Measurable X) [hX' : FiniteRange X] :
    ∃ s : S, μ Set.univ * (rexp (- H[X ; μ])).toNNReal ≤ μ.map X {s} := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.prob_ge_exp_neg_entropy' If X is an S-valued random variable, then there exists s ∈ S such that P[X=s] ≥ \exp(-H[X]) line 302 source
Source documentation
If X is an S-valued random variable, then there exists s ∈ S such that P[X=s] ≥ \exp(-H[X]).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, Exists, LE.le, Real, Real.exp, Neg.neg, ProbabilityTheory.entropy, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set
Proof uses: Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, ENNReal, HMul.hMul, Set.univ, Real.toNNReal, MeasureTheory.Measure.map, ProbabilityTheory.prob_ge_exp_neg_entropy, Exists.intro, Eq.mp, congrArg, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton, ENNReal.toReal, Eq.symm, MeasureTheory.Measure.real.eq_1, ENNReal.ofReal, propext, ENNReal.ofReal_le_iff_le_toReal and 6 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma prob_ge_exp_neg_entropy' [MeasurableSingletonClass S]
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] (X : Ω → S) (hX : Measurable X) [FiniteRange X] :
    ∃ s : S, rexp (- H[X ; μ]) ≤ μ.real (X ⁻¹' {s}) := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.const_of_nonpos_entropy If X is an S-valued random variable of non-positive entropy, then X is almost surely constant line 316 source
Source documentation
If X is an S-valued random variable of non-positive entropy, then X is almost surely constant.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.entropy, OfNat.ofNat, Exists, Eq, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set
Proof uses: Real.exp, Neg.neg, ProbabilityTheory.prob_ge_exp_neg_entropy', Exists.intro, LE.le.antisymm, Eq.mpr, Set.univ, id, congrArg, Eq.symm, MeasureTheory.probReal_univ, MeasureTheory.measureReal_mono, Set.subset_univ, MeasureTheory.measure_ne_top, le_trans, of_eq_true, Eq.trans, True, eq_true
31 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma const_of_nonpos_entropy [MeasurableSingletonClass S]
    {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}
    [IsProbabilityMeasure μ] {X : Ω → S} (hX : Measurable X) [FiniteRange X] (hent : H[X; μ] ≤ 0) :
    ∃ s : S, μ.real (X ⁻¹' {s}) = 1 := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_prod_comp H[X, f(X)] = H[X] line 333 source
Source documentation
H[X, f(X)] = H[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod, Function.comp
Proof uses: ProbabilityTheory.entropy_comp_of_injective, Prod.mk, And.left, Prod.fst, Prod.snd, Iff.mp, And, Prod.ext_iff
3 instances, coercions and auxiliary constants left out.
```
@[simp] lemma entropy_prod_comp (hX : Measurable X) (μ : Measure Ω) (f : S → T) :
    H[⟨X, f ∘ X⟩; μ] = H[X ; μ] :=
…
```
lemma ProbabilityTheory.entropy_comm H[X, Y] = H[Y, X] line 340 source
Source documentation
H[X, Y] = H[Y, X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.entropy, Prod, prod
Proof uses: id, ProbabilityTheory.entropy_comp_of_injective, Prod.mk, Measurable.prodMk, Prod.swap, Prod.swap_injective
4 instances, coercions and auxiliary constants left out.

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

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

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_assoc (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) (μ : Measure Ω) :
    H[⟨X, ⟨Y, Z⟩⟩ ; μ] = H[⟨⟨X, Y⟩, Z⟩ ; μ] := by
…
```
def ProbabilityTheory.condEntropy line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
7 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.condEntropy_def line 366 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.condEntropy, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.condEntropy_eq_zero line 376 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Eq, Real, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, OfNat.ofNat, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage
Proof uses: Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, autoParam, ProbabilityTheory.cond_eq_zero_of_meas_eq_zero, ENNReal, id, congrArg, propext, MeasureTheory.measureReal_eq_zero_iff, MeasureTheory.measure_ne_top, Eq.mp, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton, ProbabilityTheory.entropy_zero_measure
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condEntropy_eq_kernel_entropy Conditional entropy of a random variable is equal to the entropy of its conditional kernel line 385 source
Source documentation
Conditional entropy of a random variable is equal to the entropy of its conditional kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Nonempty, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map
Proof uses: Eq.mpr, MeasureTheory.integral, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, id, congrArg, ProbabilityTheory.condEntropy_def, ProbabilityTheory.measureEntropy, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.entropy.eq_1, ProbabilityTheory.integral_congr_finiteSupport, Ne, ENNReal, OfNat.ofNat, Eq.rec, Eq.refl, MeasureTheory.Measure.ext and 9 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_kernel_entropy [Nonempty S] [Countable S] [MeasurableSingletonClass S]
    (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) [IsFiniteMeasure μ] [FiniteRange Y] :
    H[X | Y ; μ] = Hk[condDistrib X Y μ, μ.map Y] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_two_eq_kernel_entropy line 401 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Prod, prod, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.condDistrib, Prod.mk, ProbabilityTheory.Kernel.snd, MeasureTheory.Measure.compProd, MeasureTheory.Measure.map and 1 more
Proof uses: Eq.mpr, id, congrArg, MeasureTheory.Measure.compProd_congr, ProbabilityTheory.condDistrib_fst_ae_eq, ProbabilityTheory.map_compProd_condDistrib, ProbabilityTheory.Kernel.entropy_congr, ProbabilityTheory.condKernel_condDistrib_ae_eq, ProbabilityTheory.Kernel.comap, Prod.swap, measurable_swap, Eq.symm, ProbabilityTheory.swap_condDistrib_ae_eq, MeasureTheory.Measure.comap, MeasureTheory.Measure.map_prod_comap_swap, Eq.refl, ProbabilityTheory.condEntropy_eq_kernel_entropy, Measurable.prodMk, ProbabilityTheory.Kernel.entropy_comap_swap
37 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condEntropy_zero_measure Any random variable on a zero measure space has zero conditional entropy line 418 source
Source documentation
Any random variable on a zero measure space has zero conditional entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Eq, Real, ProbabilityTheory.condEntropy, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.Measure.map_zero, MeasureTheory.integral_zero_measure, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_zero_measure (X : Ω → S) (Y : Ω → T) : H[X | Y ; (0 : Measure Ω)] = 0 :=
…
```
lemma ProbabilityTheory.condEntropy_nonneg Conditional entropy is non-negative line 422 source
Source documentation
Conditional entropy is non-negative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, LE.le, Real, OfNat.ofNat, ProbabilityTheory.condEntropy
Proof uses: MeasureTheory.integral_nonneg, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.measureEntropy_nonneg
32 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_nonneg (X : Ω → S) (Y : Ω → T) (μ : Measure Ω) : 0 ≤ H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.condEntropy_le_log_card Conditional entropy is at most the logarithm of the cardinality of the range line 426 source
Source documentation
Conditional entropy is at most the logarithm of the cardinality of the range.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Fintype, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, LE.le, Real, ProbabilityTheory.condEntropy, Real.log, Fintype.card
Proof uses: LE.le.trans, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.integral_mono_of_nonneg, MeasureTheory.ae_of_all, OfNat.ofNat, ProbabilityTheory.entropy_nonneg, MeasureTheory.integrable_const, ProbabilityTheory.entropy_le_log_card, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul and 5 more
66 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S]
    (X : Ω → S) (Y : Ω → T) (μ : Measure Ω) [IsProbabilityMeasure μ] :
    H[X | Y ; μ] ≤ log (Fintype.card S) := by
…
```
lemma ProbabilityTheory.condEntropy_eq_sum H[X|Y] = ∑_y P[Y=y] H[X|Y=y] line 435 source
Source documentation
H[X|Y] = ∑_y P[Y=y] H[X|Y=y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage
Proof uses: Eq.mpr, MeasureTheory.integral, id, congrArg, ProbabilityTheory.condEntropy_def, MeasureTheory.Measure.restrict, Finset, MeasureTheory.integral_eq_setIntegral, ProbabilityTheory.ae_mem_of_finiteRange, HSMul.hSMul, MeasureTheory.setIntegral_finset, MeasureTheory.IntegrableOn.finset, of_eq_true, Eq.trans, True, congrFun', Finset.sum_congr, Eq.refl, Membership.mem, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_sum [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
    [IsFiniteMeasure μ] (hY : Measurable Y) [FiniteRange Y] :
    H[X | Y ; μ] = ∑ y ∈ FiniteRange.toFinset Y, ((μ.map Y).real {y}) * H[X | Y ← y ; μ] := by
…
```
Mentions: FiniteRange, FiniteRange.toFinset
lemma ProbabilityTheory.condEntropy_eq_sum_fintype H[X|Y] = ∑_y P[Y=y] H[X|Y=y] line 443 source
Source documentation
H[X|Y] = ∑_y P[Y=y] H[X|Y=y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Measurable, Fintype, Eq, Real, ProbabilityTheory.condEntropy, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.entropy, ProbabilityTheory.cond
Proof uses: Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.map, id, congrArg, ProbabilityTheory.condEntropy_def, HSMul.hSMul, MeasureTheory.integral_fintype, MeasureTheory.Integrable.of_finite, congrFun', Finset.sum_congr, Eq.refl, Finset, Membership.mem, of_eq_true, Eq.trans, True, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton, eq_self
35 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_sum_fintype
    [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
    [IsFiniteMeasure μ] (hY : Measurable Y) [Fintype T] :
    H[X | Y ; μ] = ∑ y, μ.real (Y ⁻¹' {y}) * H[X | Y ← y ; μ] := by
…
```
lemma ProbabilityTheory.condEntropy_prod_eq_sum line 452 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, MeasureTheory.IsFiniteMeasure, Finite, Fintype, Eq, Real, ProbabilityTheory.condEntropy, Prod, prod, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.cond
Proof uses: Nonempty, nonempty_fintype, Nonempty.intro, Eq.mpr, Prod.mk, ProbabilityTheory.entropy, id, congrFun', congrArg, ProbabilityTheory.condEntropy_eq_sum_fintype, Measurable.prodMk, Finset.sum_congr, Eq.refl, Finset, Membership.mem, Fintype.sum_prod_type_right, Finset.mul_sum, AddCommMonoid, Eq.rec, funext and 26 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condEntropy_eq_sum_sum H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$ line 476 source
Source documentation
H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.negMulLog, ProbabilityTheory.cond, Set.preimage
Proof uses: Eq.mpr, ProbabilityTheory.entropy, id, congrArg, ProbabilityTheory.condEntropy_eq_sum, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, ProbabilityTheory.entropy_cond_eq_sum_finiteRange, Finset.mul_sum
18 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_sum_sum (hX : Measurable X) {Y : Ω → T} (hY : Measurable Y)
    (μ : Measure Ω) [IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    H[X | Y ; μ]
      = ∑ y ∈ FiniteRange.toFinset Y, ∑ x ∈ FiniteRange.toFinset X,
        ((μ.map Y).real {y}) * negMulLog (((μ[|Y ← y]).map X).real {x}) := by
…
```
Mentions: FiniteRange, FiniteRange.toFinset
lemma ProbabilityTheory.condEntropy_eq_sum_sum_fintype H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$ line 487 source
Source documentation
H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Fintype, Eq, Real, ProbabilityTheory.condEntropy, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Real.negMulLog, ProbabilityTheory.cond, Set.preimage
Proof uses: Eq.mpr, ProbabilityTheory.entropy, id, congrArg, ProbabilityTheory.condEntropy_eq_sum_fintype, AddCommMonoid, Finset, Eq.rec, Eq.refl, funext, tsum, SummationFilter.unconditional, ProbabilityTheory.entropy_cond_eq_sum, tsum_fintype, Finset.mul_sum, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton
22 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_sum_sum_fintype {Y : Ω → T} (hY : Measurable Y)
    (μ : Measure Ω) [IsProbabilityMeasure μ] [Fintype S] [Fintype T] :
    H[X | Y ; μ] = ∑ y, ∑ x, (μ.map Y).real {y} * negMulLog (((μ[|Y ← y]).map X).real {x}) := by
…
```
lemma ProbabilityTheory.condEntropy_eq_sum_prod Same as previous lemma, but with a sum over a product space rather than a double sum line 495 source
Source documentation
Same as previous lemma, but with a sum over a product space rather than a double sum.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Finset.sum, Prod, SProd.sprod, Finset, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, Prod.snd and 4 more
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.condEntropy_eq_sum_sum, Prod.mk, Finset.sum_product_right, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_eq_sum_prod (hX : Measurable X) {Y : Ω → T}
    (hY : Measurable Y)
    (μ : Measure Ω) [IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    H[X | Y ; μ] = ∑ p ∈ (FiniteRange.toFinset X) ×ˢ (FiniteRange.toFinset Y),
      (μ.map Y).real {p.2} * negMulLog (((μ[|Y ⁻¹' {p.2}]).map X).real {p.1}) := by
…
```
Mentions: FiniteRange, FiniteRange.toFinset
lemma ProbabilityTheory.condEntropy_of_injective If X : Ω → S, Y : Ω → T are random variables, and f : T × S → U is injective for each fixed t ∈ T, then H[f(Y, X) | Y] = H[X | Y] line 507 source
Source documentation
If X : Ω → S, Y : Ω → T are random variables, and f : T × S → U is injective for each fixed t ∈ T, then H[f(Y, X) | Y] = H[X | Y]. Thus for instance H[X-Y|Y] = H[X|Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Measurable, Function.Injective, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, MeasureTheory.Measure.map, Singleton.singleton, Set, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, id, congrArg, ProbabilityTheory.condEntropy_eq_sum, Function.comp, ProbabilityTheory.entropy_congr, Filter.Eventually, MeasureTheory.ae, ENNReal, Set.ofPred and 31 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_of_injective
    [MeasurableSingletonClass U] (μ : Measure Ω) [IsFiniteMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (f : T → S → U) (hf : ∀ t, Injective (f t)) [FiniteRange Y] :
    H[(fun ω ↦ f (Y ω) (X ω)) | Y ; μ] = H[X | Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_comp_of_injective A weaker version of the above lemma in which f is independent of Y line 527 source
Source documentation
A weaker version of the above lemma in which f is independent of Y.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, Measurable, Function.Injective, Eq, Real, ProbabilityTheory.condEntropy, Function.comp
Proof uses: MeasureTheory.integral_congr_ae, MeasureTheory.Measure.map, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.ae_of_all, ProbabilityTheory.entropy_comp_of_injective
8 instances, coercions and auxiliary constants left out.
```
lemma condEntropy_comp_of_injective {Y : Ω → U}
    (μ : Measure Ω) (hX : Measurable X) (f : S → T) (hf : Injective f) :
    H[f ∘ X | Y ; μ] = H[X | Y ; μ] :=
…
```
lemma ProbabilityTheory.condEntropy_comm H[X, Y| Z] = H[Y, X| Z] line 533 source
Source documentation
H[X, Y| Z] = H[Y, X| Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.condEntropy, Prod, prod
Proof uses: id, Eq.symm, Function.comp, Prod.swap, Prod.mk, ProbabilityTheory.condEntropy_comp_of_injective, Measurable.prodMk, Prod.swap_injective
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_comm [Countable T] {Z : Ω → U}
    (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    H[⟨X, Y⟩ | Z ; μ] = H[⟨Y, X⟩ | Z; μ] := by
…
```
lemma ProbabilityTheory.chain_rule' One form of the chain rule : H[X, Y] = H[X] + H[Y | X] line 548 source
Source documentation
One form of the chain rule : H[X, Y] = H[X] + H[Y | X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HAdd.hAdd, ProbabilityTheory.condEntropy
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.entropy_zero_measure, ProbabilityTheory.condEntropy_zero_measure, add_zero, eq_self, Eq.symm, Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, Eq.mpr, ProbabilityTheory.Kernel.entropy, Unit and 45 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
lemma chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] :
    H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y | X ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.chain_rule Another form of the chain rule : H[X, Y] = H[Y] + H[X | Y] line 575 source
Source documentation
Another form of the chain rule : H[X, Y] = H[Y] + H[X | Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HAdd.hAdd, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.entropy_comm, ProbabilityTheory.chain_rule', Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma chain_rule (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] :
    H[⟨X, Y⟩ ; μ] = H[Y ; μ] + H[X | Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.chain_rule'' Another form of the chain rule : H[X | Y] = H[X, Y] - H[Y] line 581 source
Source documentation
Another form of the chain rule : H[X | Y] = H[X, Y] - H[Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, HSub.hSub, ProbabilityTheory.entropy, Prod, prod
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, ProbabilityTheory.chain_rule, add_sub_cancel_left, Eq.refl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma chain_rule'' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) [FiniteRange X] [FiniteRange Y] :
    H[X | Y ; μ] = H[⟨X, Y⟩ ; μ] - H[Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.IdentDistrib.condEntropy_eq Two pairs of variables that have the same joint distribution, have the same conditional entropy line 588 source
Source documentation
Two pairs of variables that have the same joint distribution, have the same conditional entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, ProbabilityTheory.IdentDistrib, Prod, prod, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy
Proof uses: ProbabilityTheory.IdentDistrib.comp, Prod.snd, measurable_snd, Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, id, congrArg, ProbabilityTheory.chain_rule'', ProbabilityTheory.IdentDistrib.entropy_congr, Eq.refl
5 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma IdentDistrib.condEntropy_eq {Ω' : Type*} [MeasurableSpace Ω'] {X : Ω → S} {Y : Ω → T}
    {μ' : Measure Ω'} {X' : Ω' → S} {Y' : Ω' → T} [IsProbabilityMeasure μ] [IsProbabilityMeasure μ']
    (hX : Measurable X) (hY : Measurable Y) (hX' : Measurable X') (hY' : Measurable Y')
    (h : IdentDistrib (⟨X, Y⟩) (⟨X', Y'⟩) μ μ') [FiniteRange X] [FiniteRange Y] [FiniteRange X']
    [FiniteRange Y'] :
    H[X | Y ; μ] = H[X' | Y' ; μ'] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_of_injective' If X : Ω → S and Y : Ω → T are random variables, and f : T → U is an injection then H[X | f(Y)] = H[X | Y] line 601 source
Source documentation
If X : Ω → S and Y : Ω → T are random variables, and f : T → U is an injection then H[X | f(Y)] = H[X | Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Function.Injective, Function.comp, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, HSub.hSub, ProbabilityTheory.entropy, Prod, prod, id, congrArg, ProbabilityTheory.chain_rule'', HAdd.hAdd, ProbabilityTheory.chain_rule', HSub, Eq.rec, Eq.refl, HAdd, ProbabilityTheory.condEntropy_comp_of_injective, ProbabilityTheory.entropy_comp_of_injective
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_of_injective' (μ : Measure Ω)
    [IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y) (f : T → U)
    (hf : Injective f)
    (hfY : Measurable (f ∘ Y)) [FiniteRange X] [FiniteRange Y] :
    H[X | f ∘ Y ; μ] = H[X | Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_comp_self H[X | f(X)] = H[X] - H[f(X)] line 613 source
Source documentation
H[X | f(X)] = H[X] - H[f(X)].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Countable, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Function.comp, HSub.hSub, ProbabilityTheory.entropy
Proof uses: Eq.mpr, Prod, prod, id, congrArg, ProbabilityTheory.chain_rule'', Measurable.comp, ProbabilityTheory.entropy_prod_comp, Eq.refl
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_comp_self [IsProbabilityMeasure μ] (hX : Measurable X) {f : S → U}
    (hf : Measurable f) [FiniteRange X] : H[X | f ∘ X ; μ] = H[X ; μ] - H[f ∘ X ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.cond_chain_rule' If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z] line 619 source
Source documentation
If X : Ω → S, Y : Ω → T, Z : Ω → U are random variables, then H[X, Y | Z] = H[X | Z] + H[Y|X, Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Prod, prod, HAdd.hAdd
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.condEntropy_zero_measure, add_zero, eq_self, Eq.symm, Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, Eq.mpr, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.condDistrib, Prod.mk and 16 more
32 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
lemma cond_chain_rule' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[⟨X, Y⟩ | Z ; μ] = H[X | Z ; μ] + H[Y | ⟨X, Z⟩ ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.cond_chain_rule H[X, Y | Z] = H[Y | Z] + H[X | Y, Z] line 636 source
Source documentation
H[X, Y | Z] = H[Y | Z] + H[X | Y, Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, Prod, prod, HAdd.hAdd
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.condEntropy_comm, ProbabilityTheory.cond_chain_rule', Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma cond_chain_rule (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) [FiniteRange X] [FiniteRange Y]
    [FiniteRange Z] :
    H[⟨X, Y⟩ | Z ; μ] = H[Y | Z ; μ] + H[X | ⟨Y, Z⟩ ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_comp_le Data-processing inequality for the entropy: H[f(X)] ≤ H[X] line 644 source
Source documentation
Data-processing inequality for the entropy: H[f(X)] ≤ H[X]. To upgrade this to equality, see entropy_of_comp_eq_of_comp or entropy_comp_of_injective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.entropy, Function.comp
Proof uses: Measurable.fun_comp, Measurable.of_discrete, Eq, Prod, prod, Eq.symm, Prod.mk, ProbabilityTheory.entropy_comp_of_injective, And.left, Eq.mp, And, Prod.mk.injEq, Eq.mpr, id, congrArg, HAdd.hAdd, ProbabilityTheory.condEntropy, ProbabilityTheory.chain_rule, OfNat.ofNat, ProbabilityTheory.condEntropy_nonneg
28 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_comp_le (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (f : S → U) [FiniteRange X] :
    H[f ∘ X ; μ] ≤ H[X ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_of_comp_eq_of_comp A Schroder-Bernstein type theorem for entropy : if two random variables are functions of each other, then they have the same entropy line 660 source
Source documentation
A Schroder-Bernstein type theorem for entropy : if two random variables are functions of each other, then they have the same entropy. Can be used as a substitute for entropy_comp_of_injective if one doesn't want to establish the injectivity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Eq, Function.comp, FiniteRange, Real, ProbabilityTheory.entropy
Proof uses: LE.le, Eq.mpr, id, congrArg, ProbabilityTheory.entropy_comp_le, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, OfNat.ofNat, Eq.mp, HAdd.hAdd, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast and 34 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_of_comp_eq_of_comp
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] (hX : Measurable X) (hY : Measurable Y)
    (f : S → T) (g : T → S) (h1 : Y = f ∘ X) (h2 : X = g ∘ Y) [FiniteRange X] [FiniteRange Y] :
    H[X ; μ] = H[Y ; μ] := by
…
```
Mentions: FiniteRange
def ProbabilityTheory.mutualInfo line 679 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.mutualInfo_def line 685 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.mutualInfo, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod
Proof uses: rfl
5 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.entropy_add_entropy_sub_mutualInfo line 688 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, Prod, prod
Proof uses: sub_sub_self
9 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.IdentDistrib.mutualInfo_eq Substituting variables for ones with the same distributions doesn't change the mutual information line 693 source
Source documentation
Substituting variables for ones with the same distributions doesn't change the mutual information.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.IdentDistrib, Prod, prod, Eq, Real, ProbabilityTheory.mutualInfo
Proof uses: ProbabilityTheory.IdentDistrib.comp, Prod.fst, measurable_fst, Prod.snd, measurable_snd, id, Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, congrFun', congrArg, ProbabilityTheory.IdentDistrib.entropy_congr, of_eq_true, Eq.trans, True, eq_self
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma IdentDistrib.mutualInfo_eq {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'}
    {X' : Ω' → S} {Y' : Ω' → T} (hXY : IdentDistrib (⟨X, Y⟩) (⟨X', Y'⟩) μ μ') :
      I[X : Y ; μ] = I[X' : Y' ; μ'] := by
…
```
def ProbabilityTheory.condMutualInfo line 703 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: MeasureTheory.integral, MeasureTheory.Measure.map, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Prod, prod
12 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.condMutualInfo_def line 706 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.condMutualInfo, MeasureTheory.integral, MeasureTheory.Measure.map, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Prod, prod
Proof uses: rfl
11 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.condMutualInfo_eq_integral_mutualInfo line 715 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.condMutualInfo, MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.condMutualInfo_zero_measure line 718 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Eq, Real, ProbabilityTheory.condMutualInfo, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.integral, MeasureTheory.Measure.map, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Prod, prod, MeasureTheory.Measure.map_zero, MeasureTheory.integral_zero_measure, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.mutualInfo_nonneg Mutual information is non-negative line 726 source
Source documentation
Mutual information is non-negative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, FiniteRange, LE.le, Real, OfNat.ofNat, ProbabilityTheory.mutualInfo
Proof uses: id, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod, Eq, MeasureTheory.Measure.map, Prod.fst, Eq.mpr, Function.comp, Prod.mk, congrArg, MeasureTheory.Measure.map_map, measurable_fst, Measurable.prodMk, Eq.rec, Eq.refl, Prod.snd, measurable_snd and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_nonneg (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [FiniteRange X] [FiniteRange Y] :
    0 ≤ I[X : Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_pair_le_add Subadditivity of entropy line 740 source
Source documentation
Subadditivity of entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, FiniteRange, LE.le, Real, ProbabilityTheory.entropy, Prod, prod, HAdd.hAdd
Proof uses: Iff.mp, OfNat.ofNat, HSub.hSub, sub_nonneg, ProbabilityTheory.mutualInfo_nonneg
21 instances, coercions and auxiliary constants left out.
```
lemma entropy_pair_le_add (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) [FiniteRange X]
    [FiniteRange Y] : H[⟨X, Y⟩ ; μ] ≤ H[X ; μ] + H[Y ; μ] :=
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.mutualInfo_eq_zero I[X : Y] = 0 iff X, Y are independent line 745 source
Source documentation
I[X : Y] = 0 iff X, Y are independent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Iff, Eq, Real, ProbabilityTheory.mutualInfo, OfNat.ofNat, ProbabilityTheory.IndepFun
Proof uses: id, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod, MeasureTheory.Measure.map, Prod.fst, Eq.mpr, Function.comp, Prod.mk, congrArg, MeasureTheory.Measure.map_map, measurable_fst, Measurable.prodMk, Eq.rec, Eq.refl, Prod.snd, measurable_snd, ProbabilityTheory.measureEntropy and 23 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_eq_zero (hX : Measurable X) (hY : Measurable Y) {μ : Measure Ω}
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    I[X : Y ; μ] = 0 ↔ IndepFun X Y μ := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.mutualInfo_const The mutual information with a constant is always zero line 764 source
Source documentation
The mutual information with a constant is always zero.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.mutualInfo, OfNat.ofNat
Proof uses: ProbabilityTheory.IndepFun.mutualInfo_eq_zero, measurable_const, ProbabilityTheory.indepFun_const
3 instances, coercions and auxiliary constants left out.
```
lemma mutualInfo_const (hX : Measurable X) (c : T)
    {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ] [FiniteRange X] :
    I[X : fun _ ↦ c ; μ] = 0 :=
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_pair_eq_add H[X, Y] = H[X] + H[Y] if and only if X, Y are independent line 770 source
Source documentation
H[X, Y] = H[X] + H[Y] if and only if X, Y are independent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Iff, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HAdd.hAdd, ProbabilityTheory.IndepFun
Proof uses: Eq.mpr, id, congrArg, propext, eq_comm, HSub.hSub, OfNat.ofNat, Eq.symm, sub_eq_zero, ProbabilityTheory.mutualInfo, ProbabilityTheory.mutualInfo_eq_zero, Iff.rfl
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_pair_eq_add (hX : Measurable X) (hY : Measurable Y) {μ : Measure Ω}
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    H[⟨X, Y⟩ ; μ] = H[X ; μ] + H[Y ; μ] ↔ IndepFun X Y μ := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.iIndepFun.entropy_eq_add line 778 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Nat, MeasurableSpace, MeasurableSingletonClass, Finite, Fin, Measurable, ProbabilityTheory.iIndepFun, Eq, Real, ProbabilityTheory.entropy, Finset.sum, Finset.univ
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Nat.recAux, OfNat.ofNat, Eq.mpr, id, congrArg, Finset.sum_congr, EmptyCollection.emptyCollection, Finset, Finset.univ_eq_empty, Membership.mem, Eq.refl, Fin.elim0, eq_of_heq, HEq, HEq.refl, Eq.symm and 62 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 47 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.mutualInfo_comm I[X : Y] = I[Y : X] line 821 source
Source documentation
I[X : Y] = I[Y : X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.mutualInfo
Proof uses: id, Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod, congrArg, congrFun', add_comm, of_eq_true, Eq.trans, True, ProbabilityTheory.entropy_comm, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_comm (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω) :
    I[X : Y ; μ] = I[Y : X ; μ] := by simp_rw [mutualInfo, add_comm, entropy_comm hX hY]
```
Mentions: ProbabilityTheory.mutualInfo, ProbabilityTheory.entropy_comm
lemma ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy I[X : Y] = H[X] - H[X|Y] line 825 source
Source documentation
I[X : Y] = H[X] - H[X|Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.mutualInfo, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, HAdd.hAdd, Prod, prod, id, congrArg, ProbabilityTheory.mutualInfo_def, ProbabilityTheory.chain_rule
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_eq_entropy_sub_condEntropy
    (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    I[X : Y ; μ] = H[X ; μ] - H[X | Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy' I[X : Y] = H[Y] - H[Y | X] line 833 source
Source documentation
I[X : Y] = H[Y] - H[Y | X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.mutualInfo, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.mutualInfo_comm, ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy, Eq.refl
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma mutualInfo_eq_entropy_sub_condEntropy' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    I[X : Y ; μ] = H[Y ; μ] - H[Y | X ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy H[X] - I[X : Y] = H[X | Y] line 839 source
Source documentation
H[X] - I[X : Y] = H[X | Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy, sub_sub_self, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_eq_condEntropy (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    H[X ; μ] - I[X : Y ; μ] = H[X | Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_sub_mutualInfo_eq_condEntropy' H[Y] - I[X : Y] = H[Y | X] line 845 source
Source documentation
H[Y] - I[X : Y] = H[Y | X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.mutualInfo, ProbabilityTheory.condEntropy
Proof uses: Eq.mpr, id, congrArg, ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy', sub_sub_self, Eq.refl
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_mutualInfo_eq_condEntropy' (hX : Measurable X) (hY : Measurable Y) (μ : Measure Ω)
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
    H[Y ; μ] - I[X : Y ; μ] = H[Y | X ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.IndepFun.condEntropy_eq_entropy line 850 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, ProbabilityTheory.IndepFun, Measurable, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condEntropy, ProbabilityTheory.entropy
Proof uses: ProbabilityTheory.mutualInfo, OfNat.ofNat, ProbabilityTheory.IndepFun.mutualInfo_eq_zero, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HAdd.hAdd, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring and 40 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condMutualInfo_eq_kernel_mutualInfo The conditional mutual information agrees with the information of the conditional kernel line 862 source
Source documentation
The conditional mutual information agrees with the information of the conditional kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condMutualInfo, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.condDistrib, Prod, prod, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.FiniteSupport, Exists, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, id, MeasureTheory.integral, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.measureEntropy, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd and 51 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_eq_kernel_mutualInfo
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange Z] :
    I[X : Y | Z ; μ] = Ik[condDistrib (⟨X, Y⟩) Z μ, μ.map Z] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutualInfo_eq_sum line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, MeasureTheory.IsFiniteMeasure, Measurable, FiniteRange, Eq, Real, ProbabilityTheory.condMutualInfo, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond
Proof uses: Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.map, id, congrArg, ProbabilityTheory.condMutualInfo_eq_integral_mutualInfo, MeasureTheory.Measure.restrict, Finset, MeasureTheory.integral_eq_setIntegral, ProbabilityTheory.ae_mem_of_finiteRange, HSMul.hSMul, MeasureTheory.setIntegral_finset, MeasureTheory.IntegrableOn.finset, AddCommMonoid, Eq.rec, Eq.refl, funext, MeasureTheory.map_measureReal_apply, MeasurableSet.singleton
34 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condMutualInfo_eq_sum' A variant of condMutualInfo_eq_sum when Z has finite codomain line 904 source
Source documentation
A variant of condMutualInfo_eq_sum when Z has finite codomain.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, MeasureTheory.IsFiniteMeasure, Measurable, Fintype, Eq, Real, ProbabilityTheory.condMutualInfo, Finset.sum, Finset.univ, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond
Proof uses: Eq.mpr, FiniteRange.toFinset, id, congrArg, ProbabilityTheory.condMutualInfo_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 condMutualInfo_eq_sum' [MeasurableSingletonClass U] [IsFiniteMeasure μ]
    (hZ : Measurable Z) [Fintype U] :
    I[X : Y | Z ; μ] = ∑ z, μ.real (Z ⁻¹' {z}) * I[X : Y ; (μ[|Z ← z])] := by
…
```
lemma ProbabilityTheory.condMutualInfo_nonneg Conditional information is non-nonegative line 922 source
Source documentation
Conditional information is non-nonegative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Measurable, MeasureTheory.Measure, FiniteRange, LE.le, Real, OfNat.ofNat, ProbabilityTheory.condMutualInfo
Proof uses: MeasureTheory.integral_nonneg, MeasureTheory.Measure.map, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Prod, prod, ProbabilityTheory.mutualInfo_nonneg
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_nonneg (hX : Measurable X) (hY : Measurable Y) {Z : Ω → U} {μ : Measure Ω}
    [FiniteRange X] [FiniteRange Y] :
    0 ≤ I[X : Y | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutualInfo_comm I[X : Y | Z] = I[Y : X | Z] line 931 source
Source documentation
I[X : Y | Z] = I[Y : X | Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.condMutualInfo
Proof uses: id, Eq.mpr, MeasureTheory.integral, MeasureTheory.Measure.map, HSub.hSub, HAdd.hAdd, ProbabilityTheory.entropy, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Prod, prod, congrArg, funext, congrFun', add_comm, of_eq_true, Eq.trans, True and 2 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_comm
    (hX : Measurable X) (hY : Measurable Y) (Z : Ω → U) (μ : Measure Ω) :
    I[X : Y | Z ; μ] = I[Y : X | Z ; μ] := by
…
```
lemma ProbabilityTheory.condMutualInfo_eq I[X : Y| Z] = H[X| Z] + H[Y| Z] - H[X, Y| Z] line 939 source
Source documentation
I[X : Y| Z] = H[X| Z] + H[Y| Z] - H[X, Y| Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condMutualInfo, HSub.hSub, HAdd.hAdd, ProbabilityTheory.condEntropy, Prod, prod
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.condMutualInfo_zero_measure, ProbabilityTheory.condEntropy_zero_measure, add_zero, sub_self, eq_self, Eq.symm, Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, Eq.mpr, ProbabilityTheory.Kernel.mutualInfo and 15 more
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_eq [Countable U]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange Z] :
    I[X : Y | Z ; μ] = H[X | Z ; μ] + H[Y | Z; μ] - H[⟨X, Y⟩ | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutualInfo_eq' I[X : Y| Z] = H[X| Z] - H[X|Y, Z] line 954 source
Source documentation
I[X : Y| Z] = H[X| Z] - H[X|Y, Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.condMutualInfo, HSub.hSub, ProbabilityTheory.condEntropy, Prod, prod
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, ProbabilityTheory.condMutualInfo_eq, ProbabilityTheory.cond_chain_rule, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, OfNat.ofNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 20 more
33 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_eq' [Countable U]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    I[X : Y | Z ; μ] = H[X | Z ; μ] - H[X | ⟨Y, Z⟩ ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutualInfo_of_inj_map If f(Z, X) is injective for each fixed Z, then I[f(Z, X) : Y| Z] = I[X : Y| Z] line 962 source
Source documentation
If f(Z, X) is injective for each fixed Z, then I[f(Z, X) : Y| Z] = I[X : Y| Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, Function.Injective, FiniteRange, Eq, Real, ProbabilityTheory.condMutualInfo
Proof uses: Function.comp, Prod, Function.uncurry, prod, Measurable.fun_comp, Prod.fst, Prod.snd, Prod.mk, Measurable.of_discrete, Measurable.prodMk, Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.condEntropy, id, congrArg, ProbabilityTheory.condMutualInfo_eq, Iff.mpr, And, Prod.ext_iff and 7 more
10 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_of_inj_map [Countable U] [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    {V : Type*} [MeasurableSpace V] [MeasurableSingletonClass V] [Countable V]
    (f : U → S → V) (hf : ∀ t, Function.Injective (f t)) [FiniteRange Z] :
    I[fun ω ↦ f (Z ω) (X ω) : Y | Z ; μ] =
    I[X : Y | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutualInfo_of_inj line 976 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Function.Injective, Eq, Real, ProbabilityTheory.condMutualInfo, Function.comp
Proof uses: Measurable.fun_comp, Measurable.of_discrete, Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.condEntropy, Prod, prod, id, congrArg, ProbabilityTheory.condMutualInfo_eq, ProbabilityTheory.condEntropy_of_injective', Prod.mk, Measurable.prodMk, Eq.refl
10 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condMutualInfo_of_inj' line 988 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Function.Injective, Eq, Real, ProbabilityTheory.condMutualInfo, Function.comp
Proof uses: Trans.trans, Eq.mpr, id, congrArg, ProbabilityTheory.condMutualInfo_of_inj, Measurable.fun_comp, Measurable.of_discrete, Eq.refl, ProbabilityTheory.condMutualInfo_of_inj_map, ProbabilityTheory.condMutualInfo_comm
3 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condEntropy_prod_eq_of_indepFun line 1008 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, Finite, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, ProbabilityTheory.IndepFun, Prod, prod, Eq, Real, ProbabilityTheory.condEntropy
Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.condEntropy_zero_measure, eq_self, Eq.symm, Eq.mpr, Finset.sum, Finset.univ, HMul.hMul and 33 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condMutualInfo_eq_zero I[X : Y| Z]=0 iff X, Y are conditionally independent over Z line 1036 source
Source documentation
I[X : Y| Z]=0 iff X, Y are conditionally independent over Z.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, Measurable, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Iff, Eq, Real, ProbabilityTheory.condMutualInfo, OfNat.ofNat, ProbabilityTheory.CondIndepFun
Proof uses: Eq.mpr, Filter.Eventually, ProbabilityTheory.IndepFun, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, MeasureTheory.ae, MeasureTheory.Measure.map, id, congrArg, propext, ProbabilityTheory.condIndepFun_iff, MeasureTheory.integral, ProbabilityTheory.mutualInfo, ProbabilityTheory.condMutualInfo_eq_integral_mutualInfo, Filter.EventuallyEq, MeasureTheory.integral_eq_zero_iff_of_nonneg, dite, LE.le and 22 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma condMutualInfo_eq_zero (hX : Measurable X) (hY : Measurable Y)
    [IsZeroOrProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    I[X : Y | Z ; μ] = 0 ↔ CondIndepFun X Y Z μ := by
…
```
Mentions: FiniteRange, ProbabilityTheory.CondIndepFun
lemma ProbabilityTheory.ent_of_cond_indep If X, Y are conditionally independent over Z, then H[X, Y, Z] = H[X, Z] + H[Y, Z] - H[Z] line 1058 source
Source documentation
If X, Y are conditionally independent over Z, then H[X, Y, Z] = H[X, Z] + H[Y, Z] - H[Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, Measurable, ProbabilityTheory.CondIndepFun, MeasureTheory.IsZeroOrProbabilityMeasure, FiniteRange, Eq, Real, ProbabilityTheory.entropy, Prod, prod, HSub.hSub, HAdd.hAdd
Proof uses: ProbabilityTheory.condMutualInfo, OfNat.ofNat, Iff.mpr, ProbabilityTheory.condMutualInfo_eq_zero, Eq.mpr, id, congrArg, ProbabilityTheory.entropy_assoc, ProbabilityTheory.condEntropy, Prod.mk, ProbabilityTheory.chain_rule, Measurable.prodMk, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HMul.hMul and 46 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma ent_of_cond_indep (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
     (h : CondIndepFun X Y Z μ) [IsZeroOrProbabilityMeasure μ]
     [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
     H[⟨X, ⟨Y, Z⟩⟩ ; μ] = H[⟨X, Z⟩; μ] + H[⟨Y, Z⟩; μ] - H[Z; μ] := by
…
```
Mentions: ProbabilityTheory.CondIndepFun, FiniteRange
lemma ProbabilityTheory.entropy_sub_condEntropy H[X] - H[X|Y] = I[X : Y] line 1071 source
Source documentation
H[X] - H[X|Y] = I[X : Y]

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, Eq, Real, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, ProbabilityTheory.mutualInfo
Proof uses: Eq.mpr, HAdd.hAdd, Prod, prod, id, congrArg, ProbabilityTheory.mutualInfo_def, ProbabilityTheory.chain_rule, add_comm, add_sub_add_left_eq_sub, Eq.refl
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_sub_condEntropy (hX : Measurable X) (hY : Measurable Y) [FiniteRange X]
    [FiniteRange Y] : H[X ; μ] - H[X | Y ; μ] = I[X : Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_le_entropy H[X | Y] ≤ H[X] line 1076 source
Source documentation
H[X | Y] ≤ H[X].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.condEntropy, ProbabilityTheory.entropy
Proof uses: Iff.mp, OfNat.ofNat, HSub.hSub, sub_nonneg, Eq.mpr, ProbabilityTheory.mutualInfo, id, Eq, congrArg, ProbabilityTheory.entropy_sub_condEntropy, ProbabilityTheory.mutualInfo_nonneg
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_le_entropy (hX : Measurable X) (hY : Measurable Y) [FiniteRange X]
    [FiniteRange Y] : H[X | Y ; μ] ≤ H[X ; μ] :=
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_submodular H[X | Y, Z] ≤ H[X | Z] line 1081 source
Source documentation
H[X | Y, Z] ≤ H[X | Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.condEntropy, Prod, prod
Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.condEntropy_zero_measure, Eq.symm, Nonempty, Nonempty.map, MeasureTheory.Measure.nonempty_of_neZero, Eq.mpr, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, id and 13 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_submodular (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[X | ⟨Y, Z⟩ ; μ] ≤ H[X | Z ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condEntropy_comp_ge Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective' line 1096 source
Source documentation
Data-processing inequality for the conditional entropy: H[Y|f(X)] ≥ H[Y|X] To upgrade this to equality, see condEntropy_of_injective'

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, FiniteRange, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, GE.ge, Real, ProbabilityTheory.condEntropy, Function.comp
Proof uses: Eq, ProbabilityTheory.entropy, Prod, prod, Prod.mk, id, ProbabilityTheory.entropy_comp_of_injective, Measurable.prod, Prod.ext, And.left, Prod.fst, And, Prod.snd, Eq.mp, congrArg, Prod.mk.injEq, And.right, Measurable.fun_comp, Measurable.of_discrete, Eq.mpr and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
lemma condEntropy_comp_ge
    [FiniteRange X] [FiniteRange Y] (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ]
    (hX : Measurable X) (hY : Measurable Y) (f : S → U) : H[Y | f ∘ X ; μ] ≥ H[Y | X; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.entropy_triple_add_entropy_le The submodularity inequality: H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z] line 1111 source
Source documentation
The submodularity inequality: H[X, Y, Z] + H[Z] ≤ H[X, Z] + H[Y, Z].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Countable, MeasureTheory.IsZeroOrProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, HAdd.hAdd, ProbabilityTheory.entropy, Prod, prod
Proof uses: Eq.mpr, Prod.mk, ProbabilityTheory.condEntropy, id, Eq, congrArg, ProbabilityTheory.chain_rule, Measurable.prodMk, HMul.hMul, OfNat.ofNat, Nat, congr, Eq.trans, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl and 18 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_triple_add_entropy_le (hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    H[⟨X, ⟨Y, Z⟩⟩ ; μ] + H[Z ; μ] ≤ H[⟨X, Z⟩ ; μ] + H[⟨Y, Z⟩ ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.mutual_comp_le Let X, Ybe random variables line 1145 source
Source documentation
Let X, Ybe random variables. For any function f, g on the range of X, we have I[f(X) : Y] ≤ I[X : Y].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.mutualInfo, Function.comp
Proof uses: Measurable.fun_comp, Measurable.of_discrete, Eq.mpr, id, Eq, congrArg, ProbabilityTheory.mutualInfo_comm, HSub.hSub, ProbabilityTheory.entropy, ProbabilityTheory.condEntropy, ProbabilityTheory.mutualInfo_eq_entropy_sub_condEntropy, sub_le_sub_left, ProbabilityTheory.condEntropy_comp_ge
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma mutual_comp_le [Countable U] (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (f : S → U) [FiniteRange X] [FiniteRange Y] :
    I[f ∘ X : Y ; μ] ≤ I[X : Y ; μ] := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.mutual_comp_comp_le Let X, Y be random variables line 1156 source
Source documentation
Let X, Y be random variables. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.mutualInfo, Function.comp
Proof uses: Trans.trans, Eq, ProbabilityTheory.mutual_comp_le, Measurable.comp, ProbabilityTheory.mutualInfo_comm
7 instances, coercions and auxiliary constants left out.
```
lemma mutual_comp_comp_le [Countable U] (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (f : S → U) (g : T → V) (hg : Measurable g)
    [FiniteRange X] [FiniteRange Y] :
    I[f ∘ X : g ∘ Y ; μ] ≤ I[X : Y ; μ] :=
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.condMutual_comp_comp_le Let X, Y, Z line 1168 source
Source documentation
Let X, Y, Z. For any functions f, g on the ranges of X, Y respectively, we have I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Measurable, FiniteRange, LE.le, Real, ProbabilityTheory.condMutualInfo, Function.comp
Proof uses: Eq.mpr, Finset.sum, FiniteRange.toFinset, HMul.hMul, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, ProbabilityTheory.mutualInfo, ProbabilityTheory.cond, id, Eq, congrArg, ProbabilityTheory.condMutualInfo_eq_sum, Finset.sum_le_sum, Membership.mem, Finset, OfNat.ofNat, LT.lt, Or and 23 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma condMutual_comp_comp_le (μ : Measure Ω) [IsProbabilityMeasure μ] (hX : Measurable X)
    (hY : Measurable Y) (hZ : Measurable Z) (f : S → V) (g : T → W) (hg : Measurable g)
    [FiniteRange X] [FiniteRange Y] [FiniteRange Z] :
    I[f ∘ X : g ∘ Y | Z ; μ] ≤ I[X : Y | Z ; μ] := by
…
```
Mentions: FiniteRange
example (example at line 1197) line 1197 source
Source documentation
An example to illustrate how MeasureSpace can be used to suppress the ambient measure.
```
example (hX : Measurable X) (hY : Measurable Y) :
  H[⟨X, Y⟩] = H[Y] + H[X | Y] := chain_rule _ hX hY
…
```