Documentation Verification Report

Integral

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

Statistics

Metric	Count
Definitions	0
Theorems `ae_integrable_condKernel_iff`, `integral_condKernel`, `integral_kernel_condKernel`, `condKernel_ae`, `integral_condKernel`, `integral_norm_condKernel`, `norm_integral_condKernel`, `integral_condKernel`, `lintegral_condKernel`, `lintegral_condKernel_mem`, `setIntegral_condKernel`, `setIntegral_condKernel_univ_left`, `setIntegral_condKernel_univ_right`, `setLIntegral_condKernel`, `setLIntegral_condKernel_eq_measure_prod`, `setLIntegral_condKernel_univ_left`, `setLIntegral_condKernel_univ_right`, `integral_condKernel`, `lintegral_condKernel`, `lintegral_condKernel_mem`, `setIntegral_condKernel`, `setIntegral_condKernel_univ_left`, `setIntegral_condKernel_univ_right`, `setLIntegral_condKernel`, `setLIntegral_condKernel_eq_measure_prod`, `setLIntegral_condKernel_univ_left`, `setLIntegral_condKernel_univ_right`	27
Total	27

MeasureTheory.AEStronglyMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ae_integrable_condKernel_iff` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`Filter.Eventually` `MeasureTheory.Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.fst` `Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.disintegrate` `MeasureTheory.Measure.condKernel.instIsCondKernel` `MeasureTheory.Measure.integrable_compProd_iff` `MeasureTheory.Measure.instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `MeasureTheory.Measure.instIsMarkovKernelCondKernel`
`integral_condKernel` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `MeasureTheory.Measure.fst`	—	`integral_kernel_compProd` `ProbabilityTheory.Kernel.const.instIsSFiniteKernel` `MeasureTheory.Measure.instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsSFiniteKernel.prodMkLeft` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `MeasureTheory.Measure.instIsMarkovKernelCondKernel` `MeasureTheory.Measure.disintegrate` `MeasureTheory.Measure.condKernel.instIsCondKernel`
`integral_kernel_condKernel` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instMeasurableSpace` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike`	`MeasureTheory.integral` `ProbabilityTheory.Kernel.condKernel` `ProbabilityTheory.Kernel.fst`	—	`integral_kernel_compProd` `ProbabilityTheory.Kernel.IsSFiniteKernel.fst` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelCondKernel` `ProbabilityTheory.Kernel.disintegrate` `ProbabilityTheory.Kernel.condKernel.instIsCondKernel`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condKernel_ae` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace`	`Filter.Eventually` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `MeasureTheory.ae` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.fst`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff`
`integral_condKernel` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `MeasureTheory.Measure.fst`	—	`MeasureTheory.integrable_norm_iff` `MeasureTheory.AEStronglyMeasurable.integral_condKernel` `norm_integral_condKernel`
`integral_norm_condKernel` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace`	`Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.Measure.fst`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff`
`norm_integral_condKernel` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace`	`Real` `Real.pseudoMetricSpace` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.integral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `MeasureTheory.Measure.condKernel` `MeasureTheory.Measure.fst`	—	`mono` `integral_norm_condKernel` `MeasureTheory.AEStronglyMeasurable.norm` `MeasureTheory.AEStronglyMeasurable.integral_condKernel` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `norm_norm` `LE.le.trans_eq` `MeasureTheory.norm_integral_le_integral_norm` `Real.norm_of_nonneg` `MeasureTheory.integral_nonneg_of_ae` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `norm_nonneg`

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_condKernel` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace`	`MeasureTheory.integral` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel`	—	`disintegrate` `condKernel.instIsCondKernel` `integral_compProd` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`lintegral_condKernel` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel`	—	`disintegrate` `condKernel.instIsCondKernel` `lintegral_compProd` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`lintegral_condKernel_mem` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`MeasureTheory.lintegral` `fst` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `setOf` `Set.instMembership`	—	`disintegrate` `condKernel.instIsCondKernel` `compProd_apply` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`setIntegral_condKernel` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd`	`MeasureTheory.integral` `restrict` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel`	—	`disintegrate` `condKernel.instIsCondKernel` `setIntegral_compProd` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`setIntegral_condKernel_univ_left` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	`MeasureTheory.integral` `fst` `restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel`	—	`setIntegral_condKernel` `MeasurableSet.univ` `restrict_univ`
`setIntegral_condKernel_univ_right` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	`MeasureTheory.integral` `restrict` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel`	—	`setIntegral_condKernel` `MeasurableSet.univ` `restrict_univ`
`setLIntegral_condKernel` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `restrict` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `SProd.sprod` `Set` `Set.instSProd`	—	`disintegrate` `condKernel.instIsCondKernel` `setLIntegral_compProd` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`setLIntegral_condKernel_eq_measure_prod` 📖	mathematical	`MeasurableSet`	`MeasureTheory.lintegral` `restrict` `fst` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `ProbabilityTheory.Kernel` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `Prod.instMeasurableSpace` `SProd.sprod` `Set.instSProd`	—	`disintegrate` `condKernel.instIsCondKernel` `compProd_apply_prod` `instSFiniteFstOfProd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `instIsMarkovKernelCondKernel`
`setLIntegral_condKernel_univ_left` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `fst` `restrict` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`setLIntegral_condKernel` `MeasurableSet.univ` `restrict_univ`
`setLIntegral_condKernel_univ_right` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `restrict` `fst` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `ProbabilityTheory.Kernel.instFunLike` `condKernel` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`setLIntegral_condKernel` `MeasurableSet.univ` `restrict_univ`

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_condKernel` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instMeasurableSpace` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	`MeasureTheory.integral` `Kernel.fst` `Kernel.condKernel`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `integral_compProd` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`lintegral_condKernel` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `Kernel.condKernel`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `Kernel.lintegral_compProd` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`lintegral_condKernel_mem` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Kernel.condKernel` `Set.preimage`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `Kernel.compProd_apply` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`setIntegral_condKernel` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Kernel.fst` `Kernel.condKernel`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `setIntegral_compProd` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`setIntegral_condKernel_univ_left` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	`MeasureTheory.integral` `Kernel.fst` `MeasureTheory.Measure.restrict` `Kernel.condKernel`	—	`setIntegral_condKernel` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`
`setIntegral_condKernel_univ_right` 📖	mathematical	`MeasurableSet` `MeasureTheory.IntegrableOn` `Prod.instMeasurableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Kernel.fst` `Kernel.condKernel`	—	`setIntegral_condKernel` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`
`setLIntegral_condKernel` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `Kernel.condKernel` `SProd.sprod` `Set` `Set.instSProd`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `Kernel.setLIntegral_compProd` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`setLIntegral_condKernel_eq_measure_prod` 📖	mathematical	`MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Prod.instMeasurableSpace` `Kernel.condKernel` `SProd.sprod` `Set.instSProd`	—	`Kernel.disintegrate` `Kernel.condKernel.instIsCondKernel` `Kernel.compProd_apply_prod` `Kernel.IsSFiniteKernel.fst` `Kernel.IsFiniteKernel.isSFiniteKernel` `IsZeroOrMarkovKernel.isFiniteKernel` `IsMarkovKernel.IsZeroOrMarkovKernel` `Kernel.instIsMarkovKernelCondKernel`
`setLIntegral_condKernel_univ_left` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `MeasureTheory.Measure.restrict` `Kernel.condKernel` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`setLIntegral_condKernel` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`
`setLIntegral_condKernel_univ_right` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `MeasurableSet`	`MeasureTheory.lintegral` `MeasureTheory.Measure.restrict` `DFunLike.coe` `Kernel` `MeasureTheory.Measure` `Kernel.instFunLike` `Kernel.fst` `Kernel.condKernel` `SProd.sprod` `Set` `Set.instSProd` `Set.univ`	—	`setLIntegral_condKernel` `MeasurableSet.univ` `MeasureTheory.Measure.restrict_univ`

---

← Back to Index