CompProdEqIff

📁 Source: Mathlib/Probability/Kernel/CompProdEqIff.lean

Statistics

Metric	Count
Definitions	0
Theorems compProd_withDensity, ae_eq_of_compProd_eq, compProd_eq_iff	3
Total	3

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd_withDensity 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	compProd ProbabilityTheory.Kernel.withDensity withDensity	—	ext compProd_apply MeasureTheory.withDensity_apply MeasureTheory.lintegral_indicator lintegral_compProd Measurable.indicator ProbabilityTheory.Kernel.withDensity_apply' measurable_prodMk_left

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_eq_of_compProd_eq 📖	mathematical	MeasureTheory.Measure.compProd	Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.absolutelyContinuous_of_eq IsFiniteKernel.isSFiniteKernel Filter.mp_mem Filter.univ_mem' withDensity_rnDeriv_eq MeasureTheory.Measure.ae_ae_of_ae_compProd MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel measurable_rnDeriv measurable_const MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter one_mul MeasureTheory.Measure.compProd_congr instIsFiniteKernelWithDensityRnDeriv MeasureTheory.Measure.compProd_withDensity MeasureTheory.withDensity_apply rnDeriv_eq_one_iff_eq
compProd_eq_iff 📖	mathematical	—	MeasureTheory.Measure.compProd Filter.EventuallyEq MeasureTheory.Measure MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.Measure.instOuterMeasureClass ae_eq_of_compProd_eq MeasureTheory.Measure.compProd_congr IsFiniteKernel.isSFiniteKernel

---

← Back to Index