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

26 declarations, 0 contain sorry, 0 declared as axioms

Mutual Information of kernels

Main definitions

mutualInfo: Mutual information of a kernel κ into a product space with respect to a measure μ. This is denoted by Ik[κ, μ] and is equal to Hk[fst κ, μ] + Hk[snd κ, μ] - Hk[κ, μ].

Main statements

mutualInfo_nonneg: Ik[κ, μ] is nonnegative
entropy_condKernel_le_entropy_fst and entropy_condKernel_le_entropy_snd: conditioning reduces entropy.

Notations

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

Imports (2)

Imported by 3 files

def ProbabilityTheory.Kernel.mutualInfo line 40 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Real
Proof uses: HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.mutualInfo_def line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd
Proof uses: rfl
6 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.mutualInfo_zero_measure line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, OfNat.ofNat, MeasureTheory.Measure
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, congr, ProbabilityTheory.Kernel.entropy_zero_measure, 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.Kernel.mutualInfo_zero_kernel line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, OfNat.ofNat, ProbabilityTheory.Kernel, Prod
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, congr, ProbabilityTheory.Kernel.fst_zero, ProbabilityTheory.Kernel.entropy_zero_kernel, ProbabilityTheory.Kernel.snd_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.Kernel.mutualInfo_congr line 57 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Filter.EventuallyEq, MeasureTheory.ae, Eq, Real, ProbabilityTheory.Kernel.mutualInfo
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, id, congrArg, ProbabilityTheory.Kernel.mutualInfo.eq_1, Filter.mp_mem, Set.ofPred, Filter.univ_mem', Membership.mem, Set, MeasureTheory.Measure.map, Prod.fst, ProbabilityTheory.Kernel.fst_apply, Eq.refl, Prod.snd, ProbabilityTheory.Kernel.snd_apply and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.compProd_assoc' line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Prod, Eq, ProbabilityTheory.Kernel.map, ProbabilityTheory.Kernel.compProd, MeasurableEquiv, MeasurableEquiv.prodAssoc, ProbabilityTheory.Kernel.comap, MeasurableEquiv.measurable
Proof uses: ProbabilityTheory.Kernel.ext, MeasureTheory.Measure.ext, MeasureTheory.Measure, Set, MeasurableSet, Eq.mpr, ENNReal, Set.preimage, id, congrArg, ProbabilityTheory.Kernel.map_apply', MeasureTheory.lintegral, Prod.mk, ProbabilityTheory.Kernel.compProd_apply, ProbabilityTheory.Kernel.lintegral_compProd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', Eq.rec, Eq.refl, funext, measurable_prodMk_left
12 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.Measure.compProd_compProd line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Prod, Eq, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd, MeasureTheory.Measure.map, MeasurableEquiv, MeasurableEquiv.prodAssoc
Proof uses: dite, MeasureTheory.SFinite, Classical.propDecidable, MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, MeasureTheory.lintegral, Set.preimage, Prod.mk, id, congrArg, MeasureTheory.Measure.compProd_apply, MeasureTheory.Measure.map_apply, MeasurableEquiv.measurable, MeasureTheory.Measure.lintegral_compProd, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left, Eq.rec, Eq.refl and 14 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.Measure.compProd_compProd' line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Prod, Eq, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd, MeasureTheory.Measure.comap, MeasurableEquiv, MeasurableEquiv.symm, MeasurableEquiv.prodAssoc
Proof uses: Eq.mpr, MeasureTheory.Measure.map, id, congrArg, MeasurableEquiv.comap_symm, ProbabilityTheory.Kernel.Measure.compProd_compProd, 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 ProbabilityTheory.Kernel.Measure.compProd_compProd'' line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Prod, Eq, MeasureTheory.Measure.compProd, MeasureTheory.Measure.comap, MeasurableEquiv, MeasurableEquiv.prodAssoc, ProbabilityTheory.Kernel.compProd
Proof uses: Eq.mpr, MeasureTheory.Measure.map, id, congrArg, ProbabilityTheory.Kernel.Measure.compProd_compProd, MeasurableEquiv.symm, Eq.symm, MeasurableEquiv.map_symm, Function.comp, MeasureTheory.Measure.map_map, MeasurableEquiv.measurable, of_eq_true, Eq.trans, True, congrFun', MeasurableEquiv.symm_comp_self, MeasureTheory.Measure.map_id, eq_self
8 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_swapRight line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.swapRight
Proof uses: Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, id, congrArg, ProbabilityTheory.Kernel.mutualInfo.eq_1, ProbabilityTheory.Kernel.fst_swapRight, ProbabilityTheory.Kernel.snd_swapRight, ProbabilityTheory.Kernel.entropy_swapRight, add_comm, Eq.refl
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_nonneg' line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, LE.le, Real, OfNat.ofNat, ProbabilityTheory.Kernel.mutualInfo
Proof uses: id, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd, Eq.mpr, MeasureTheory.integral, ProbabilityTheory.measureEntropy, MeasureTheory.Measure.restrict, Finset, MeasureTheory.Measure.support, Eq, congrArg, congr, NormedAddCommGroup, NormedSpace, MeasureTheory.integral_eq_setIntegral, ProbabilityTheory.ae_mem_support, Finset.sum and 24 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_nonneg line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, OfNat.ofNat, ProbabilityTheory.Kernel.mutualInfo
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, id, Eq, congrArg, ProbabilityTheory.Kernel.mutualInfo_congr, ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk, ProbabilityTheory.Kernel.mutualInfo_nonneg', ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_compProd line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.Measure.compProd, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.compProd, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.fst, id, congrArg, ProbabilityTheory.Kernel.mutualInfo.eq_1, ProbabilityTheory.Kernel.entropy_compProd, ProbabilityTheory.Kernel.fst_compProd, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_eq_fst_sub line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.swapRight, ProbabilityTheory.Kernel.snd and 1 more
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, ProbabilityTheory.Kernel.mutualInfo.eq_1, ProbabilityTheory.Kernel.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
49 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_prod line 159 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.prod, OfNat.ofNat
Proof uses: ProbabilityTheory.IsMarkovKernel, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, of_eq_true, Eq.trans, True, congrFun', congrArg, Prod, ProbabilityTheory.Kernel.zero_prod, ProbabilityTheory.Kernel.mutualInfo_zero_kernel, eq_self, Eq.symm, ProbabilityTheory.Kernel.prod_zero, Eq.mpr, HSub.hSub, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.snd and 7 more
21 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.mutualInfo_eq_snd_sub line 170 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, Real, ProbabilityTheory.Kernel.mutualInfo, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.condKernel, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, HAdd.hAdd, id, congrArg, ProbabilityTheory.Kernel.mutualInfo.eq_1, ProbabilityTheory.Kernel.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
47 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_condKernel_le_entropy_fst line 178 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.swapRight, ProbabilityTheory.Kernel.snd, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, OfNat.ofNat, HSub.hSub, id, Eq, congrArg, Eq.symm, propext, sub_nonneg, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.mutualInfo_eq_fst_sub, ProbabilityTheory.Kernel.mutualInfo_nonneg
35 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_condKernel_le_entropy_snd line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.snd, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, OfNat.ofNat, HSub.hSub, id, Eq, congrArg, Eq.symm, propext, sub_nonneg, ProbabilityTheory.Kernel.mutualInfo, ProbabilityTheory.Kernel.mutualInfo_eq_snd_sub, ProbabilityTheory.Kernel.mutualInfo_nonneg
33 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_snd_sub_mutualInfo_le_entropy_map_of_injective TODO: extract lemma(s) from this: line 195 source
Source comment
TODO: extract lemma(s) from this:

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsZeroOrMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, Function.Injective, Prod.mk, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, LE.le, Real, HSub.hSub, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.mutualInfo, 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.snd_zero, ProbabilityTheory.Kernel.entropy_zero_kernel, ProbabilityTheory.Kernel.mutualInfo_zero_kernel, sub_self, ProbabilityTheory.Kernel.map_zero, Eq.symm, MeasureTheory.IsProbabilityMeasure, MeasureTheory.eq_zero_or_isProbabilityMeasure, ProbabilityTheory.Kernel.entropy_zero_measure and 75 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_snd_sub_mutualInfo_le_entropy_map_of_injective {V : Type*} [Countable V]
    [MeasurableSpace V] [MeasurableSingletonClass V]
    (κ : Kernel T (S × U)) [IsZeroOrMarkovKernel κ] (μ : Measure T) [IsZeroOrProbabilityMeasure μ]
    (f : S × U → V) (hfi : ∀ x, Injective (fun y ↦ f (x, y))) [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) :
    Hk[snd κ, μ] - Ik[κ, μ] ≤ Hk[map κ f, μ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport
lemma ProbabilityTheory.Kernel.entropy_reverse line 237 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, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.reverse
Proof uses: le_antisymm, Eq.mpr, LE.le, ProbabilityTheory.Kernel.map, Prod.mk, Prod.snd, Prod.fst, id, congrFun', congrArg, ProbabilityTheory.Kernel.reverse_eq, ProbabilityTheory.Kernel.entropy_map_le, Eq.rec, Eq.refl, Eq.trans, Eq.symm, ProbabilityTheory.Kernel.reverse_reverse, congr, Eq.mp, ProbabilityTheory.Kernel.AEFiniteKernelSupport.reverse
9 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.Kernel.IsZeroOrProbabilityMeasure.compProd line 246 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, MeasureTheory.Measure.compProd
Proof uses: Eq, OfNat.ofNat, ProbabilityTheory.IsMarkovKernel, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, Eq.mpr, id, congrArg, MeasureTheory.Measure.compProd_zero_right, inferInstance, Eq.symm, MeasureTheory.IsProbabilityMeasure, MeasureTheory.eq_zero_or_isProbabilityMeasure, MeasureTheory.Measure.compProd_zero_left
9 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_condKernel_compProd_triple line 256 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Nonempty, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, Eq, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.compProd, MeasureTheory.Measure.compProd
Proof uses: ProbabilityTheory.Kernel.entropy_congr, ProbabilityTheory.Kernel.condKernel_compProd_ae_eq
20 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.entropy_submodular_compProd from kernel (T × S × U) V ; Measure (T × S × U) to kernel (T × S) V ; Measure (T × S) line 264 source
Source comment
from kernel (T × S × U) V ; Measure (T × S × U) to kernel (T × S) V ; Measure (T × S)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd, LE.le, Real, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.comap, MeasurableEquiv, MeasurableEquiv.prodAssoc and 1 more
Proof uses: Eq, OfNat.ofNat, MeasureTheory.IsProbabilityMeasure, Or, MeasureTheory.eq_zero_or_isProbabilityMeasure, of_eq_true, Eq.trans, True, congr, congrArg, MeasureTheory.Measure.compProd_zero_left, ProbabilityTheory.Kernel.entropy_zero_measure, Eq.symm, ProbabilityTheory.eq_zero_or_isMarkovKernel, ProbabilityTheory.Kernel.compProd_zero_left, MeasureTheory.Measure.compProd_zero_right, Nonempty, ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel, MeasureTheory.Measure.nonempty_of_neZero, ProbabilityTheory.Kernel.compProd_zero_right and 26 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_submodular_compProd {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ]
    {κ : Kernel (T × S) U} [IsZeroOrMarkovKernel κ] {η : Kernel (T × S × U) V} [IsMarkovKernel η]
    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ (μ ⊗ₘ ξ))
    (hη : AEFiniteKernelSupport η (μ ⊗ₘ (ξ ⊗ₖ κ))) (hξ : AEFiniteKernelSupport ξ μ) :
    Hk[η, μ ⊗ₘ (ξ ⊗ₖ κ)]
      ≤ Hk[snd (κ ⊗ₖ (comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable)),
            μ ⊗ₘ ξ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport
lemma ProbabilityTheory.Kernel.entropy_compProd_triple_add_entropy_le $$ H[X,Y,Z] + H[X] \leq H[Z,X] + H[Y,X].$$ line 299 source
Source comment
$$ H[X,Y,Z] + H[X] \leq H[Z,X] + H[Y,X].$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, MeasureTheory.IsZeroOrProbabilityMeasure, ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd, LE.le, Real, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.comap, MeasurableEquiv and 2 more
Proof uses: Eq, 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.symm, ProbabilityTheory.eq_zero_or_isMarkovKernel, congrFun', ProbabilityTheory.Kernel.compProd_zero_left, ProbabilityTheory.Kernel.entropy_zero_kernel, Nonempty, ProbabilityTheory.Kernel.nonempty_of_isProbabilityMeasure_of_isMarkovKernel, MeasureTheory.Measure.nonempty_of_neZero and 26 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_compProd_triple_add_entropy_le {ξ : Kernel T S} [IsZeroOrMarkovKernel ξ]
    {κ : Kernel (T × S) U} [IsMarkovKernel κ]
    {η : Kernel (T × S × U) V} [IsMarkovKernel η]
    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ (μ ⊗ₘ ξ))
    (hη : AEFiniteKernelSupport η (μ ⊗ₘ (ξ ⊗ₖ κ))) (hξ : AEFiniteKernelSupport ξ μ) :
    Hk[(ξ ⊗ₖ κ) ⊗ₖ η, μ] + Hk[ξ, μ]
      ≤ Hk[ξ ⊗ₖ snd (κ ⊗ₖ comap η MeasurableEquiv.prodAssoc MeasurableEquiv.prodAssoc.measurable),
          μ] + Hk[ξ ⊗ₖ κ, μ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport
lemma ProbabilityTheory.Kernel.entropy_triple_add_entropy_le' The submodularity inequality: $$ H[X,Y,Z] + H[X] \leq H[X,Z] + H[X,Y].$$ line 338 source
Source documentation
The submodularity inequality: $$ H[X,Y,Z] + H[X] \leq H[X,Z] + H[X,Y].$$

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, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.deleteMiddle, ProbabilityTheory.Kernel.deleteRight
Proof uses: Eq, OfNat.ofNat, ProbabilityTheory.IsMarkovKernel, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, of_eq_true, Eq.trans, True, congr, congrArg, ProbabilityTheory.Kernel.entropy_zero_kernel, congrFun', ProbabilityTheory.Kernel.fst_zero, add_zero, ProbabilityTheory.Kernel.deleteMiddle_zero, ProbabilityTheory.Kernel.deleteRight_zero, Eq.symm, MeasureTheory.IsProbabilityMeasure, MeasureTheory.eq_zero_or_isProbabilityMeasure, ProbabilityTheory.Kernel.entropy_zero_measure and 57 more
46 instances, coercions and auxiliary constants left out.

Tactic trace: 55 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_triple_add_entropy_le' {κ : Kernel T (S × U × V)} [IsZeroOrMarkovKernel κ]
    {μ : Measure T} [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) :
    Hk[κ, μ] + Hk[fst κ, μ] ≤ Hk[deleteMiddle κ, μ] + Hk[deleteRight κ, μ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.deleteMiddle, ProbabilityTheory.Kernel.deleteRight
lemma ProbabilityTheory.Kernel.entropy_triple_add_entropy_le The submodularity inequality: $$ H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$$ line 390 source
Source documentation
The submodularity inequality: $$ H[X,Y,Z] + H[Z] \leq H[X,Z] + H[Y,Z].$$

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, HAdd.hAdd, ProbabilityTheory.Kernel.entropy, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.deleteMiddle
Proof uses: Eq, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.reverse, Eq.mpr, ProbabilityTheory.Kernel.map, Prod.fst, id, congrArg, ProbabilityTheory.Kernel.fst_eq, Prod.mk, Prod.snd, ProbabilityTheory.Kernel.reverse_eq, ProbabilityTheory.Kernel.snd_eq, Function.comp, ProbabilityTheory.Kernel.map_map, Measurable.prodMk, Measurable.snd, measurable_id', Measurable.fst, Eq.rec and 16 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
lemma entropy_triple_add_entropy_le (κ : Kernel T (S × U × V)) [IsZeroOrMarkovKernel κ]
    (μ : Measure T) [IsZeroOrProbabilityMeasure μ] [FiniteSupport μ]
    (hκ : AEFiniteKernelSupport κ μ) :
    Hk[κ, μ] + Hk[snd (snd κ), μ] ≤ Hk[deleteMiddle κ, μ] + Hk[snd κ, μ] := by
…
```
Mentions: ProbabilityTheory.FiniteSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.deleteMiddle