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

38 declarations, 0 contain sorry, 0 declared as axioms

Entropy of a kernel with respect to a measure

Main definitions

Kernel.entropy: entropy of a kernel κ with respect to a measure μ, μ[fun t ↦ measureEntropy (κ t)]. We use the notation Hk[κ, μ].

Main statements

chain_rule: Hk[κ, μ] = Hk[fst κ, μ] + Hk[condKernel κ, μ ⊗ₘ (fst κ)].
entropy_map_le: data-processing inequality for the kernel entropy

Notations

Hk[κ, μ] = Kernel.entropy κ μ

Imports (3)

Imported by 2 files

def ProbabilityTheory.Kernel.entropy line 38 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasureTheory.Measure, Real
Proof uses: MeasureTheory.integral, ProbabilityTheory.measureEntropy
7 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.entropy_zero_measure line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Eq, Real, ProbabilityTheory.Kernel.entropy, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.integral_zero_measure, ProbabilityTheory.measureEntropy, 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.Kernel.entropy_zero_kernel line 47 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, OfNat.ofNat, ProbabilityTheory.Kernel
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.integral, ProbabilityTheory.measureEntropy, funext, zero_apply, ProbabilityTheory.measureEntropy_zero, MeasureTheory.integral_zero, eq_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_congr line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.Kernel, Filter.EventuallyEq, MeasureTheory.ae, Eq, Real, ProbabilityTheory.Kernel.entropy
Proof uses: id, MeasureTheory.integral_congr_ae, ProbabilityTheory.measureEntropy, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, Eq.mpr, congrArg, Eq.refl
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_nonneg line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasureTheory.Measure, LE.le, Real, OfNat.ofNat, ProbabilityTheory.Kernel.entropy
Proof uses: MeasureTheory.integral_nonneg, ProbabilityTheory.measureEntropy, ProbabilityTheory.measureEntropy_nonneg
33 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.entropy_const line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.const, HMul.hMul, ENNReal.toReal, Set, ENNReal, Set.univ, ProbabilityTheory.measureEntropy
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, MeasureTheory.integral_const, eq_self
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.finiteKernelSupport_of_const Constant kernels with finite support, have finite kernel support line 64 source
Source documentation
Constant kernels with finite support, have finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.const
Proof uses: Exists.intro, Finset, Eq, ENNReal, Set, ProbabilityTheory.Kernel, Compl.compl, OfNat.ofNat, MeasureTheory.Measure.support, of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.measure_compl_support, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
lemma finiteKernelSupport_of_const (ν : Measure S) [FiniteSupport ν] :
    FiniteKernelSupport (Kernel.const T ν) := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.finiteSupport_of_compProd' Composing a finitely supported measure with a finitely supported kernel gives a finitely supported kernel line 72 source
Source documentation
Composing a finitely supported measure with a finitely supported kernel gives a finitely supported kernel.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, Prod, MeasureTheory.Measure.compProd
Proof uses: Finset, MeasureTheory.Measure.support, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, ProbabilityTheory.measure_compl_support, Membership.mem, Filter.Eventually, MeasureTheory.ae, Exists, ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport, ProbabilityTheory.FiniteSupport.mk, Exists.intro, autoParam, SProd.sprod, Eq.mpr, Prod.mk, id and 10 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
lemma finiteSupport_of_compProd' [MeasurableSingletonClass S] [MeasurableSingletonClass T]
    {μ : Measure T} [IsFiniteMeasure μ] {κ : Kernel T S}
    [IsZeroOrMarkovKernel κ] [FiniteSupport μ] (hκ : FiniteKernelSupport κ) :
    FiniteSupport (μ ⊗ₘ κ) := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.finiteSupport_of_compProd line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Prod, MeasureTheory.Measure.compProd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, id, Eq, congrArg, MeasureTheory.Measure.compProd_congr, ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk, ProbabilityTheory.Kernel.finiteSupport_of_compProd', ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.aefiniteKernelSupport_condDistrib line 93 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Nonempty, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Measurable, FiniteRange, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map
