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

53 declarations, 0 contain sorry, 0 declared as axioms

Entropy of a measure

Main definitions

measureEntropy: entropy of a measure μ, denoted by Hm[μ]
measureMutualInfo: mutual information of a measure over a product space, denoted by Im[μ], equal to Hm[μ.map Prod.fst] + Hm[μ.map Prod.snd] - Hm[μ]

Notations

Hm[μ] = measureEntropy μ
Im[μ] = measureMutualInfo μ

Imports (9)

Imported by 2 files

def ProbabilityTheory.measureEntropy line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Real
Proof uses: tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ, Singleton.singleton, SummationFilter.unconditional
17 instances, coercions and auxiliary constants left out.
class ProbabilityTheory.FiniteSupport A measure has finite support if there exists a finite set whose complement has zero measure line 57 source
Source documentation
A measure has finite support if there exists a finite set whose complement has zero measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure
1 instances, coercions and auxiliary constants left out.
```
class FiniteSupport (μ : Measure S := by volume_tac) : Prop where
…
```
def ProbabilityTheory._root_.MeasureTheory.Measure.support line 62 source
lemma ProbabilityTheory.measure_compl_support line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, Eq, ENNReal, Set, Compl.compl, Finset, MeasureTheory.Measure.support, OfNat.ofNat
Proof uses: Exists.choose, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, ProbabilityTheory.FiniteSupport.finite, LE.le, Union.union, Set.iUnion, Finset.filter, Singleton.singleton, dite, Classical.propDecidable, of_eq_true, Eq.trans, Or, And, True, congrFun', congrArg and 43 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.ae_mem_support line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, Filter.Eventually, Membership.mem, Finset, MeasureTheory.Measure.support, MeasureTheory.ae
Proof uses: ProbabilityTheory.measure_compl_support
4 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.mem_support line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, Iff, Membership.mem, Finset, MeasureTheory.Measure.support, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat
Proof uses: Iff.intro, And.right, Exists.choose, Filter.Eventually, MeasureTheory.ae, autoParam, ProbabilityTheory.FiniteSupport.finite, Not, Eq, Eq.mp, And, Eq.trans, Finset.filter, congrFun', congrArg, Finset.filter_congr, Iff.of_eq, Eq.refl, Mathlib.Tactic.Contrapose.contrapose₂, MeasureTheory.measure_mono_null and 5 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.finiteSupport_zero line 99 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.FiniteSupport, OfNat.ofNat, MeasureTheory.Measure
Proof uses: ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, False, Bot.bot, Filter, True, congr, congrArg, funext, MeasureTheory.ae_zero
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def ProbabilityTheory.FiniteEntropy TODO: replace FiniteSupport hypotheses ∈ these files with FiniteEntropy hypotheses line 103 source
Source documentation
TODO: replace FiniteSupport hypotheses ∈ these files with FiniteEntropy hypotheses.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure
Proof uses: And, Summable, Real, Real.negMulLog, ENNReal.toReal, Set, ENNReal, HSMul.hSMul, Inv.inv, Set.univ, Singleton.singleton, SummationFilter.unconditional, Exists, Countable, Eq, Compl.compl, OfNat.ofNat
21 instances, coercions and auxiliary constants left out.
```
noncomputable def FiniteEntropy (μ : Measure S := by volume_tac) : Prop :=
…
```
instance ProbabilityTheory.finiteSupport_of_fintype line 107 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finite, ProbabilityTheory.FiniteSupport
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, Finset.univ, of_eq_true, Eq.trans, True, congrFun', Filter, congrArg, funext and 1 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.finiteSupport_of_mul line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, ENNReal, HSMul.hSMul
Proof uses: ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, MeasureTheory.Measure.support, MeasureTheory.Measure.ae_smul_measure, ProbabilityTheory.ae_mem_support
23 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.finiteSupport_of_comp line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, Measurable, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, Finset.image, Classical.propDecidable, Eq, MeasureTheory.Measure.support, Eq.mpr, id, congrArg, propext, MeasureTheory.ae_map_iff, Measurable.aemeasurable, Set.Finite.measurableSet, Finset.finite_toSet, Filter.mp_mem and 5 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.finiteSupport_of_dirac line 127 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.FiniteSupport, MeasureTheory.Measure.dirac
Proof uses: ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, MeasureTheory.Measure, Singleton.singleton, of_eq_true, Eq.trans, Eq, True, Pure.pure, Filter, congr, congrArg, funext, MeasureTheory.ae_dirac_eq, eq_self
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.full_measure_of_finiteRange duplicate of FiniteRange.null_of_compl line 130 source
Source documentation
duplicate of FiniteRange.null_of_compl

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, FiniteRange, Eq, ENNReal, Set, MeasureTheory.Measure.map, Compl.compl, Finset, FiniteRange.toFinset, OfNat.ofNat
Proof uses: Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.compl, Finset.measurableSet, EmptyCollection.emptyCollection, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, DFunLike, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans and 12 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma full_measure_of_finiteRange {μ : Measure Ω} {X : Ω → S}
    (hX : Measurable X) [hX' : FiniteRange X] :
    (μ.map X) hX'.toFinsetᶜ = 0 := by
…
```
Mentions: FiniteRange
lemma ProbabilityTheory.ae_mem_of_finiteRange line 138 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, FiniteRange, Filter.Eventually, Membership.mem, Finset, FiniteRange.toFinset, MeasureTheory.ae, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.full_measure_of_finiteRange
4 instances, coercions and auxiliary constants left out.
instance ProbabilityTheory.finiteSupport_of_finiteRange line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, FiniteRange, ProbabilityTheory.FiniteSupport, MeasureTheory.Measure.map
Proof uses: dite, AEMeasurable, Classical.propDecidable, ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, FiniteRange.toFinset, FiniteRange.null_of_compl, Not, Eq, OfNat.ofNat, Ne, Or, eq_or_ne, EmptyCollection.emptyCollection, of_eq_true and 28 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.finiteSupport_of_prod line 153 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, MeasureTheory.SigmaFinite, Prod, MeasureTheory.Measure.prod
Proof uses: ProbabilityTheory.FiniteSupport.mk, Exists.intro, Finset, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, SProd.sprod, MeasureTheory.Measure.support, MeasureTheory.Measure.prod_of_full_measure_finset, ProbabilityTheory.measure_compl_support
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.integrable_of_finiteSupport Every function is integrable against a finite measure with finite support line 160 source
Source documentation
Every function is integrable against a finite measure with finite support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, NormedAddCommGroup, MeasureTheory.IsFiniteMeasure, MeasureTheory.Integrable
Proof uses: MeasureTheory.IntegrableOn, Finset, MeasureTheory.Measure.support, MeasureTheory.IntegrableOn.finset, Eq.mp, MeasureTheory.Measure.restrict, congrArg, MeasureTheory.Measure.restrict_eq_self_of_ae_mem, ProbabilityTheory.ae_mem_support, MeasureTheory.IntegrableOn.eq_1
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma integrable_of_finiteSupport (μ : Measure S) [FiniteSupport μ]
    {β : Type*} [NormedAddCommGroup β] [IsFiniteMeasure μ]
    {f : S → β} : Integrable f μ := by
…
```
Mentions: ProbabilityTheory.FiniteSupport
lemma ProbabilityTheory.integral_congr_finiteSupport line 166 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, NormedAddCommGroup, NormedSpace, Real, ProbabilityTheory.FiniteSupport, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, Eq, MeasureTheory.integral
Proof uses: MeasureTheory.integral_congr_ae, MeasureTheory.measure_mono_null, Compl.compl, Set.ofPred, Finset, MeasureTheory.Measure.support, Membership.mem, Iff.mp, ProbabilityTheory.mem_support, ProbabilityTheory.measure_compl_support
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport This generalizes Measure.ext_iff_singleton ∈ MeasureReal line 173 source
Source documentation
This generalizes Measure.ext_iff_singleton ∈ MeasureReal

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, Iff, Eq, ENNReal, Set, Singleton.singleton
Proof uses: Iff.intro, of_eq_true, Eq.trans, True, forall_congr, eq_self, implies_true, Finset, MeasureTheory.Measure.support, Compl.compl, OfNat.ofNat, ProbabilityTheory.measure_compl_support, MeasureTheory.Measure.ext, MeasurableSet, Inter.inter, Union.union, Eq.symm, MeasureTheory.measure_eq_measure_of_null_sdiff, LE.le, MeasureTheory.measure_mono_null and 24 more
35 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
theorem Measure.ext_iff_singleton_finiteSupport
    {μ1 μ2 : Measure S} [FiniteSupport μ1] [FiniteSupport μ2] :
    μ1 = μ2 ↔ ∀ x, μ1 {x} = μ2 {x} := by
…
```
Mentions: ProbabilityTheory.FiniteSupport
theorem ProbabilityTheory.Measure.ext_iff_measureReal_singleton_finiteSupport line 201 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, MeasureTheory.IsFiniteMeasure, Iff, Eq, Real, MeasureTheory.Measure.real, Singleton.singleton, Set
Proof uses: Eq.mpr, ENNReal, id, congrArg, propext, ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport, iff_of_eq, pi_congr, Ne, Top.top, MeasureTheory.measure_ne_top, ENNReal.toReal, MeasureTheory.measureReal_def, Or, And, OfNat.ofNat, ENNReal.toReal_eq_toReal_iff, of_eq_true, Eq.trans, True and 9 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_eq_sum line 213 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, Real, ProbabilityTheory.measureEntropy, Finset.sum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, Inv.inv, Set.univ, Singleton.singleton
Proof uses: id, Eq.mpr, tsum, SummationFilter.unconditional, congrArg, tsum_eq_sum, Not, Membership.mem, ENNReal.toReal, MeasureTheory.Measure.real.eq_1, MeasureTheory.measure_mono_null, LE.le, Eq.trans, of_eq_true, eq_self, True, congrFun', HMul.hMul, MeasureTheory.measureReal_ennreal_smul_apply, congr and 4 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_zero line 223 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Eq, Real, ProbabilityTheory.measureEntropy, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ, Singleton.singleton, SummationFilter.unconditional, SummationFilter, optParam, funext, Top.top, ENNReal.inv_zero and 4 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_dirac line 226 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.dirac, OfNat.ofNat
Proof uses: Eq.mpr, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, MeasureTheory.Measure, Inv.inv, Set, Set.univ, Singleton.singleton, SummationFilter.unconditional, id, congrArg, ProbabilityTheory.measureEntropy.eq_1, congrFun', SummationFilter, optParam, funext, Eq.trans and 23 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_of_not_isFiniteMeasure line 235 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Not, MeasureTheory.IsFiniteMeasure, Eq, Real, ProbabilityTheory.measureEntropy, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ, Singleton.singleton, SummationFilter.unconditional, SummationFilter, optParam, funext, Top.top, Iff.mp and 6 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_of_isProbabilityMeasure line 238 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, Real, ProbabilityTheory.measureEntropy, tsum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton, Set, SummationFilter.unconditional
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, HSMul.hSMul, ENNReal, Inv.inv, Set.univ, congrFun', SummationFilter, optParam, funext, Top.top, ENNReal.inv_zero, smul_zero and 7 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_of_isProbabilityMeasure' line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, Real, ProbabilityTheory.measureEntropy, tsum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton, Set, SummationFilter.unconditional
Proof uses: ProbabilityTheory.measureEntropy_of_isProbabilityMeasure
5 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.measureEntropy_of_isProbabilityMeasure_finite line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, MeasureTheory.IsZeroOrProbabilityMeasure, Real, ProbabilityTheory.measureEntropy, Finset.sum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton
Proof uses: Eq.mpr, HSMul.hSMul, Inv.inv, Set.univ, id, congrArg, ProbabilityTheory.measureEntropy_eq_sum, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, Finset.sum_congr, Eq.refl, Membership.mem, congrFun', Top.top, ENNReal.inv_zero and 9 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_of_isProbabilityMeasure_finite' line 254 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, MeasureTheory.IsZeroOrProbabilityMeasure, Real, ProbabilityTheory.measureEntropy, Finset.sum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton
Proof uses: ProbabilityTheory.measureEntropy_of_isProbabilityMeasure_finite
16 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.measureEntropy_univ_smul line 259 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.measureEntropy, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ
Proof uses: dite, MeasureTheory.IsFiniteMeasure, Classical.propDecidable, OfNat.ofNat, NeZero, Or, eq_zero_or_neZero, Or.inl, of_eq_true, Eq.trans, True, congr, congrArg, Top.top, congrFun', ENNReal.inv_zero, smul_zero, ProbabilityTheory.measureEntropy_zero, eq_self, Or.inr and 25 more
64 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_nonneg line 269 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, LE.le, Real, OfNat.ofNat, ProbabilityTheory.measureEntropy
Proof uses: dite, MeasureTheory.IsFiniteMeasure, Classical.propDecidable, tsum_nonneg, SummationFilter.unconditional, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ, Singleton.singleton, Real.negMulLog_nonneg, MeasureTheory.measureReal_nonneg, ENNReal.toReal_le_of_le_ofReal, zero_le_one, Eq.mpr, ENNReal.ofReal, id and 21 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_le_card_aux Auxiliary lemma for measureEntropy_le_log_card_of_mem, which removes the probability measure assumption line 285 source
Source documentation
Auxiliary lemma for measureEntropy_le_log_card_of_mem, which removes the probability measure assumption.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, LE.le, Real, ProbabilityTheory.measureEntropy, Real.log, Finset.card
Proof uses: Eq.mpr, id, congrArg, Eq.symm, compl_compl, HSub.hSub, Set.univ, MeasureTheory.measure_compl, MeasurableSet.compl, Finset.measurableSet, MeasureTheory.measure_ne_top, of_eq_true, Eq.trans, True, congrFun', MeasureTheory.IsProbabilityMeasure.measure_univ, tsub_zero, eq_self, Nat, LT.lt and 63 more
169 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma measureEntropy_le_card_aux {μ : Measure S} [IsProbabilityMeasure μ]
    (A : Finset S) (hμ : μ Aᶜ = 0) :
    Hm[μ] ≤ log A.card := by
…
```
lemma ProbabilityTheory.measureEntropy_eq_card_iff_measureReal_eq_aux line 317 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Fintype, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Iff, Eq, Real, ProbabilityTheory.measureEntropy, Real.log, Fintype.card, MeasureTheory.Measure.real, Singleton.singleton, Set, Inv.inv
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Or.inl, of_eq_true, Eq.trans, True, congr, congrArg, OfNat.ofNat, Subsingleton.elim, ProbabilityTheory.measureEntropy_zero, Nat, Fintype.card_eq_zero, CharP.cast_eq_zero, Real.log_zero, eq_self, forall_congr, congrFun' and 63 more
137 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq_aux line 338 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Fintype, MeasureTheory.IsProbabilityMeasure, Iff, Eq, Real, ProbabilityTheory.measureEntropy, Real.log, Fintype.card, ENNReal, Set, Singleton.singleton, Inv.inv, NNReal
Proof uses: Eq.mpr, MeasureTheory.Measure.real, id, congrArg, propext, ProbabilityTheory.measureEntropy_eq_card_iff_measureReal_eq_aux, iff_of_eq, pi_congr, ENNReal.toReal, MeasureTheory.measureReal_def, Eq.symm, ENNReal.toReal_eq_toReal_iff', MeasureTheory.measure_ne_top, of_eq_true, Not, Top.top, Eq.trans, False, True, not_false_eq_true and 4 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_le_log_card_of_mem line 347 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Finset, MeasureTheory.Measure, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, LE.le, Real, ProbabilityTheory.measureEntropy, Real.log, Finset.card
Proof uses: Nat.card, Subtype, Membership.mem, Real.log_natCast_nonneg, NeZero, Or, eq_zero_or_neZero, Eq.mpr, id, Eq.trans, congrFun', congrArg, ProbabilityTheory.measureEntropy_zero, Eq.symm, dite, MeasureTheory.IsFiniteMeasure, Classical.propDecidable, HSMul.hSMul, Inv.inv, Set.univ and 8 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_le_log_card line 360 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Fintype, MeasureTheory.Measure, LE.le, Real, ProbabilityTheory.measureEntropy, Real.log, Fintype.card
Proof uses: ProbabilityTheory.measureEntropy_le_log_card_of_mem, Finset.univ, of_eq_true, Eq, ENNReal, Set, Compl.compl, Finset, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Set.univ, Finset.coe_univ, Set.compl_univ, MeasureTheory.measure_empty, eq_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_eq_card_iff_measureReal_eq line 363 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Fintype, MeasureTheory.IsFiniteMeasure, NeZero, Iff, Eq, Real, ProbabilityTheory.measureEntropy, Real.log, Fintype.card, MeasureTheory.Measure.real, Singleton.singleton, Set, HDiv.hDiv, Set.univ
Proof uses: Eq.mpr, HSMul.hSMul, ENNReal, Inv.inv, id, congrArg, Eq.symm, ProbabilityTheory.measureEntropy_univ_smul, eq_of_heq, HEq, Eq.refl, HEq.refl, pi_congr, propext, HMul.hMul, ENNReal.toReal, congrFun', MeasureTheory.measureReal_ennreal_smul_apply, ENNReal.toReal_inv, inv_mul_eq_iff_eq_mul₀ and 4 more
49 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.entropy_of_uniformOn The entropy of a uniform measure is the log of the cardinality of its support line 373 source
Source documentation
The entropy of a uniform measure is the log of the cardinality of its support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Set, Nonempty, Finite, Eq, Real, ProbabilityTheory.measureEntropy, ProbabilityTheory.uniformOn, Real.log, Nat.card
Proof uses: Eq.mpr, tsum, Real.negMulLog, HDiv.hDiv, Inter.inter, Singleton.singleton, SummationFilter.unconditional, id, congrFun', congrArg, SummationFilter, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, MeasureTheory.Measure, Inv.inv, Set.univ, optParam, funext, Eq.trans and 73 more
123 instances, coercions and auxiliary constants left out.

Tactic trace: 21 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_of_uniformOn (H : Set S) [Nonempty H] [Finite H] :
    measureEntropy (uniformOn H) = log (Nat.card H) := by
…
```
Mentions: ProbabilityTheory.measureEntropy
lemma ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq line 394 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasurableSingletonClass, Fintype, MeasureTheory.IsFiniteMeasure, NeZero, Iff, Eq, Real, ProbabilityTheory.measureEntropy, Real.log, Fintype.card, ENNReal, Set, Singleton.singleton, HDiv.hDiv, Set.univ
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, OfNat.ofNat, Subsingleton.elim, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.measureEntropy_zero, Nat, Fintype.card_eq_zero, CharP.cast_eq_zero, Real.log_zero, eq_self, forall_congr, congrFun', ENNReal.zero_div and 27 more
71 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_map_of_injective line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Measurable, Function.Injective, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map
Proof uses: ENNReal, Set, Set.univ, Eq.mpr, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.univ, of_eq_true, eq_self, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, Inv.inv, Singleton.singleton, SummationFilter.unconditional, ENNReal.toReal, congr and 46 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_comap line 432 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasurableEmbedding, Filter.EventuallyEqSet, MeasureTheory.ae, Set.range, Set.univ, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.comap
Proof uses: id, Eq.mpr, tsum, Real.negMulLog, MeasureTheory.Measure.real, HSMul.hSMul, ENNReal, Inv.inv, Set, Singleton.singleton, SummationFilter.unconditional, ENNReal.toReal, congr, congrArg, congrFun', SummationFilter, optParam, funext, MeasureTheory.Measure.ennreal_smul_real_apply, Set.image and 34 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_comap_equiv line 451 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasurableEquiv, Eq, Real, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.measureEntropy_comap, MeasurableEquiv.measurableEmbedding, Eq.mpr, Filter.EventuallyEqSet, MeasureTheory.ae, Set.range, Set.univ, ENNReal, Set, Compl.compl, OfNat.ofNat, id, Equiv.range_eq_univ, MeasurableEquiv.toEquiv, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection and 3 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureEntropy_prod An ambitious goal would be to replace FiniteSupport with finite entropy line 459 source
Source documentation
An ambitious goal would be to replace FiniteSupport with finite entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, MeasureTheory.IsProbabilityMeasure, Eq, Real, ProbabilityTheory.measureEntropy, Prod, MeasureTheory.Measure.prod, HAdd.hAdd
Proof uses: Finset, MeasureTheory.Measure.support, ENNReal, Set, Compl.compl, OfNat.ofNat, ProbabilityTheory.measure_compl_support, SProd.sprod, Union.union, Set.univ, Set.ext, Iff, Membership.mem, Eq.mpr, Prod.mk, Not, Or, id, congr, congrArg and 66 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.
```
lemma measureEntropy_prod {μ : Measure S} {ν : Measure T} [FiniteSupport μ] [FiniteSupport ν]
    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] [MeasurableSingletonClass T] :
    Hm[μ.prod ν] = Hm[μ] + Hm[ν] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport
