Documentation Verification Report

FiniteMeasurePi

📁 Source: Mathlib/MeasureTheory/Measure/FiniteMeasurePi.lean

Statistics

Metric	Count
Definitions `pi`, `pi`	2
Theorems `mass_pi`, `pi_map_pi`, `pi_pi`, `toMeasure_pi`, `continuous_pi`, `pi_pi`, `toMeasure_pi`	7
Total	9

MeasureTheory.FiniteMeasure

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	4 math math: `pi_pi`, `pi_map_pi`, `toMeasure_pi`, `mass_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mass_pi` 📖	mathematical	—	`mass` `MeasurableSpace.pi` `pi` `Finset.prod` `NNReal` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `Finset.univ`	—	`Finset.prod_congr` `Set.pi_univ` `pi_pi`
`pi_map_pi` 📖	mathematical	`AEMeasurable` `toMeasure`	`map` `MeasurableSpace.pi` `pi`	—	`MeasureTheory.Measure.pi_map_pi` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.Measure.isFiniteMeasure_map` `isFiniteMeasure`
`pi_pi` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.FiniteMeasure` `MeasurableSpace.pi` `Set` `NNReal` `instFunLike` `pi` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `Finset.univ`	—	`MeasureTheory.Measure.pi_pi` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `isFiniteMeasure` `ENNReal.toNNReal_prod` `Finset.prod_congr`
`toMeasure_pi` 📖	mathematical	—	`toMeasure` `MeasurableSpace.pi` `pi` `MeasureTheory.Measure.pi`	—	—

MeasureTheory.ProbabilityMeasure

Definitions

Name	Category	Theorems
`pi` 📖	CompOp	3 math math: `continuous_pi`, `pi_pi`, `toMeasure_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_pi` 📖	mathematical	`SecondCountableTopology` `TopologicalSpace.PseudoMetrizableSpace` `OpensMeasurableSpace`	`Continuous` `MeasureTheory.ProbabilityMeasure` `MeasurableSpace.pi` `Pi.topologicalSpace` `instTopologicalSpace` `Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `pi`	—	`Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `continuous_iff_continuousAt` `Set.pi_inter_distrib` `MeasurableSet.inter` `null_frontier_inter` `IsPiSystem.tendsto_probabilityMeasure_of_tendsto_of_mem` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `FirstCountableTopology.nhds_generated_countable` `TopologicalSpace.instFirstCountableTopologyForallOfCountable` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `MeasurableSet.univ_pi` `Metric.isOpen_iff` `MeasureTheory.exists_null_frontier_thickening` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `measurableSet_ball` `Metric.thickening_singleton` `IsOpen.mem_nhds` `isOpen_set_pi` `Set.finite_univ` `dist_self` `Set.pi_mono'` `Metric.ball_subset_ball` `LT.lt.le` `subset_refl` `Set.instReflSubset` `ball_pi` `pi_pi` `tendsto_finset_prod` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring` `tendsto_measure_of_null_frontier_of_tendsto` `instHasOuterApproxClosedOfPseudoMetrizableSpace` `Filter.Tendsto.apply_nhds`
`pi_pi` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.ProbabilityMeasure` `MeasurableSpace.pi` `Set` `NNReal` `instFunLike` `pi` `Set.pi` `Set.univ` `Finset.prod` `CommSemiring.toCommMonoid` `instCommSemiringNNReal` `Finset.univ`	—	`MeasureTheory.Measure.pi_pi` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `instIsProbabilityMeasureToMeasure` `ENNReal.toNNReal_prod` `Finset.prod_congr`
`toMeasure_pi` 📖	mathematical	—	`toMeasure` `MeasurableSpace.pi` `pi` `MeasureTheory.Measure.pi`	—	—

---

← Back to Index