Proof uses: Filter.mp_mem, MeasureTheory.ae, Set.ofPred, Eq, ProbabilityTheory.Kernel, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Exists, Finset, ENNReal, Compl.compl, OfNat.ofNat, ProbabilityTheory.condDistrib_ae_eq, Filter.univ_mem', Membership.mem, id, Eq.mpr, congrArg and 1 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_le_log_card line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, Fintype, MeasureTheory.IsProbabilityMeasure, LE.le, Real, ProbabilityTheory.Kernel.entropy, Real.log, Fintype.card
Proof uses: LE.le.trans, MeasureTheory.integral, ProbabilityTheory.measureEntropy, MeasureTheory.integral_mono_of_nonneg, MeasureTheory.ae_of_all, OfNat.ofNat, ProbabilityTheory.measureEntropy_nonneg, MeasureTheory.integrable_const, ProbabilityTheory.measureEntropy_le_log_card, of_eq_true, Eq.trans, True, congrFun', congrArg, HSMul.hSMul, MeasureTheory.Measure.real, Set.univ, MeasureTheory.integral_const, MeasureTheory.probReal_univ, one_mul
65 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_eq_integral_sum line 112 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, MeasureTheory.integral, tsum, Real.negMulLog, MeasureTheory.Measure.real, Singleton.singleton, Set, SummationFilter.unconditional
Proof uses: id, of_eq_true, ProbabilityTheory.measureEntropy, Eq.trans, True, congrFun', congrArg, funext, ProbabilityTheory.measureEntropy_of_isProbabilityMeasure, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_snd_compProd_deterministic_of_injective entropy_map_of_injective is a special case of this (see def of map) line 117 source
Source comment
entropy_map_of_injective is a special case of this (see def of map)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, Prod, Function.Injective, Prod.mk, Measurable, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.deterministic
Proof uses: ProbabilityTheory.Kernel.map, MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, Set.preimage, Prod.snd, id, congrArg, ProbabilityTheory.Kernel.snd_apply', Set.ofPred, Membership.mem, ProbabilityTheory.Kernel.compProd_deterministic_apply, measurable_snd, ProbabilityTheory.Kernel.map_apply', Measurable.fun_comp, Measurable.prodMk, measurable_const, measurable_id' and 18 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_snd_compProd_deterministic_of_injective [MeasurableSingletonClass U]
    (κ : Kernel T S) [IsMarkovKernel κ]
    (μ : Measure T) {f : T × S → U}
    (hf : ∀ t, Function.Injective (fun x ↦ f (t, x))) (hmes : Measurable f) :
    Hk[snd (κ ⊗ₖ deterministic f hmes), μ] = Hk[κ, μ] := by
