Documentation Verification Report

Integration

📁 Source: Mathlib/Probability/Independence/Integration.lean

Statistics

Metric	Count
Definitions	0
Theorems `integrable_left_of_integrable_mul`, `integrable_mul`, `integrable_right_of_integrable_mul`, `integral_comp_mul_comp`, `integral_fun_comp_mul_comp`, `integral_fun_mul_eq_mul_integral`, `integral_mul_eq_mul_integral`, `integral_fun_prod_comp`, `integral_fun_prod_eq_prod_integral`, `integral_prod_comp`, `integral_prod_eq_prod_integral`, `indepFun_iff_integral_comp_mul`, `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun`, `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'`, `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun''`, `lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace`, `lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator`, `lintegral_prod_eq_prod_lintegral_of_indepFun`	18
Total	18

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`indepFun_iff_integral_comp_mul` 📖	mathematical	`Measurable`	`IndepFun` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Pi.instMul` `Real.instMul`	—	`IndepFun.integral_comp_mul_comp` `Measurable.aemeasurable` `Measurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `instSecondCountableTopologyReal` `BorelSpace.opensMeasurable` `Real.borelSpace` `IndepFun_iff` `ENNReal.toReal_eq_toReal_iff'` `MeasureTheory.measure_ne_top` `ENNReal.mul_ne_top` `ENNReal.toReal_mul` `MeasureTheory.measureReal_def` `MeasureTheory.integral_indicator_one` `MeasurableSet.inter` `Set.inter_indicator_one` `Measurable.indicator` `measurable_one` `MeasureTheory.Integrable.indicator` `MeasureTheory.integrable_const` `Measurable.comp` `measurable_id`
`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace` `IndepFun`	`MeasureTheory.lintegral` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace` `measurable_iff_comap_le` `Measurable.of_comap_le` `le_rfl`
`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `IndepFun`	`MeasureTheory.lintegral` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.mul` `MeasureTheory.lintegral_congr_ae` `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun` `IndepFun.congr`
`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun''` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `IndepFun`	`MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'`
`lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `Indep` `Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Measurable.ennreal_induction` `lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator` `indepSets_of_indepSets_of_le_right` `Set.singleton_subset_iff` `Measurable.mono` `le_rfl` `left_distrib` `Distrib.leftDistribClass` `MeasureTheory.lintegral_add_left` `Measurable.mul` `ENNReal.instMeasurableMul₂` `ENNReal.mul_iSup` `MeasureTheory.lintegral_iSup` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasurableSet` `IndepSets` `setOf` `Set` `Set.instSingletonSet` `Measurable` `ENNReal` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.indicator` `instZeroENNReal`	—	`Measurable.ennreal_induction` `MeasureTheory.lintegral_indicator` `MeasurableSet.inter` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `mul_mul_mul_comm` `IndepSets_iff` `Set.mem_singleton` `Measurable.mono` `le_rfl` `right_distrib` `Distrib.rightDistribClass` `MeasureTheory.lintegral_add_left` `Measurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.indicator` `measurable_const` `ENNReal.iSup_mul` `MeasureTheory.lintegral_iSup` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid`
`lintegral_prod_eq_prod_lintegral_of_indepFun` 📖	mathematical	`iIndepFun` `ENNReal` `ENNReal.measurableSpace` `Measurable`	`MeasureTheory.lintegral` `Finset.prod` `CommSemiring.toCommMonoid` `ENNReal.instCommSemiring`	—	`iIndepFun.isProbabilityMeasure` `Finset.cons_induction` `MeasureTheory.lintegral_const` `MeasureTheory.IsProbabilityMeasure.measure_univ` `mul_one` `Finset.prod_cons` `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'` `Measurable.aemeasurable` `Finset.aemeasurable_prod` `ENNReal.instMeasurableMul₂` `IndepFun.symm` `iIndepFun.indepFun_finset_prod_of_notMem`

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_left_of_integrable_mul` 📖	—	`ProbabilityTheory.IndepFun` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `MeasureTheory.AEStronglyMeasurable` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff'` `MeasureTheory.AEStronglyMeasurable.enorm` `Filter.mp_mem` `Filter.univ_mem'` `MeasureTheory.hasFiniteIntegral_iff_enorm` `lt_top_iff_ne_top` `comp` `measurable_enorm` `ENNReal.top_mul` `ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun''` `enorm_mul` `NormedDivisionRing.toNormMulClass`
`integrable_mul` 📖	mathematical	`ProbabilityTheory.IndepFun` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing`	`Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing`	—	`comp` `measurable_enorm` `BorelSpace.opensMeasurable` `AEMeasurable.enorm` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `enorm_mul` `NormedDivisionRing.toNormMulClass` `ENNReal.mul_lt_top`
`integrable_right_of_integrable_mul` 📖	—	`ProbabilityTheory.IndepFun` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `NormedDivisionRing.toNormedRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `NormedRing.toRing` `MeasureTheory.AEStronglyMeasurable` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff'` `MeasureTheory.AEStronglyMeasurable.enorm` `Filter.mp_mem` `Filter.univ_mem'` `lt_top_iff_ne_top` `comp` `measurable_enorm` `ENNReal.mul_top` `ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun''` `enorm_mul` `NormedDivisionRing.toNormMulClass`
`integral_comp_mul_comp` 📖	mathematical	`ProbabilityTheory.IndepFun` `AEMeasurable` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MeasureTheory.Measure.map`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`integral_fun_comp_mul_comp`
`integral_fun_comp_mul_comp` 📖	mathematical	`ProbabilityTheory.IndepFun` `AEMeasurable` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MeasureTheory.Measure.map`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`comp₀` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `RCLike.borelSpace` `MeasureTheory.AEStronglyMeasurable.comp_aemeasurable` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `MulZeroClass.zero_mul` `MeasureTheory.integral_congr_ae` `MeasureTheory.integral_zero` `MulZeroClass.mul_zero` `MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun` `BorelSpace.opensMeasurable` `integrable_left_of_integrable_mul` `MeasureTheory.integral_map` `AEMeasurable.prodMk` `ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.AEStronglyMeasurable.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MeasureTheory.AEStronglyMeasurable.comp_fst` `MeasureTheory.AEStronglyMeasurable.comp_snd` `MeasureTheory.integral_prod_mul` `MeasureTheory.Measure.instSFiniteMap` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.integral_undef` `not_and_or` `integrable_mul`
`integral_fun_mul_eq_mul_integral` 📖	mathematical	`ProbabilityTheory.IndepFun` `RCLike.measurableSpace` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`integral_mul_eq_mul_integral`
`integral_mul_eq_mul_integral` 📖	mathematical	`ProbabilityTheory.IndepFun` `RCLike.measurableSpace` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing`	—	`integral_comp_mul_comp` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `RCLike.borelSpace` `aestronglyMeasurable_id` `BorelSpace.opensMeasurable` `secondCountable_of_proper` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real`

