Documentation Verification Report

Geometric

📁 Source: Mathlib/Probability/Distributions/Geometric.lean

Statistics

Metric	Count
Definitions `geometricMeasure`, `geometricPMF`, `geometricPMFReal`	3
Theorems `geometricPMFRealSum`, `geometricPMFReal_nonneg`, `geometricPMFReal_pos`, `isProbabilityMeasureGeometric`, `isProbabilityMeasure_geometricMeasure`, `measurable_geometricPMFReal`, `stronglyMeasurable_geometricPMFReal`	7
Total	10

ProbabilityTheory

Definitions

Name	Category	Theorems
`geometricMeasure` 📖	CompOp	2 math math: `isProbabilityMeasure_geometricMeasure`, `isProbabilityMeasureGeometric`
`geometricPMF` 📖	CompOp	—
`geometricPMFReal` 📖	CompOp	5 math math: `stronglyMeasurable_geometricPMFReal`, `measurable_geometricPMFReal`, `geometricPMFReal_nonneg`, `geometricPMFReal_pos`, `geometricPMFRealSum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`geometricPMFRealSum` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne`	`HasSum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `geometricPMFReal` `SummationFilter.unconditional`	—	`hasSum_geometric_of_lt_one` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_lt_self` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `div_self` `LT.lt.ne'` `inv_mul_eq_div` `sub_sub_cancel` `hasSum_mul_right_iff` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal`
`geometricPMFReal_nonneg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne`	`geometricPMFReal`	—	`geometricPMFReal.eq_1` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `le_of_lt`
`geometricPMFReal_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`geometricPMFReal`	—	`geometricPMFReal.eq_1` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass`
`isProbabilityMeasureGeometric` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne`	`MeasureTheory.IsProbabilityMeasure` `Nat.instMeasurableSpace` `geometricMeasure`	—	`isProbabilityMeasure_geometricMeasure`
`isProbabilityMeasure_geometricMeasure` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instOne`	`MeasureTheory.IsProbabilityMeasure` `Nat.instMeasurableSpace` `geometricMeasure`	—	`PMF.toMeasure.isProbabilityMeasure`
`measurable_geometricPMFReal` 📖	mathematical	—	`Measurable` `Real` `Nat.instMeasurableSpace` `Real.measurableSpace` `geometricPMFReal`	—	`measurable_from_nat`
`stronglyMeasurable_geometricPMFReal` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Nat.instMeasurableSpace` `geometricPMFReal`	—	`stronglyMeasurable_iff_measurable` `EMetricSpace.metrizableSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `measurable_geometricPMFReal`

---

← Back to Index