MeasurableLIntegral

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

Statistics

Metric	Count
Definitions	0
Theorems lintegral_kernel, lintegral_kernel_prod_left, lintegral_kernel_prod_left', lintegral_kernel_prod_right, lintegral_kernel_prod_right', lintegral_kernel_prod_right'', setLIntegral_kernel, setLIntegral_kernel_prod_left, setLIntegral_kernel_prod_right, measurable_kernel_prodMk_left, measurable_kernel_prodMk_left', measurable_kernel_prodMk_left_of_finite, measurable_kernel_prodMk_right, measurable_lintegral_indicator_const	14
Total	14

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lintegral_kernel 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	fun_comp MeasureTheory.Measure.measurable_lintegral ProbabilityTheory.Kernel.measurable
lintegral_kernel_prod_left 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	lintegral_kernel_prod_right fun_comp prodMk snd measurable_id' fst
lintegral_kernel_prod_left' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	lintegral_kernel_prod_right fun_comp prodMk snd measurable_id' fst
lintegral_kernel_prod_right 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	MeasureTheory.SimpleFunc.iSup_eapprox_apply MeasureTheory.lintegral_iSup comp MeasureTheory.SimpleFunc.measurable measurable_prodMk_left MeasureTheory.SimpleFunc.monotone_eapprox iSup ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology instCountableNat MeasureTheory.SimpleFunc.induction Set.piecewise_eq_indicator ProbabilityTheory.Kernel.measurable_lintegral_indicator_const Pi.add_apply MeasureTheory.lintegral_add_left fun_comp prodMk measurable_const measurable_id' add ContinuousAdd.measurableMul₂ ENNReal.instContinuousAdd
lintegral_kernel_prod_right' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	lintegral_kernel_prod_right
lintegral_kernel_prod_right'' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	comp lintegral_kernel_prod_right' fun_comp prodMk snd fst measurable_id' measurable_prodMk_left
setLIntegral_kernel 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	setLIntegral_kernel_prod_right fun_comp snd measurable_id'
setLIntegral_kernel_prod_left 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	ProbabilityTheory.Kernel.lintegral_restrict lintegral_kernel_prod_left ProbabilityTheory.Kernel.IsSFiniteKernel.restrict
setLIntegral_kernel_prod_right 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	ProbabilityTheory.Kernel.lintegral_restrict lintegral_kernel_prod_right ProbabilityTheory.Kernel.IsSFiniteKernel.restrict

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_kernel_prodMk_left 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.preimage	—	instCountableNat kernel_sum_seq sum_apply' measurable_prodMk_left Measurable.ennreal_tsum measurable_kernel_prodMk_left_of_finite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure isFiniteKernel_seq
measurable_kernel_prodMk_left' 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.preimage	—	Measurable.comp measurable_kernel_prodMk_left Measurable.prodMk Measurable.snd measurable_fst measurable_snd measurable_prodMk_left
measurable_kernel_prodMk_left_of_finite 📖	mathematical	MeasurableSet Prod.instMeasurableSpace MeasureTheory.IsFiniteMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	Measurable ENNReal ENNReal.measurableSpace Set MeasureTheory.Measure.instFunLike Set.preimage	—	MeasurableSpace.induction_on_inter generateFrom_prod isPiSystem_prod MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass Set.mk_preimage_prod_right_eq_if Measurable.ite measurable_coe measurable_const Set.ext Set.diff_inter_self_eq_diff Set.inter_univ MeasureTheory.measure_diff Set.subset_univ MeasurableSet.nullMeasurableSet measurable_prodMk_left MeasureTheory.measure_ne_top Measurable.sub ENNReal.instMeasurableSub₂ MeasurableSet.univ Set.preimage_iUnion MeasureTheory.measure_iUnion instCountableNat Pairwise.mono Disjoint.preimage Measurable.ennreal_tsum
measurable_kernel_prodMk_right 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Set.preimage	—	measurable_kernel_prodMk_left measurableSet_swap_iff
measurable_lintegral_indicator_const 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	Measurable ENNReal ENNReal.measurableSpace MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Set.indicator instZeroENNReal	—	MeasureTheory.lintegral_indicator_const_comp measurable_prodMk_left Measurable.const_mul MeasurableMul₂.toMeasurableMul ENNReal.instMeasurableMul₂ measurable_kernel_prodMk_left

---

← Back to Index