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

64 declarations, 0 contain sorry, 0 declared as axioms

Disintegration of kernels in finite spaces

We can write κ : Kernel S (T × U) as a composition-product (fst κ) ⊗ₖ (condKernel κ) where fst κ : Kernel S T and condKernel : Kernel (S × T) U is defined in this file.

Imports (5)

Imported by 3 files

lemma ProbabilityTheory.Kernel.condKernel_apply line 43 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsFiniteKernel, Ne, ENNReal, MeasureTheory.Measure, Set, Prod.fst, Set.preimage, Singleton.singleton, Prod.snd, OfNat.ofNat, Eq, ProbabilityTheory.Kernel.condKernel, MeasureTheory.Measure.condKernel
Proof uses: Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.Kernel.fst, Prod.mk, ProbabilityTheory.Kernel.condKernel_apply_eq_condKernel, Eq.mp, Filter.Eventually, congrArg, propext, MeasureTheory.ae_iff_of_countable, Filter.EventuallyEq.eq_1, Eq.mpr, Set.ofPred, Membership.mem, id, ProbabilityTheory.Kernel.fst_apply', MeasurableSet.singleton
26 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.condKernel_apply' line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsFiniteKernel, Ne, ENNReal, MeasureTheory.Measure, Set, Prod.fst, Set.preimage, Singleton.singleton, Prod.snd, OfNat.ofNat, Eq, ProbabilityTheory.Kernel.condKernel, HMul.hMul, Inv.inv and 1 more
Proof uses: Eq.mpr, MeasureTheory.Measure.condKernel, id, congrArg, ProbabilityTheory.Kernel.condKernel_apply, MeasureTheory.Measure.fst, MeasureTheory.Measure.condKernel_apply_of_ne_zero, MeasureTheory.Measure.fst_apply, MeasurableSet.singleton, Eq.refl
37 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.condKernel_compProd_apply' line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, ProbabilityTheory.Kernel, ProbabilityTheory.IsFiniteKernel, Prod, ProbabilityTheory.IsMarkovKernel, Ne, ENNReal, MeasureTheory.Measure, Set, Prod.fst, Singleton.singleton, Prod.snd, OfNat.ofNat, MeasurableSet, Eq, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.compProd
Proof uses: Set.preimage, Eq.mpr, id, congrArg, ProbabilityTheory.Kernel.compProd_preimage_fst, MeasurableSet.singleton, HMul.hMul, Inv.inv, SProd.sprod, ProbabilityTheory.Kernel.condKernel_apply', MeasureTheory.lintegral, Prod.mk, ProbabilityTheory.Kernel.compProd_apply, MeasurableSet.prod, MeasurableSingletonClass.measurableSet_singleton, Not, measurableSet_preimage, Measurable.fst, measurable_id', MeasurableSet.of_discrete and 29 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.condKernel_compProd_apply line 75 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, ProbabilityTheory.Kernel, ProbabilityTheory.IsFiniteKernel, Prod, ProbabilityTheory.IsMarkovKernel, Ne, ENNReal, MeasureTheory.Measure, Set, Prod.fst, Singleton.singleton, Prod.snd, OfNat.ofNat, Eq, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.compProd
Proof uses: MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, Eq.refl, ProbabilityTheory.Kernel.condKernel_compProd_apply'
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.disintegration line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsFiniteKernel, Eq, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.condKernel
Proof uses: ProbabilityTheory.Kernel.ext, MeasureTheory.Measure.ext, MeasureTheory.Measure, Set, MeasurableSet, Eq.mpr, ENNReal, MeasureTheory.lintegral, Prod.mk, Set.preimage, id, congrArg, ProbabilityTheory.Kernel.compProd_apply, Prod.fst, ProbabilityTheory.Kernel.lintegral_fst, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', tsum, HMul.hMul, Singleton.singleton, SummationFilter.unconditional and 59 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 33 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.condKernel_compProd_ae_eq line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsFiniteKernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.compProd
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, ProbabilityTheory.Kernel.condKernel_compProd_apply, Not, Or, Set.preimage, Prod.mk, Exists, Prod.fst and 39 more
60 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.compProd_swapLeft_prodMkLeft line 134 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Eq, Prod, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.swapLeft, ProbabilityTheory.Kernel.prodMkLeft, ProbabilityTheory.Kernel.prod
Proof uses: ProbabilityTheory.Kernel.ext, MeasureTheory.Measure.ext, MeasureTheory.Measure, Set, MeasurableSet, of_eq_true, ENNReal, Eq.trans, MeasureTheory.lintegral, Set.preimage, Prod.mk, True, congr, congrArg, ProbabilityTheory.Kernel.compProd_apply, ProbabilityTheory.Kernel.prodMkRight, ProbabilityTheory.Kernel.prod_apply', eq_self
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.condKernel_prod_ae_eq line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.IsFiniteKernel, MeasureTheory.Measure, ProbabilityTheory.IsMarkovKernel, Filter.EventuallyEq, Prod, MeasureTheory.ae, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.prod, ProbabilityTheory.Kernel.prodMkRight
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.swapLeft, ProbabilityTheory.Kernel.prodMkLeft, id, Eq, congrFun', congrArg, ProbabilityTheory.Kernel.condKernel.congr_simp, ProbabilityTheory.Kernel.condKernel_compProd_ae_eq
27 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.ae_eq_condKernel_of_compProd_eq line 147 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsFiniteKernel, MeasureTheory.Measure, ProbabilityTheory.IsMarkovKernel, Eq, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.fst, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.condKernel
Proof uses: StandardBorelSpace, MeasurableSpace.CountableOrCountablyGenerated, Eq.rec, Eq.refl, Eq.symm, Eq.mpr, id, congrArg, Filter.EventuallyEq.symm, ProbabilityTheory.Kernel.condKernel_compProd_ae_eq
21 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.condKernel_map_prodMk_left line 154 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Countable, MeasurableSpace, DiscreteMeasurableSpace, Nonempty, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.fst, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.map, Prod.mk, Prod.fst, ProbabilityTheory.Kernel.snd, ProbabilityTheory.Kernel.compProd, ProbabilityTheory.Kernel.deterministic and 2 more
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, And, Not, Set.ofPred, Exists, Eq.mp, tsum, HMul.hMul and 67 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 44 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_apply' line 215 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Ne, ENNReal, Set, Set.preimage, Singleton.singleton, OfNat.ofNat, MeasurableSet, Eq, ProbabilityTheory.Kernel, ProbabilityTheory.condDistrib, HMul.hMul, Inv.inv and 1 more
Proof uses: Eq.mpr, MeasureTheory.Measure.map, Prod, Prod.mk, SProd.sprod, id, congrArg, ProbabilityTheory.condDistrib_apply_of_ne_zero, MeasureTheory.Measure.map_apply, MeasurableSet.singleton, Measurable.prodMk, MeasurableSet.prod, MeasurableSingletonClass.measurableSet_singleton, HMul, Eq.rec, Eq.refl, DFunLike
30 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_apply line 224 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Ne, ENNReal, Set, Set.preimage, Singleton.singleton, OfNat.ofNat, Eq, ProbabilityTheory.Kernel, ProbabilityTheory.condDistrib, MeasureTheory.Measure.map, ProbabilityTheory.cond
Proof uses: MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, HMul.hMul, Inv.inv, Inter.inter, id, congrArg, ProbabilityTheory.condDistrib_apply', MeasureTheory.Measure.map_apply, ProbabilityTheory.cond_apply, MeasurableSet.singleton, Eq.refl
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_ae_eq line 234 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.map, ProbabilityTheory.Kernel, ProbabilityTheory.condDistrib, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, ProbabilityTheory.condDistrib_apply, Eq.mp, MeasureTheory.Measure.map_apply, MeasurableSet.singleton
14 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_fst_of_ne_zero line 244 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Ne, ENNReal, Set, Set.preimage, Singleton.singleton, OfNat.ofNat, Eq, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.fst, ProbabilityTheory.condDistrib, Prod, Prod.mk
Proof uses: MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, Set.ofPred, Membership.mem, Prod.fst, id, congrArg, ProbabilityTheory.Kernel.fst_apply', HMul.hMul, Inv.inv, Inter.inter, ProbabilityTheory.condDistrib_apply', Measurable.prodMk, measurable_fst, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_fst_ae_eq line 255 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.map, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.fst, ProbabilityTheory.condDistrib, Prod, Prod.mk
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, ProbabilityTheory.condDistrib_fst_of_ne_zero, Eq.mp, Set.preimage, MeasureTheory.Measure.map_apply, MeasurableSet.singleton, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_snd_of_ne_zero line 264 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Ne, ENNReal, Set, Set.preimage, Singleton.singleton, OfNat.ofNat, Eq, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.snd, ProbabilityTheory.condDistrib, Prod, Prod.mk
Proof uses: MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, Prod.snd, id, congrArg, ProbabilityTheory.Kernel.snd_apply', HMul.hMul, Inv.inv, Inter.inter, ProbabilityTheory.condDistrib_apply', Measurable.prodMk, measurable_snd, Eq.refl
33 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_snd_ae_eq line 275 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.map, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.snd, ProbabilityTheory.condDistrib, Prod, Prod.mk
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, ProbabilityTheory.condDistrib_snd_of_ne_zero, Eq.mp, Set.preimage, MeasureTheory.Measure.map_apply, MeasurableSet.singleton, Eq.refl
23 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condKernel_condDistrib_ae_eq line 284 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, Prod, MeasureTheory.ae, MeasureTheory.Measure.map, Prod.mk, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.condDistrib, ProbabilityTheory.Kernel.snd
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, MeasureTheory.Measure.ext, MeasurableSet, Set.preimage, Prod.fst, Eq.mp, MeasureTheory.Measure.map_apply, Measurable.prodMk and 75 more
84 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.swap_condDistrib_ae_eq line 339 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, Prod, MeasureTheory.ae, MeasureTheory.Measure.map, Prod.mk, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.comap, ProbabilityTheory.condDistrib, Prod.swap, measurable_swap
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, MeasureTheory.Measure.ext, MeasurableSet, ProbabilityTheory.Kernel.comap_apply', Set.preimage, Set.ext, Iff, Membership.mem and 20 more
31 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_const_unit line 357 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsFiniteMeasure, Filter.EventuallyEq, Prod, Unit, MeasureTheory.ae, MeasureTheory.Measure.map, Prod.mk, Unit.unit, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.condKernel, ProbabilityTheory.Kernel.const, ProbabilityTheory.Kernel.prodMkLeft, ProbabilityTheory.condDistrib
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, Set.preimage, Prod.snd, Set.ext, Iff, Membership.mem, congr, Eq.trans and 30 more
44 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_unit_right line 381 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Eq, ProbabilityTheory.Kernel, Unit, ProbabilityTheory.condDistrib, Unit.unit, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.map
Proof uses: ProbabilityTheory.Kernel.ext, MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, HMul.hMul, Inv.inv, Set.preimage, Singleton.singleton, Inter.inter, id, congrArg, ProbabilityTheory.condDistrib_apply', measurable_const, of_eq_true, Ne, OfNat.ofNat, Eq.trans, True and 16 more
40 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.map_compProd_condDistrib line 391 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Eq, Prod, MeasureTheory.Measure.compProd, MeasureTheory.Measure.map, ProbabilityTheory.condDistrib, Prod.mk
Proof uses: MeasureTheory.Measure.ext, Set, MeasurableSet, Eq.mpr, ENNReal, Set.preimage, id, congrArg, MeasureTheory.Measure.map_apply, Measurable.prodMk, MeasureTheory.lintegral, ProbabilityTheory.Kernel, MeasureTheory.Measure.compProd_apply, tsum, HMul.hMul, Singleton.singleton, SummationFilter.unconditional, MeasureTheory.lintegral_eq_tsum, Inter.inter, AddCommMonoid and 48 more
79 instances, coercions and auxiliary constants left out.

