Documentation Verification Report

Pi

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

Statistics

Metric	Count
Definitions	0
Theorems `eval`, `of_eval`, `eval`, `fst`, `of_eval`, `of_fst_snd`, `snd`, `eval_integral`, `integrable_pi_iff`, `memLp_pi_iff`, `memLp_prod_iff`	11
Total	11

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_integral` 📖	mathematical	`CompleteSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Integrable` `UniformSpace.toTopologicalSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Pi.normedAddCommGroup` `Pi.normedSpace` `Real` `Real.normedField`	—	`ContinuousLinearMap.integral_comp_comm` `Pi.complete` `Integrable.of_eval`
`integrable_pi_iff` 📖	mathematical	—	`Integrable` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—
`memLp_pi_iff` 📖	mathematical	—	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Pi.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.topologicalSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`LipschitzWith.comp_memLp` `LipschitzWith.eval` `Finset.sum_apply` `Finset.sum_congr` `Finset.sum_pi_single` `memLp_finset_sum'` `Pi.continuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Isometry.lipschitz` `Isometry.single` `Pi.single_zero`
`memLp_prod_iff` 📖	mathematical	—	`MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Prod.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `instTopologicalSpaceProd` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`LipschitzWith.comp_memLp` `LipschitzWith.prod_fst` `LipschitzWith.prod_snd` `add_zero` `zero_add` `MemLp.add` `Prod.continuousAdd` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Isometry.lipschitz` `Isometry.inl` `Isometry.inr`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval` 📖	—	`MeasureTheory.Integrable` `Pi.topologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	—	`MeasureTheory.integrable_pi_iff`
`of_eval` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Pi.topologicalSpace` `Pi.seminormedAddGroup`	—	`MeasureTheory.integrable_pi_iff`

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval` 📖	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Pi.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `Pi.topologicalSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`MeasureTheory.memLp_pi_iff`
`fst` 📖	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Prod.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `instTopologicalSpaceProd` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`MeasureTheory.memLp_prod_iff`
`of_eval` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Pi.seminormedAddGroup` `Pi.topologicalSpace`	—	`MeasureTheory.memLp_pi_iff`
`of_fst_snd` 📖	mathematical	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`Prod.seminormedAddGroup` `instTopologicalSpaceProd`	—	`MeasureTheory.memLp_prod_iff`
`snd` 📖	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `Prod.seminormedAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `instTopologicalSpaceProd` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	—	`MeasureTheory.memLp_prod_iff`

---

← Back to Index