def ProbabilityTheory.measureMutualInfo line 498 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, autoParam, MeasureTheory.Measure, Prod, Real
Proof uses: HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod.fst, Prod.snd
7 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.measureMutualInfo_def line 504 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Prod, Eq, Real, ProbabilityTheory.measureMutualInfo, HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod.fst, Prod.snd
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.measureMutualInfo_zero_measure line 508 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Eq, Real, ProbabilityTheory.measureMutualInfo, OfNat.ofNat, MeasureTheory.Measure, Prod
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod.fst, Prod.snd, congr, MeasureTheory.Measure.map_zero, ProbabilityTheory.measureEntropy_zero, add_zero, sub_self, eq_self
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_of_not_isFiniteMeasure line 511 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Prod, Not, MeasureTheory.IsFiniteMeasure, Eq, Real, ProbabilityTheory.measureMutualInfo, OfNat.ofNat
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod.fst, Prod.snd, id, congrArg, ProbabilityTheory.measureMutualInfo_def, ENNReal, Set, Set.univ, Top.top, propext, MeasureTheory.not_isFiniteMeasure_iff, Eq.symm, Eq.mp, MeasureTheory.Measure.map_apply, measurable_fst and 10 more
20 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_univ_smul line 526 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Prod, Eq, Real, ProbabilityTheory.measureMutualInfo, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ
Proof uses: dite, MeasureTheory.IsFiniteMeasure, Classical.propDecidable, OfNat.ofNat, NeZero, Or, eq_zero_or_neZero, of_eq_true, Eq.trans, True, congr, congrArg, Top.top, congrFun', ENNReal.inv_zero, smul_zero, ProbabilityTheory.measureMutualInfo_zero_measure, eq_self, Eq.mpr, HSub.hSub and 32 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_swap line 545 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Prod, Eq, Real, ProbabilityTheory.measureMutualInfo, MeasureTheory.Measure.map, Prod.swap
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, Prod.fst, Prod.snd, id, congrArg, ProbabilityTheory.measureMutualInfo_def, add_comm, Function.comp, MeasureTheory.Measure.map_map, measurable_snd, measurable_swap, measurable_fst, HSub, Eq.rec, Eq.refl, tsum, Real.negMulLog and 43 more
34 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_prod line 561 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, MeasureTheory.IsProbabilityMeasure, Eq, Real, ProbabilityTheory.measureMutualInfo, MeasureTheory.Measure.prod, OfNat.ofNat
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, Prod, Prod.fst, Prod.snd, id, congrArg, ProbabilityTheory.measureMutualInfo_def, ProbabilityTheory.measureEntropy_prod, of_eq_true, Eq.trans, True, congrFun', congr, HSMul.hSMul, ENNReal, Set and 7 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_nonneg_aux An ambitious goal would be to replace FiniteSupport with finite entropy line 569 source
Source documentation
An ambitious goal would be to replace FiniteSupport with finite entropy. Proof is long and slow; needs to be optimized

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Prod, ProbabilityTheory.FiniteSupport, MeasureTheory.IsZeroOrProbabilityMeasure, And, LE.le, Real, OfNat.ofNat, ProbabilityTheory.measureMutualInfo, Iff, Eq, MeasureTheory.Measure.real, Singleton.singleton, Set, HMul.hMul, MeasureTheory.Measure.map, Prod.fst, Prod.snd
Proof uses: MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.measureMutualInfo_zero_measure, congrFun', eq_self, forall_congr, MeasureTheory.Measure.map_zero, MulZeroClass.mul_zero, implies_true, iff_self, and_self, Eq.symm, Finset, MeasureTheory.Measure.support and 193 more
220 instances, coercions and auxiliary constants left out.

