Basic

📁 Source: Mathlib/Probability/Kernel/Disintegration/Basic.lean

Statistics

Metric	Count
Definitions IsCondKernel, IsCondKernel, condKernelCountable	3
Theorems apply_of_ne_zero, disintegrate, isMarkovKernel, isProbabilityMeasure, isSFiniteKernel, disintegrate, disintegrate, isProbabilityMeasure_ae, instIsCondKernel, instIsMarkovKernel, condKernelCountable_apply, disintegrate, instIsCondKernel_zero	13
Total	16

MeasureTheory.Measure

Definitions

Name	Category	Theorems
IsCondKernel 📖	CompData	1 math math: condKernel.instIsCondKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disintegrate 📖	mathematical	—	compProd fst	—	IsCondKernel.disintegrate

MeasureTheory.Measure.IsCondKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_of_ne_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv MeasureTheory.Measure.fst Set.instSingletonSet Prod.instMeasurableSpace SProd.sprod Set.instSProd	—	IsScalarTower.right MeasureTheory.Measure.ext Set.singleton_prod MeasurableEmbedding.comap_apply measurableEmbedding_prodMk_left
disintegrate 📖	mathematical	—	MeasureTheory.Measure.compProd MeasureTheory.Measure.fst	—	—
isMarkovKernel 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel	—	isProbabilityMeasure
isProbabilityMeasure 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	apply_of_ne_zero Set.prod_univ MeasureTheory.Measure.fst_apply MeasurableSingletonClass.measurableSet_singleton ENNReal.inv_mul_cancel MeasureTheory.measure_ne_top MeasureTheory.Measure.fst.instIsFiniteMeasure
isSFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel	—	Mathlib.Tactic.Contrapose.contrapose₂ MeasureTheory.Measure.disintegrate MeasureTheory.Measure.compProd_of_not_isSFiniteKernel

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
IsCondKernel 📖	CompData	6 math math: condKernelUnitBorel.instIsCondKernel, condKernelBorel.instIsCondKernel, condKernel.instIsCondKernel, instIsCondKernel_zero, condKernelCountable.instIsCondKernel, condKernelUnitReal.instIsCondKernel
condKernelCountable 📖	CompOp	4 math math: condKernelCountable.instIsCondKernel, condKernelCountable_apply, condKernel_def, condKernelCountable.instIsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condKernelCountable_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike condKernelCountable	—	—
disintegrate 📖	mathematical	—	compProd fst	—	IsCondKernel.disintegrate
instIsCondKernel_zero 📖	mathematical	—	IsCondKernel ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	fst_zero compProd_zero_left

ProbabilityTheory.Kernel.IsCondKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disintegrate 📖	mathematical	—	ProbabilityTheory.Kernel.compProd ProbabilityTheory.Kernel.fst	—	—
isProbabilityMeasure_ae 📖	mathematical	—	Filter.Eventually MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.fst	—	ProbabilityTheory.Kernel.disintegrate MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.fst_compProd_apply ProbabilityTheory.Kernel.IsSFiniteKernel.fst ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_fst Measurable.comp ProbabilityTheory.Kernel.measurable_coe MeasurableSet.univ measurable_prodMk_left MeasureTheory.ae_le_const_iff_forall_gt_measure_zero ENNReal.instOrderTopology TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace measurableSet_Ici BorelSpace.opensMeasurable ENNReal.borelSpace instClosedIciTopology OrderTopology.to_orderClosedTopology Set.indicator_of_mem Set.indicator_of_notMem LE.le.trans_eq MeasureTheory.lintegral_mono Mathlib.Tactic.Contrapose.contrapose₁ one_mul ENNReal.mul_lt_mul_left ne_of_gt lt_of_le_of_ne' zero_le ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.lintegral_indicator_const MeasureTheory.ae_const_le_iff_forall_lt_measure_zero measurableSet_Iic instClosedIicTopology Eq.trans_le Filter.mp_mem Filter.univ_mem' le_antisymm MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.ae.congr_simp ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_right ProbabilityTheory.Kernel.fst_zero MeasureTheory.ae_zero

ProbabilityTheory.Kernel.condKernelCountable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCondKernel 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasureTheory.Measure.IsCondKernel DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	ProbabilityTheory.Kernel.IsCondKernel ProbabilityTheory.Kernel.condKernelCountable	—	ProbabilityTheory.Kernel.ext MeasureTheory.Measure.ext MeasureTheory.Measure.disintegrate ProbabilityTheory.Kernel.compProd_apply ProbabilityTheory.Kernel.IsSFiniteKernel.fst ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernel MeasureTheory.Measure.compProd_apply MeasureTheory.Measure.instSFiniteFstOfProd ProbabilityTheory.IsSFiniteKernel.sFinite
instIsMarkovKernel 📖	mathematical	ProbabilityTheory.IsMarkovKernel	Prod.instMeasurableSpace ProbabilityTheory.Kernel.condKernelCountable	—	ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure

---

← Back to Index