AbsolutelyContinuous

📁 Source: Mathlib/Probability/Kernel/Composition/AbsolutelyContinuous.lean

Statistics

Metric	Count
Definitions	0
Theorems kernel_of_compProd, compProd_of_right, compProd_of_right', absolutelyContinuous_compProd_iff', absolutelyContinuous_compProd_right_iff, mutuallySingular_compProd_right_iff	6
Total	6

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_compProd_iff' 📖	mathematical	MeasureTheory.Measure instZero DFunLike.coe ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike	AbsolutelyContinuous Prod.instMeasurableSpace compProd Filter.Eventually MeasureTheory.ae instFunLike instOuterMeasureClass	—	instOuterMeasureClass absolutelyContinuous_of_compProd ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel AbsolutelyContinuous.kernel_of_compProd AbsolutelyContinuous.compProd
absolutelyContinuous_compProd_right_iff 📖	mathematical	—	AbsolutelyContinuous Prod.instMeasurableSpace compProd Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae instFunLike instOuterMeasureClass	—	instOuterMeasureClass AbsolutelyContinuous.kernel_of_compProd AbsolutelyContinuous.compProd_right ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel
mutuallySingular_compProd_right_iff 📖	mathematical	—	MutuallySingular Prod.instMeasurableSpace compProd Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae instFunLike instOuterMeasureClass	—	instOuterMeasureClass mutuallySingular_of_mutuallySingular_compProd ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel AbsolutelyContinuous.rfl MutuallySingular.compProd_of_right

MeasureTheory.Measure.AbsolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kernel_of_compProd 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous Prod.instMeasurableSpace MeasureTheory.Measure.compProd	Filter.Eventually DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.MutuallySingular.compProd_of_right ProbabilityTheory.Kernel.instIsFiniteKernelSingularPart Filter.Eventually.of_forall ProbabilityTheory.Kernel.mutuallySingular_singularPart MeasureTheory.Measure.compProd_eq_zero_iff MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular add_left_iff MeasureTheory.Measure.compProd_add_right ProbabilityTheory.Kernel.instIsFiniteKernelWithDensityRnDeriv ProbabilityTheory.Kernel.rnDeriv_add_singularPart Filter.mp_mem Filter.univ_mem' ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous

MeasureTheory.Measure.MutuallySingular

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd_of_right 📖	mathematical	Filter.Eventually MeasureTheory.Measure.MutuallySingular DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Prod.instMeasurableSpace MeasureTheory.Measure.compProd	—	MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.Kernel.measurableSet_mutuallySingularSet symm MeasureTheory.Measure.compProd_apply ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel MeasurableSet.compl ProbabilityTheory.Kernel.measure_mutuallySingularSetSlice Filter.mp_mem Filter.univ_mem' ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular MeasureTheory.lintegral_const MulZeroClass.zero_mul MeasureTheory.lintegral_congr_ae MeasureTheory.Measure.compProd_of_not_sfinite
compProd_of_right' 📖	mathematical	Filter.Eventually MeasureTheory.Measure.MutuallySingular DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Prod.instMeasurableSpace MeasureTheory.Measure.compProd	—	MeasureTheory.Measure.instOuterMeasureClass symm compProd_of_right

---

← Back to Index