Documentation Verification Report

Poisson

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

Statistics

Metric	Count
Definitions `poissonMeasure`, `poissonPMF`, `poissonPMFReal`	3
Theorems `isProbabilityMeasurePoisson`, `measurable_poissonPMFReal`, `poissonPMFRealSum`, `poissonPMFReal_nonneg`, `poissonPMFReal_pos`, `stronglyMeasurable_poissonPMFReal`	6
Total	9

ProbabilityTheory

Definitions

Name	Category	Theorems
`poissonMeasure` 📖	CompOp	1 math math: `isProbabilityMeasurePoisson`
`poissonPMF` 📖	CompOp	—
`poissonPMFReal` 📖	CompOp	5 math math: `stronglyMeasurable_poissonPMFReal`, `measurable_poissonPMFReal`, `poissonPMFReal_pos`, `poissonPMFRealSum`, `poissonPMFReal_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProbabilityMeasurePoisson` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Nat.instMeasurableSpace` `poissonMeasure`	—	`PMF.toMeasure.isProbabilityMeasure`
`measurable_poissonPMFReal` 📖	mathematical	—	`Measurable` `Real` `Nat.instMeasurableSpace` `Real.measurableSpace` `poissonPMFReal`	—	`measurable_from_nat`
`poissonPMFRealSum` 📖	mathematical	—	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `poissonPMFReal` `Real.instOne` `SummationFilter.unconditional`	—	`hasSum_mul_left_iff` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Real.exp_ne_zero` `mul_one` `mul_div_assoc` `Real.exp_neg` `mul_assoc` `div_eq_mul_inv` `div_self` `one_mul` `Real.exp_eq_exp_ℝ` `NormedSpace.expSeries_div_hasSum_exp` `RCLike.charZero_rclike` `Real.instCompleteSpace`
`poissonPMFReal_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `poissonPMFReal`	—	`Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `Real.exp_pos` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `NNReal.coe_nonneg` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos`
`poissonPMFReal_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`Real` `Real.instLT` `Real.instZero` `poissonPMFReal`	—	`poissonPMFReal.eq_1` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Real.exp_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.nnreal_coe_pos` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos`
`stronglyMeasurable_poissonPMFReal` 📖	mathematical	—	`MeasureTheory.StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Nat.instMeasurableSpace` `poissonPMFReal`	—	`stronglyMeasurable_iff_measurable` `EMetricSpace.metrizableSpace` `Real.borelSpace` `instSecondCountableTopologyReal` `measurable_poissonPMFReal`

---

← Back to Index