Documentation Verification Report

MeasurableIntegral

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

Statistics

Metric	Count
Definitions	0
Theorems `integral_kernel`, `integral_kernel_prod_left`, `integral_kernel_prod_left'`, `integral_kernel_prod_left''`, `integral_kernel_prod_right`, `integral_kernel_prod_right'`, `integral_kernel_prod_right''`, `measurableSet_integrable`, `measurableSet_kernel_integrable`	9
Total	9

MeasureTheory.StronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_kernel` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`separableSpace_range_union_singleton` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `measurable` `Set.union_singleton` `stronglyMeasurable_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `indicator` `MeasureTheory.SimpleFunc.integral_eq` `Finset.stronglyMeasurable_fun_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smul_const` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Measurable.stronglyMeasurable` `instSecondCountableTopologyReal` `Real.borelSpace` `Measurable.ennreal_toReal` `ProbabilityTheory.Kernel.measurable_coe` `MeasureTheory.SimpleFunc.measurableSet_fiber` `ProbabilityTheory.measurableSet_integrable` `tendsto_pi_nhds` `Set.indicator_of_mem` `MeasureTheory.tendsto_integral_approxOn_of_measurable_of_range_subset` `subset_rfl` `Set.instReflSubset` `Set.indicator_of_notMem` `MeasureTheory.integral_undef` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `MeasureTheory.integral_def`
`integral_kernel_prod_left` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`integral_kernel_prod_right'` `comp_measurable` `measurable_swap`
`integral_kernel_prod_left'` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`integral_kernel_prod_right'` `comp_measurable` `measurable_swap`
`integral_kernel_prod_left''` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`comp_measurable` `integral_kernel_prod_left'` `Measurable.prodMk` `measurable_fst` `Measurable.snd` `measurable_snd` `measurable_prodMk_left`
`integral_kernel_prod_right` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`BorelSpace.opensMeasurable` `measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Set.union_singleton` `separableSpace_range_union_singleton` `measurable_prodMk_left` `indicator` `Finset.Subset.trans` `Finset.filter_subset` `MeasureTheory.SimpleFunc.integral_eq_sum_of_subset` `Finset.stronglyMeasurable_fun_sum` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `smul_const` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Measurable.stronglyMeasurable` `instSecondCountableTopologyReal` `Real.borelSpace` `Measurable.ennreal_toReal` `ProbabilityTheory.Kernel.measurable_kernel_prodMk_left` `MeasureTheory.SimpleFunc.measurableSet_fiber` `ProbabilityTheory.measurableSet_kernel_integrable` `tendsto_pi_nhds` `MeasureTheory.Integrable.mono'` `MeasureTheory.Integrable.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.Integrable.norm` `MeasureTheory.SimpleFunc.aestronglyMeasurable` `Filter.univ_mem'` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.SimpleFunc.norm_approxOn_zero_le` `Set.indicator_of_mem` `MeasureTheory.SimpleFunc.integral_eq_integral` `MeasureTheory.tendsto_integral_of_dominated_convergence` `Filter.Eventually.of_forall` `MeasureTheory.SimpleFunc.tendsto_approxOn` `subset_closure` `Set.indicator_of_notMem` `MeasureTheory.integral_undef` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `stronglyMeasurable_of_tendsto` `instIsCountablyGenerated_atTop` `OrderTopology.of_linearLocallyFinite` `instDiscreteTopologyNat` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `instCountableNat` `MeasureTheory.integral_def`
`integral_kernel_prod_right'` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`integral_kernel_prod_right`
`integral_kernel_prod_right''` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	—	`comp_measurable` `integral_kernel_prod_right'` `Measurable.prodMk` `Measurable.snd` `measurable_fst` `measurable_snd` `measurable_prodMk_left`

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measurableSet_integrable` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`MeasurableSet` `setOf` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	—	`MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `measurableSet_lt` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Measurable.lintegral_kernel` `MeasureTheory.StronglyMeasurable.enorm` `measurable_const`
`measurableSet_kernel_integrable` 📖	mathematical	`MeasureTheory.StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasurableSet` `setOf` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	—	`MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.of_uncurry_left` `measurableSet_lt` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `Measurable.lintegral_kernel_prod_right` `MeasureTheory.StronglyMeasurable.enorm` `measurable_const`

---

← Back to Index