Commit 2024-07-26 12:50 ad0a80b0

View on Github →

refactor: Extract predicate for conditional kernels (#15105) Sometimes conditional kernels exist "by chance" and the existing Measure.condKernel and Kernel.condKernel definitions fail to capture this. This PR extracts the disintegration property of conditional kernels into two Prop-valued typeclasses Measure.IsCondKernel and Kernel.IsCondKernel. Zulip

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Probability/Kernel/Basic.lean

added theorem ProbabilityTheory.Kernel.apply_congr_of_mem_measurableAtom

added theorem ProbabilityTheory.Kernel.isSFiniteKernel_const

Modified Mathlib/Probability/Kernel/Composition.lean

added theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkLeft_unit

added theorem ProbabilityTheory.Kernel.isSFiniteKernel_prodMkRight_unit

Created Mathlib/Probability/Kernel/Disintegration/Basic.lean

added theorem MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero

added theorem MeasureTheory.Measure.IsCondKernel.isMarkovKernel

added theorem MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure

added theorem MeasureTheory.Measure.IsCondKernel.isSFiniteKernel

added theorem MeasureTheory.Measure.disintegrate

added theorem ProbabilityTheory.Kernel.condKernelCountable_apply

added theorem ProbabilityTheory.Kernel.disintegrate

Modified Mathlib/Probability/Kernel/Disintegration/Integral.lean

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean

modified theorem ProbabilityTheory.Kernel.compProd_fst_condKernel

deleted def ProbabilityTheory.Kernel.condKernelCountable

deleted theorem ProbabilityTheory.Kernel.condKernelCountable_apply

modified def ProbabilityTheory.Kernel.condKernelUnitBorel

Modified Mathlib/Probability/Kernel/Disintegration/Unique.lean

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

added theorem MeasureTheory.Measure.compProd_of_not_isSFiniteKernel

added theorem MeasureTheory.Measure.compProd_of_not_sfinite