Tactic trace: 29 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.condDistrib_eq_prod_of_indepFun line 427 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, DiscreteMeasurableSpace, MeasurableSingletonClass, Nonempty, Measurable, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, ProbabilityTheory.IndepFun, Prod, Prod.mk, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.map, ProbabilityTheory.Kernel, ProbabilityTheory.condDistrib, ProbabilityTheory.Kernel.prod, ProbabilityTheory.Kernel.prodMkRight, ProbabilityTheory.Kernel.prodMkLeft
Proof uses: Eq.mpr, Filter.Eventually, Eq, id, congrArg, Filter.EventuallyEq.eq_1, Ne, ENNReal, Set, Singleton.singleton, OfNat.ofNat, propext, MeasureTheory.ae_iff_of_countable, MeasureTheory.Measure.ext, MeasurableSet, ProbabilityTheory.cond, Set.preimage, ProbabilityTheory.condDistrib_apply, Measurable.prodMk, Eq.mp and 69 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 46 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.compProd_apply_singleton line 513 source
lemma ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.ae_of_compProd_eq_zero line 534 source
lemma ProbabilityTheory.Kernel._root_.MeasureTheory.Measure.ae_of_ae_compProd line 548 source
lemma ProbabilityTheory.Kernel.compProd_congr_ae line 558 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, MeasureTheory.SFinite, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, Prod, Filter.EventuallyEq, MeasureTheory.ae, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd
Proof uses: Filter.Eventually, Eq, Prod.mk, MeasureTheory.Measure.ae_of_ae_compProd, Filter.mp_mem, Set.ofPred, Membership.mem, Set, Filter.univ_mem', id, MeasureTheory.Measure.ext, MeasurableSet, Eq.mpr, ENNReal, MeasureTheory.lintegral, Set.preimage, congrArg, ProbabilityTheory.Kernel.compProd_apply, Eq.symm, MeasureTheory.lintegral_congr_ae and 1 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
def ProbabilityTheory.Kernel.FiniteKernelSupport The analogue of FiniteSupport for probability kernels line 571 source
Source documentation
The analogue of FiniteSupport for probability kernels.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel
Proof uses: Exists, Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat
8 instances, coercions and auxiliary constants left out.
```
noncomputable def FiniteKernelSupport (κ : Kernel T S) : Prop :=
…
```
def ProbabilityTheory.Kernel.AEFiniteKernelSupport A kernel κ has almost everywhere finite support wrt a measure μ if, for almost every point t, then κ t has finite support line 576 source
Source documentation
A kernel κ has almost everywhere finite support wrt a measure μ if, for almost every point t, then κ t has finite support. Note that we don't require any uniformity wrt t.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasureTheory.Measure
Proof uses: Filter.Eventually, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, MeasureTheory.ae
9 instances, coercions and auxiliary constants left out.
```
noncomputable def AEFiniteKernelSupport (κ : Kernel T S) (μ : Measure T) : Prop :=
…
```
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.aefiniteKernelSupport line 579 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport
Proof uses: MeasureTheory.ae_of_all, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat
9 instances, coercions and auxiliary constants left out.
lemma ProbabilityTheory.Kernel.finiteKernelSupport_zero line 584 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel.FiniteKernelSupport, OfNat.ofNat, ProbabilityTheory.Kernel
Proof uses: Exists.intro, Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, EmptyCollection.emptyCollection, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, Set.univ, zero_apply, Finset.coe_empty, Set.compl_empty, 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.aefiniteKernelSupport_zero line 587 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, OfNat.ofNat, ProbabilityTheory.Kernel
Proof uses: ProbabilityTheory.Kernel.FiniteKernelSupport.aefiniteKernelSupport, ProbabilityTheory.Kernel.finiteKernelSupport_zero
4 instances, coercions and auxiliary constants left out.
def ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk line 598 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport
Proof uses: dite, Nonempty, Classical.propDecidable, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Nonempty.some, Not
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_zero line 606 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, OfNat.ofNat, ProbabilityTheory.Kernel, Eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, of_eq_true, Eq.trans, ProbabilityTheory.Kernel.piecewise, Set.univ, Set, Set.ofPred, Exists, Finset, ENNReal, Compl.compl, DecidablePred, Membership.mem, MeasurableSet, congrArg, True, funext and 23 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq_zero_of_isEmpty line 614 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, IsEmpty, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, OfNat.ofNat
Proof uses: of_eq_true, dite, Nonempty, Classical.propDecidable, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Exists, Finset, ENNReal, Set, Compl.compl, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac, Nonempty.some, Not, Eq.trans, True, Nonempty.intro
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq line 620 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, Nonempty, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Exists, Finset, ENNReal, Set, Compl.compl, OfNat.ofNat, Classical.propDecidable, ProbabilityTheory.Kernel.const, MeasureTheory.Measure.dirac and 1 more
Proof uses: of_eq_true, Eq.trans, eq_true, True, congrFun', congrArg, dite_eq_left_of_eq_true, Not, eq_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk line 626 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, of_eq_true, Eq.trans, OfNat.ofNat, True, congrArg, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq_zero_of_isEmpty, Eq.mpr, Exists, Finset, Eq, ENNReal, Set, Compl.compl, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Classical.propDecidable and 25 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk line 639 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Filter.EventuallyEq, MeasureTheory.ae, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Filter.univ_mem', Set.ofPred, Eq, id, Membership.mem, Set, MeasureTheory.Measure.ext, MeasurableSet, of_eq_true, ENNReal, Eq.trans, OfNat.ofNat, True, congr, congrArg, EmptyCollection.emptyCollection and 21 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.Kernel.AEFiniteKernelSupport.isMarkovKernel_mk line 650 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, ProbabilityTheory.IsMarkovKernel.mk, False.elim, MeasureTheory.IsProbabilityMeasure, IsEmpty.false, MeasureTheory.Measure.nonempty_of_neZero, Inhabited.default, Lean.Elab.Tactic.nonempty_to_inhabited, Eq.mpr, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Exists, Finset, Eq, ENNReal, Set, Compl.compl and 9 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.Kernel.AEFiniteKernelSupport.isZeroOrMarkovKernel_mk line 660 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsZeroOrMarkovKernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: Eq, OfNat.ofNat, ProbabilityTheory.IsMarkovKernel, Or, ProbabilityTheory.eq_zero_or_isMarkovKernel, Eq.mpr, id, congrArg, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_zero, inferInstance, Eq.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
instance ProbabilityTheory.Kernel.AEFiniteKernelSupport.isSFiniteKernel_mk line 668 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.IsSFiniteKernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk
Proof uses: IsEmpty, Nonempty, Or, isEmpty_or_nonempty, Eq.mpr, OfNat.ofNat, id, Eq, congrArg, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk_eq_zero_of_isEmpty, inferInstance, ProbabilityTheory.Kernel.piecewise, Set.ofPred, Exists, Finset, ENNReal, Set, Compl.compl, Classical.propDecidable, ProbabilityTheory.Kernel.const and 3 more
18 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.aefiniteKernelSupport_iff line 676 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, Iff, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Exists, And, ProbabilityTheory.Kernel.FiniteKernelSupport, Filter.EventuallyEq, MeasureTheory.ae
Proof uses: Iff.intro, Exists.intro, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, And.intro, ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk, Filter.EventuallyEq.symm, ProbabilityTheory.Kernel.AEFiniteKernelSupport.ae_eq_mk, Filter.mp_mem, Set.ofPred, Eq, Finset, ENNReal, Set, Compl.compl, OfNat.ofNat, Filter.univ_mem', Membership.mem, id, Eq.mpr, congrArg and 1 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport Finite kernel support locally implies uniform finite kernel support line 686 source
Source documentation
Finite kernel support locally implies uniform finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, Finset, Exists, Membership.mem, Filter.Eventually, MeasureTheory.ae, MeasureTheory.Measure
Proof uses: Exists.intro, Finset.biUnion, Classical.propDecidable, Eq, Exists.choose, ENNReal, Set, Compl.compl, OfNat.ofNat, id, MeasureTheory.measure_mono_null, Eq.mpr, Not, implies_congr, Eq.trans, Set.iInter, congrFun', congrArg, Set.iUnion, Finset.coe_biUnion and 11 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma local_support_of_finiteKernelSupport
    {κ : Kernel T S} (h : FiniteKernelSupport κ) (A : Finset T) :
    ∃ B : Finset S, ∀ t ∈ A, ∀ᵐ x ∂(κ t), x ∈ B := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.finiteKernelSupport_of_finite_range Finite range implies finite kernel support line 702 source