ProbabilityTheory.iIndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_fun_prod_comp` 📖	mathematical	`ProbabilityTheory.iIndepFun` `AEMeasurable` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MeasureTheory.Measure.map`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`isProbabilityMeasure` `MeasureTheory.integral_map` `aemeasurable_pi_lambda` `Finite.to_countable` `Finite.of_fintype` `ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map` `Finset.aestronglyMeasurable_fun_prod` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving` `MeasureTheory.Measure.quasiMeasurePreserving_eval` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.integral_fintype_prod_eq_prod`
`integral_fun_prod_eq_prod_integral` 📖	mathematical	`ProbabilityTheory.iIndepFun` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `FiniteDimensional.rclike_to_real` `RCLike.measurableSpace` `RCLike.borelSpace` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`MeasureTheory.integral` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`FiniteDimensional.rclike_to_real` `RCLike.borelSpace` `integral_fun_prod_comp` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `aestronglyMeasurable_id` `BorelSpace.opensMeasurable` `secondCountable_of_proper` `FiniteDimensional.proper_real`
`integral_prod_comp` 📖	mathematical	`ProbabilityTheory.iIndepFun` `AEMeasurable` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `MeasureTheory.Measure.map`	`MeasureTheory.integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`Finset.prod_apply` `Finset.prod_congr` `integral_fun_prod_comp`
`integral_prod_eq_prod_integral` 📖	mathematical	`ProbabilityTheory.iIndepFun` `MeasureTheory.MeasureSpace.toMeasurableSpace` `measureSpaceOfInnerProductSpace` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.toInnerProductSpaceReal` `FiniteDimensional.rclike_to_real` `RCLike.measurableSpace` `RCLike.borelSpace` `MeasureTheory.AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing`	`MeasureTheory.integral` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `Finset.prod` `Pi.commMonoid` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`FiniteDimensional.rclike_to_real` `RCLike.borelSpace` `integral_prod_comp` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `aestronglyMeasurable_id` `BorelSpace.opensMeasurable` `secondCountable_of_proper` `FiniteDimensional.proper_real`

---

← Back to Index