…
```
lemma ProbabilityTheory.Kernel.entropy_map_of_injective line 135 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, Function.Injective, Measurable, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map
Proof uses: id, Eq.mpr, MeasureTheory.integral, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.map, congrFun', congrArg, funext, ProbabilityTheory.Kernel.map_apply, of_eq_true, Eq.trans, True, ProbabilityTheory.measureEntropy_map_of_injective, eq_self
7 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_map_swap line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map, Prod.swap
Proof uses: ProbabilityTheory.Kernel.entropy_map_of_injective, Prod.swap_injective, measurable_swap
3 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.entropy_swapRight line 145 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.swapRight
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.swap, id, congrArg, ProbabilityTheory.Kernel.swapRight_eq, ProbabilityTheory.Kernel.entropy_map_swap, Eq.refl
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_comap line 150 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, MeasurableEmbedding, Filter.EventuallyEqSet, MeasureTheory.ae, Set.range, Set.univ, MeasureTheory.IsFiniteMeasure, MeasureTheory.Measure.comap, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.comap, MeasurableEmbedding.measurable
Proof uses: Exists, Finset, Filter.Eventually, Membership.mem, autoParam, Finset.image, Classical.propDecidable, id, Eq.mpr, ENNReal, Set, Compl.compl, OfNat.ofNat, And, Set.image, Eq.trans, Union.union, congrFun', congrArg, Finset.coe_image and 31 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteSupport.comap_equiv line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasurableEquiv, ProbabilityTheory.FiniteSupport, MeasureTheory.Measure.comap
Proof uses: Finset, MeasureTheory.Measure.support, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, ProbabilityTheory.measure_compl_support, ProbabilityTheory.FiniteSupport.mk, Exists.intro, Filter.Eventually, Membership.mem, MeasureTheory.ae, autoParam, Finset.image, Classical.propDecidable, MeasurableEquiv.symm, id, Eq.mpr, Set.image and 15 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_comap_equiv line 190 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, MeasurableEquiv, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.comap, MeasurableEquiv.measurable, MeasureTheory.Measure.comap
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, ProbabilityTheory.Kernel.entropy_comap, MeasurableEquiv.measurableEmbedding, Filter.EventuallyEqSet, MeasureTheory.ae, Set.range, Set.univ, ENNReal, Set, Compl.compl, OfNat.ofNat, EquivLike.range_eq_univ, EmptyCollection.emptyCollection, Set.compl_univ, MeasureTheory.measure_empty, eq_self 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 ProbabilityTheory.Kernel.entropy_comap_swap line 197 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.comap, Prod.swap, measurable_swap, MeasureTheory.Measure.comap
Proof uses: ProbabilityTheory.Kernel.entropy_comap_equiv, MeasurableEquiv.prodComm
3 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.entropy_prodMkLeft_unit line 203 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, Prod, Unit, ProbabilityTheory.Kernel.prodMkLeft, MeasureTheory.Measure.map, Prod.mk, Unit.unit
Proof uses: Eq.mpr, PUnit, ProbabilityTheory.Kernel.comap, MeasurableEquiv, MeasurableEquiv.punitProd, MeasurableEquiv.measurable, MeasureTheory.Measure.comap, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, heq_of_eq, MeasurableEquiv.symm, id, congrArg, MeasurableEquiv.map_symm, Eq.rec, PUnit.unit, ProbabilityTheory.Kernel.entropy_comap_equiv
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_compProd_aux line 211 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.compProd, HAdd.hAdd, MeasureTheory.integral, ProbabilityTheory.Kernel.comap, Prod.mk, measurable_prodMk_left
Proof uses: OfNat.ofNat, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', ProbabilityTheory.Kernel.compProd_zero_left, ProbabilityTheory.Kernel.entropy_zero_kernel, funext, zero_apply, ProbabilityTheory.Kernel.entropy_zero_measure, MeasureTheory.integral_zero, add_zero, eq_self, Eq.symm, Finset, MeasureTheory.Measure.support and 120 more
140 instances, coercions and auxiliary constants left out.

Tactic trace: 50 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_compProd' line 268 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.compProd, HAdd.hAdd, MeasureTheory.Measure.compProd
Proof uses: Eq.mpr, MeasureTheory.integral, ProbabilityTheory.Kernel.comap, Prod.mk, measurable_prodMk_left, id, congrArg, ProbabilityTheory.Kernel.entropy_compProd_aux, HAdd, Eq.rec, Eq.refl, ProbabilityTheory.measureEntropy, ProbabilityTheory.Kernel.entropy.eq_1, MeasureTheory.Measure.integral_compProd, ProbabilityTheory.Kernel.finiteSupport_of_compProd', ProbabilityTheory.integrable_of_finiteSupport, NormedAddCommGroup, NormedSpace
19 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_compProd line 282 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.Measure.compProd, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.compProd, HAdd.hAdd
Proof uses: ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, MeasureTheory.Measure.compProd_congr, Filter.EventuallyEq.symm, MeasureTheory.ae, ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk, ProbabilityTheory.Kernel.entropy_congr, ProbabilityTheory.Kernel.compProd_congr_ae, Eq.mpr, Filter.EventuallyEq, eq_of_heq, Filter, HEq, Eq.refl, HEq.refl, Eq.symm, FunLike, Set, ENNReal, MeasureTheory.OuterMeasureClass, id and 3 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_deterministic line 299 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.deterministic, Measurable.of_discrete, OfNat.ofNat
Proof uses: id, Eq.mpr, MeasureTheory.integral, ProbabilityTheory.measureEntropy, ProbabilityTheory.Kernel, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, NormedAddCommGroup, NormedSpace, heq_of_eq, funext, ProbabilityTheory.measureEntropy_dirac, MeasureTheory.integral_zero
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_compProd_deterministic line 307 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Prod, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.deterministic, Measurable.of_discrete
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HAdd.hAdd, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.entropy_compProd, ProbabilityTheory.Kernel.FiniteKernelSupport.aefiniteKernelSupport, ProbabilityTheory.Kernel.FiniteKernelSupport.deterministic, OfNat.ofNat, ProbabilityTheory.Kernel.entropy_deterministic, add_zero, eq_self
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.nonempty_of_isMarkovKernel line 314 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, Nonempty
Proof uses: MeasureTheory.Measure.nonempty_of_neZero, MeasureTheory.Measure, Classical.arbitrary
4 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel line 318 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, Nonempty
Proof uses: MeasureTheory.Measure.nonempty_of_neZero, ProbabilityTheory.Kernel.nonempty_of_isMarkovKernel
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.chain_rule line 324 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, Nonempty, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, HAdd.hAdd, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.snd, MeasureTheory.Measure.compProd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.compProd, id, Eq.rec, Eq.refl, Eq.trans, congrArg, ProbabilityTheory.Kernel.disintegration, ProbabilityTheory.Kernel.entropy_compProd, ProbabilityTheory.Kernel.AEFiniteKernelSupport.fst, ProbabilityTheory.Kernel.aefiniteKernelSupport_of_cond
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.chain_rule' line 333 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Nonempty, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, HAdd.hAdd, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.swapRight, MeasureTheory.Measure.compProd
Proof uses: Eq.mpr, id, congrArg, Eq.symm, ProbabilityTheory.Kernel.entropy_swapRight, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.chain_rule, ProbabilityTheory.Kernel.AEFiniteKernelSupport.swapRight, of_eq_true, Eq.trans, True, congrFun', congr, ProbabilityTheory.Kernel.fst_swapRight, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_prodMkRight line 343 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, Prod, ProbabilityTheory.Kernel.prodMkRight, MeasureTheory.Measure.compProd
Proof uses: ProbabilityTheory.Kernel.finiteSupport_of_compProd, of_eq_true, MeasureTheory.integral, ProbabilityTheory.measureEntropy, Eq.trans, True, congrFun', congrArg, Prod.fst, Prod.mk, MeasureTheory.Measure.integral_compProd, MeasureTheory.Integrable, funext, HSMul.hSMul, MeasureTheory.Measure.real, Set.univ, MeasureTheory.integral_const, OfNat.ofNat, MeasureTheory.probReal_univ, one_mul and 1 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_prodMkRight' line 352 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, Prod, ProbabilityTheory.Kernel.prodMkRight, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.const, id, congrArg, Eq.symm, ProbabilityTheory.Kernel.entropy_prodMkRight, ProbabilityTheory.Kernel.FiniteKernelSupport.aefiniteKernelSupport, ProbabilityTheory.Kernel.finiteKernelSupport_of_const, Eq.rec, Eq.refl, MeasureTheory.Measure.ext, Set, MeasurableSet, ENNReal, MeasureTheory.lintegral, Set.preimage, Prod.mk, congrFun', MeasureTheory.SFinite and 5 more
8 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_prodMkLeft line 364 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, Prod, ProbabilityTheory.Kernel.prodMkLeft, MeasureTheory.Measure.prod
Proof uses: id, MeasureTheory.integral, ProbabilityTheory.measureEntropy, Eq.mpr, Prod.snd, Prod.mk, congrArg, MeasureTheory.integral_prod, ProbabilityTheory.integrable_of_finiteSupport, of_eq_true, Eq.trans, True, congrFun', HSMul.hSMul, MeasureTheory.Measure.real, Set.univ, MeasureTheory.integral_const, OfNat.ofNat, MeasureTheory.probReal_univ, one_mul and 1 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_prod line 378 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.entropy, Prod, ProbabilityTheory.Kernel.prod, HAdd.hAdd
Proof uses: OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.Kernel.entropy_zero_measure, add_zero, eq_self, Eq.symm, Nonempty, ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel, Eq.mpr, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.snd, MeasureTheory.Measure.compProd and 9 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_map_le Data-processing inequality for the kernel entropy line 389 source
Source documentation
Data-processing inequality for the kernel entropy.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.map
Proof uses: Eq, OfNat.ofNat, ProbabilityTheory.IsMarkovKernel, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', ProbabilityTheory.Kernel.map_zero, ProbabilityTheory.Kernel.entropy_zero_kernel, Eq.symm, MeasureTheory.IsProbabilityMeasure, MeasureTheory.eq_zero_or_isProbabilityMeasure, ProbabilityTheory.Kernel.entropy_zero_measure, Nonempty, ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel, Prod and 20 more
42 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_map_le
    {κ : Kernel T S} [IsZeroOrMarkovKernel κ] {μ : Measure T} [IsZeroOrProbabilityMeasure μ]
    (f : S → U) [FiniteSupport μ] (hκ : AEFiniteKernelSupport κ μ) :
    Hk[map κ f, μ] ≤ Hk[κ, μ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport
lemma ProbabilityTheory.Kernel.entropy_of_map_eq_of_map line 407 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Eq, ProbabilityTheory.Kernel.map, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Real, ProbabilityTheory.Kernel.entropy
Proof uses: le_antisymm, Eq.mpr, LE.le, id, congrArg, ProbabilityTheory.Kernel.entropy_map_le
3 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_snd_le line 417 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.snd, id, Eq, congrArg, ProbabilityTheory.Kernel.snd_eq, ProbabilityTheory.Kernel.entropy_map_le
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.entropy_fst_le line 424 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.fst, id, Eq, congrArg, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.entropy_map_le
6 instances, coercions and auxiliary constants left out.

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