Source documentation
Finite range implies finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Finite, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport
Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Exists.intro, Finset, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat, Finset.univ, of_eq_true, Eq.trans, True, congrFun', congrArg, EmptyCollection.emptyCollection, Set.univ and 5 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma finiteKernelSupport_of_finite_range [Finite S] (κ : Kernel T S) : FiniteKernelSupport κ := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.deterministic Deterministic kernels have finite kernel support line 709 source
Source documentation
Deterministic kernels have finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, Prod, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.deterministic, Measurable.of_discrete
Proof uses: Exists, Finset, Eq, ENNReal, MeasureTheory.Measure, Set, ProbabilityTheory.Kernel, Compl.compl, OfNat.ofNat, Exists.intro, Prod.mk, Singleton.singleton, Eq.mpr, Set.indicator, id, congrArg, ProbabilityTheory.Kernel.deterministic_apply', of_eq_true, MeasurableSet, Eq.trans and 10 more
26 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.deterministic [Countable S] [Countable T]
    [MeasurableSingletonClass S] [MeasurableSingletonClass T] [MeasurableSingletonClass U]
    (f : T × S → U) :
    FiniteKernelSupport (deterministic f .of_discrete) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.map maps preserve finite kernel support line 719 source
Source documentation
maps preserve finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.map
Proof uses: dite, Measurable, Classical.propDecidable, Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat, Exists, Exists.intro, Finset.image, Eq.mpr, Set.preimage, id, congrArg, ProbabilityTheory.Kernel.map_apply', MeasurableSet.compl, Set.Finite.measurableSet and 19 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.map [MeasurableSingletonClass U]
    {κ : Kernel T S} (hκ : FiniteKernelSupport κ) (f : S → U) :
    FiniteKernelSupport (map κ f) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.map line 738 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.map