Tactic trace: 210 steps (first 200 of 210)
Open to load the checked before-and-after goal states.
```
lemma measureMutualInfo_nonneg_aux {μ : Measure (S × U)} [FiniteSupport μ]
    [IsZeroOrProbabilityMeasure μ] :
    0 ≤ Im[μ] ∧
    (Im[μ] = 0 ↔ ∀ p, μ.real {p} = (μ.map Prod.fst).real {p.1} * (μ.map Prod.snd).real {p.2}) := by
…
```
Mentions: ProbabilityTheory.FiniteSupport
lemma ProbabilityTheory.measureMutualInfo_nonneg line 763 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Prod, ProbabilityTheory.FiniteSupport, LE.le, Real, OfNat.ofNat, ProbabilityTheory.measureMutualInfo
Proof uses: dite, MeasureTheory.IsFiniteMeasure, Classical.propDecidable, Eq.mpr, HSMul.hSMul, ENNReal, Inv.inv, Set, Set.univ, id, Eq, congrArg, Eq.symm, ProbabilityTheory.measureMutualInfo_univ_smul, And.left, Iff, MeasureTheory.Measure.real, Singleton.singleton, HMul.hMul, MeasureTheory.Measure.map and 6 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.measureMutualInfo_eq_zero_iff line 770 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, Prod, ProbabilityTheory.FiniteSupport, MeasureTheory.IsZeroOrProbabilityMeasure, Iff, Eq, Real, ProbabilityTheory.measureMutualInfo, OfNat.ofNat, MeasureTheory.Measure.real, Singleton.singleton, Set, HMul.hMul, MeasureTheory.Measure.map, Prod.fst, Prod.snd
Proof uses: And.right, LE.le, ProbabilityTheory.measureMutualInfo_nonneg_aux
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
example Mathlib.Meta.Positivity.(example at line 796) line 796 source