Documentation Verification Report

Pi

📁 Source: Mathlib/MeasureTheory/Integral/Pi.lean

Statistics

Metric	Count
Definitions	0
Theorems `fin_nat_prod`, `fintype_prod`, `fintype_prod_dep`, `integrable_comp_eval`, `integral_comp_eval`, `integral_fin_nat_prod_eq_prod`, `integral_fin_nat_prod_volume_eq_prod`, `integral_fintype_prod_eq_pow`, `integral_fintype_prod_eq_prod`, `integral_fintype_prod_volume_eq_pow`, `integral_fintype_prod_volume_eq_prod`	11
Total	11

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integrable_comp_eval` 📖	mathematical	`IsFiniteMeasure` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`MeasurableSpace.pi` `Measure.pi`	—	`Integrable.comp_measurable` `IsScalarTower.right` `Measure.pi_map_eval` `IsFiniteMeasure.toSigmaFinite` `Integrable.smul_measure` `ENNReal.prod_ne_top` `measure_ne_top` `measurable_pi_apply`
`integral_comp_eval` 📖	mathematical	`IsProbabilityMeasure` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`integral` `MeasurableSpace.pi` `Measure.pi`	—	`MeasurePreserving.map_eq` `measurePreserving_eval` `integral_map` `Measurable.aemeasurable` `measurable_pi_apply`
`integral_fin_nat_prod_eq_prod` 📖	mathematical	`SigmaFinite`	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasurableSpace.pi` `Measure.pi` `Fin.fintype` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `integral_const` `RCLike.toCompleteSpace` `Measure.pi_empty_univ` `one_smul` `MeasurePreserving.integral_comp'` `MeasurePreserving.symm` `measurePreserving_piFinSuccAbove` `Fin.prod_univ_succ` `Fin.succAbove_zero` `Fin.insertNth_zero` `Fin.cons_succ` `Fin.cons_zero` `integral_prod_mul` `instSFiniteOfSigmaFinite` `Measure.pi.sigmaFinite`
`integral_fin_nat_prod_volume_eq_prod` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureSpace.pi` `Fin.fintype` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`integral_fin_nat_prod_eq_prod`
`integral_fintype_prod_eq_pow` 📖	mathematical	—	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasurableSpace.pi` `Measure.pi` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Fintype.card`	—	`integral_fintype_prod_eq_prod` `Finset.prod_const` `Fintype.card.eq_1`
`integral_fintype_prod_eq_prod` 📖	mathematical	`SigmaFinite`	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasurableSpace.pi` `Measure.pi` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`MeasurePreserving.integral_comp'` `measurePreserving_piCongrLeft` `Equiv.prod_comp` `Finset.prod_congr` `MeasurableEquiv.coe_piCongrLeft` `Equiv.piCongrLeft_apply_apply` `integral_fin_nat_prod_eq_prod`
`integral_fintype_prod_volume_eq_pow` 📖	mathematical	—	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureSpace.toMeasurableSpace` `MeasureSpace.pi` `MeasureSpace.volume` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Fintype.card`	—	`integral_fintype_prod_eq_pow`
`integral_fintype_prod_volume_eq_prod` 📖	mathematical	`SigmaFinite` `MeasureSpace.toMeasurableSpace` `MeasureSpace.volume`	`integral` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureSpace.pi` `Finset.prod` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NormedField.toField` `Finset.univ`	—	`integral_fintype_prod_eq_prod`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fin_nat_prod` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing`	`MeasurableSpace.pi` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.univ` `Fin.fintype` `MeasureTheory.Measure.pi`	—	`Finset.prod_congr` `Finset.univ_eq_empty` `Fin.isEmpty'` `MeasureTheory.Measure.pi_empty_univ` `MeasureTheory.MeasurePreserving.symm` `MeasureTheory.measurePreserving_piFinSuccAbove` `MeasureTheory.MeasurePreserving.integrable_comp_emb` `MeasurableEquiv.measurableEmbedding` `Fin.prod_univ_succ` `Fin.succAbove_zero` `Fin.insertNth_zero` `mul_prod`
`fintype_prod` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing`	`MeasurableSpace.pi` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.univ` `MeasureTheory.Measure.pi`	—	`fintype_prod_dep`
`fintype_prod_dep` 📖	mathematical	`MeasureTheory.SigmaFinite` `MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing`	`MeasurableSpace.pi` `Finset.prod` `CommRing.toCommMonoid` `NormedCommRing.toCommRing` `Finset.univ` `MeasureTheory.Measure.pi`	—	`MeasureTheory.MeasurePreserving.integrable_comp_emb` `MeasureTheory.measurePreserving_piCongrLeft` `MeasurableEquiv.measurableEmbedding` `Equiv.prod_comp` `MeasurableEquiv.coe_piCongrLeft` `Finset.prod_congr` `Equiv.piCongrLeft_apply_apply` `fin_nat_prod`

---

← Back to Index