Proof uses: dite, Measurable, Classical.propDecidable, Filter.mp_mem, MeasureTheory.ae, Set.ofPred, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, Filter.univ_mem', Membership.mem, id, Exists.intro, Finset.image, Eq.mpr, Set.preimage and 22 more
22 instances, coercions and auxiliary constants left out.

Tactic trace: 19 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.comap comaps preserve finite kernel support line 757 source
Source documentation
comaps preserve finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, Measurable, ProbabilityTheory.Kernel.comap
Proof uses: Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat, Exists, Exists.intro, Eq.mpr, id, congrArg, ProbabilityTheory.Kernel.comap_apply
9 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.comap {κ : Kernel T S} (hκ : FiniteKernelSupport κ)
    {f : U → T} (hf : Measurable f) :
    FiniteKernelSupport (comap κ f hf) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.comap_equiv line 765 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasurableEquiv, ProbabilityTheory.Kernel.comap, MeasurableEquiv.measurable, MeasureTheory.Measure.comap
Proof uses: Eq.mpr, MeasureTheory.Measure.map, MeasurableEquiv.symm, id, Eq, congrArg, Eq.symm, MeasurableEquiv.map_symm, Filter.Eventually, Exists, Finset, ENNReal, Set, Compl.compl, OfNat.ofNat, MeasureTheory.ae, ProbabilityTheory.Kernel.AEFiniteKernelSupport.eq_1, propext, MeasureTheory.ae_map_iff, Measurable.aemeasurable and 9 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.FiniteKernelSupport.fst Projecting a kernel to first coordinate preserves finite kernel support line 779 source
Source documentation
Projecting a kernel to first coordinate preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.fst, id, Eq, congrArg, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.FiniteKernelSupport.map
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.fst [MeasurableSingletonClass S]
   {κ : Kernel T (S × U)} (hκ : FiniteKernelSupport κ) :
    FiniteKernelSupport (fst κ) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.fst line 785 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.fst, id, Eq, congrArg, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.map
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.snd Projecting a kernel to second coordinate preserves finite kernel support line 792 source
Source documentation
Projecting a kernel to second coordinate preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.snd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.snd, id, Eq, congrArg, ProbabilityTheory.Kernel.snd_eq, ProbabilityTheory.Kernel.FiniteKernelSupport.map
2 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.snd [MeasurableSingletonClass U]
    {κ : Kernel T (S × U)} (hκ : FiniteKernelSupport κ) :
    FiniteKernelSupport (snd κ) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.snd line 798 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.snd
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.snd, id, Eq, congrArg, ProbabilityTheory.Kernel.snd_eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.map
2 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_of_cond Conditioning a kernel preserves finite kernel support line 805 source
Source documentation
Conditioning a kernel preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, Nonempty, MeasurableSingletonClass, Countable, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.IsFiniteKernel, ProbabilityTheory.Kernel.condKernel, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.fst
Proof uses: Eq.mpr, Filter.Eventually, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, MeasureTheory.ae, id, congrArg, ProbabilityTheory.Kernel.AEFiniteKernelSupport.eq_1, Ne, Singleton.singleton, propext, MeasureTheory.ae_iff_of_countable, Prod.mk, Eq.mp, And.right and 31 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma aefiniteKernelSupport_of_cond {κ : Kernel T (S × U)} [hU : Nonempty U]
    [MeasurableSingletonClass S] [MeasurableSingletonClass T]
    [MeasurableSingletonClass U] [Countable U] [Countable S] [Countable T]
    (μ : Measure T) (hκ : AEFiniteKernelSupport κ μ) [IsFiniteKernel κ] :
    AEFiniteKernelSupport (condKernel κ) (μ ⊗ₘ (Kernel.fst κ)) := by
…
```
Mentions: hU, ProbabilityTheory.Kernel.AEFiniteKernelSupport
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.swapRight Swapping a kernel right preserves finite kernel support line 831 source
Source documentation
Swapping a kernel right preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.swapRight
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.swap, id, Eq, congrArg, ProbabilityTheory.Kernel.swapRight_eq, ProbabilityTheory.Kernel.FiniteKernelSupport.map
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.swapRight
    [MeasurableSingletonClass S] [MeasurableSingletonClass U]
    {κ : Kernel T (S × U)} (hκ : FiniteKernelSupport κ) :
    FiniteKernelSupport (swapRight κ) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.swapRight line 838 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, MeasurableSingletonClass, ProbabilityTheory.Kernel.AEFiniteKernelSupport, ProbabilityTheory.Kernel.swapRight
Proof uses: Eq.mpr, ProbabilityTheory.Kernel.map, Prod.swap, id, Eq, congrArg, ProbabilityTheory.Kernel.swapRight_eq, ProbabilityTheory.Kernel.AEFiniteKernelSupport.map
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.prod Products preserve finite kernel support line 846 source
Source documentation
Products preserve finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, MeasurableSingletonClass, ProbabilityTheory.IsMarkovKernel, ProbabilityTheory.Kernel.FiniteKernelSupport, Prod, ProbabilityTheory.Kernel.prod
Proof uses: Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat, Exists, Exists.intro, SProd.sprod, Eq.mpr, MeasureTheory.lintegral, Set.preimage, Prod.mk, id, congrArg, ProbabilityTheory.Kernel.prod_apply', MeasurableSet, Eq.trans, Finset.coe_product and 17 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 13 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.prod {κ : Kernel T S} {η : Kernel T U}
    [MeasurableSingletonClass S] [MeasurableSingletonClass U]
    [IsMarkovKernel κ] [IsMarkovKernel η]
    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) :
    FiniteKernelSupport (κ ×ₖ η) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.prod line 861 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.IsMarkovKernel, MeasureTheory.Measure, ProbabilityTheory.Kernel.AEFiniteKernelSupport, Prod, ProbabilityTheory.Kernel.prod
Proof uses: Filter.mp_mem, MeasureTheory.ae, Set.ofPred, Exists, Finset, Eq, ENNReal, Set, Compl.compl, OfNat.ofNat, Membership.mem, Filter.univ_mem', id, Exists.intro, SProd.sprod, Eq.mpr, congrArg, Finset.coe_product, Union.union, Set.univ and 12 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.compProd Composition-product preserves finite kernel support line 871 source
Source documentation
Composition-product preserves finite kernel support

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, ProbabilityTheory.Kernel.FiniteKernelSupport, ProbabilityTheory.Kernel.compProd
Proof uses: dite, ProbabilityTheory.IsSFiniteKernel, Classical.propDecidable, Finset, Eq, ENNReal, MeasureTheory.Measure, Set, Compl.compl, OfNat.ofNat, Exists, Membership.mem, SProd.sprod, Singleton.singleton, Filter.Eventually, MeasureTheory.ae, ProbabilityTheory.Kernel.local_support_of_finiteKernelSupport, Exists.intro, Eq.mpr, MeasureTheory.lintegral and 44 more
45 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.
```
lemma FiniteKernelSupport.compProd [MeasurableSingletonClass S] [MeasurableSingletonClass U]
    {κ : Kernel T S} {η : Kernel (T × S) U}
    (hκ : FiniteKernelSupport κ) (hη : FiniteKernelSupport η) :
    FiniteKernelSupport (κ ⊗ₖ η) := by
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.compProd line 892 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, Countable, MeasurableSingletonClass, ProbabilityTheory.Kernel, Prod, MeasureTheory.Measure, MeasureTheory.SFinite, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.Measure.compProd, ProbabilityTheory.Kernel.compProd
Proof uses: dite, ProbabilityTheory.IsSFiniteKernel, Classical.propDecidable, Eq.mpr, Exists, And, ProbabilityTheory.Kernel.FiniteKernelSupport, Filter.EventuallyEq, MeasureTheory.ae, id, Eq, congrArg, propext, ProbabilityTheory.Kernel.aefiniteKernelSupport_iff, Exists.intro, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, And.intro, ProbabilityTheory.Kernel.FiniteKernelSupport.compProd, ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk, MeasureTheory.Measure.compProd_congr and 21 more
14 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkRight prodMkRight preserves finite kernel support line 909 source
Source documentation
prodMkRight preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, Prod, ProbabilityTheory.Kernel.prodMkRight
Proof uses: ProbabilityTheory.Kernel.FiniteKernelSupport.comap, Prod.fst, measurable_fst
2 instances, coercions and auxiliary constants left out.
```
lemma FiniteKernelSupport.prodMkRight {κ : Kernel T S} (hκ : FiniteKernelSupport κ) :
    FiniteKernelSupport (prodMkRight U κ) :=
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.prodMkRight line 913 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.SFinite, Prod, ProbabilityTheory.Kernel.prodMkRight, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, Exists, And, ProbabilityTheory.Kernel.FiniteKernelSupport, Filter.EventuallyEq, MeasureTheory.ae, id, Eq, congrArg, propext, ProbabilityTheory.Kernel.aefiniteKernelSupport_iff, Exists.intro, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, And.intro, ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkRight, ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk, Filter.Eventually, Filter.EventuallyEq.eq_1, Membership.mem, Set and 17 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkLeft prodMkLeft preserves finite kernel support line 929 source
Source documentation
prodMkLeft preserves finite kernel support.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.FiniteKernelSupport, Prod, ProbabilityTheory.Kernel.prodMkLeft
Proof uses: ProbabilityTheory.Kernel.FiniteKernelSupport.comap, Prod.snd, measurable_snd
2 instances, coercions and auxiliary constants left out.
```
lemma FiniteKernelSupport.prodMkLeft {κ : Kernel T S} (hκ : FiniteKernelSupport κ) :
    FiniteKernelSupport (prodMkLeft U κ) :=
…
```
Mentions: ProbabilityTheory.Kernel.FiniteKernelSupport
lemma ProbabilityTheory.Kernel.AEFiniteKernelSupport.prodMkLeft line 933 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: MeasurableSpace, MeasurableSingletonClass, Countable, MeasureTheory.Measure, ProbabilityTheory.Kernel, ProbabilityTheory.Kernel.AEFiniteKernelSupport, MeasureTheory.SFinite, Prod, ProbabilityTheory.Kernel.prodMkLeft, MeasureTheory.Measure.prod
Proof uses: Eq.mpr, Exists, And, ProbabilityTheory.Kernel.FiniteKernelSupport, Filter.EventuallyEq, MeasureTheory.ae, id, Eq, congrArg, propext, ProbabilityTheory.Kernel.aefiniteKernelSupport_iff, Exists.intro, ProbabilityTheory.Kernel.AEFiniteKernelSupport.mk, And.intro, ProbabilityTheory.Kernel.FiniteKernelSupport.prodMkLeft, ProbabilityTheory.Kernel.AEFiniteKernelSupport.finiteKernelSupport_mk, Filter.Eventually, Filter.EventuallyEq.eq_1, Membership.mem, Set and 15 more
12 instances, coercions and auxiliary constants left out.

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