Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `poissonMeasure`, `poissonPMF`, `poissonPMFReal`	3
Theorems `hasSum_integral_poissonMeasure`, `hasSum_one_poissonMeasure`, `integrable_poissonMeasure_iff`, `integral_poissonMeasure`, `integral_poissonMeasure'`, `isProbabilityMeasure_poissonMeasure`, `measurable_poissonPMFReal`, `poissonMeasure_real_singleton`, `poissonMeasure_real_singleton_pos`, `poissonMeasure_singleton`, `poissonPMFRealSum`, `poissonPMFReal_nonneg`, `poissonPMFReal_ofReal_eq_poissonPMF`, `poissonPMFReal_pos`, `stronglyMeasurable_poissonPMFReal`	15
Total	18

ProbabilityTheory

Definitions

Name	Category	Theorems
`poissonMeasure` 📖	CompOp	9 math math: `hasSum_integral_poissonMeasure`, `isProbabilityMeasure_poissonMeasure`, `poissonMeasure_singleton`, `integral_poissonMeasure`, `poissonMeasure_real_singleton`, `poissonMeasure_real_singleton_pos`, `binomial_tendsto_poissonPMFReal_atTop`, `integrable_poissonMeasure_iff`, `integral_poissonMeasure'`
`poissonPMF` 📖	CompOp	1 math math: `poissonPMFReal_ofReal_eq_poissonPMF`
`poissonPMFReal` 📖	CompOp	6 math math: `poissonPMFReal_ofReal_eq_poissonPMF`, `stronglyMeasurable_poissonPMFReal`, `measurable_poissonPMFReal`, `poissonPMFReal_pos`, `poissonPMFRealSum`, `poissonPMFReal_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasSum_integral_poissonMeasure` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Nat.instMeasurableSpace` `poissonMeasure`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instNatCast` `Nat.factorial` `MeasureTheory.integral` `Nat.instMeasurableSpace` `poissonMeasure` `SummationFilter.unconditional`	—	`ENNReal.toReal_ofReal` `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` `MeasureTheory.hasSum_integral_sum_dirac` `instCountableNat` `Nat.instMeasurableSingletonClass` `integrable_poissonMeasure_iff`
`hasSum_one_poissonMeasure` 📖	mathematical	—	`HasSum` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial` `Real.instOne` `SummationFilter.unconditional`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `mul_div_assoc` `instIsTopologicalRingReal` `neg_add_cancel` `Real.exp_zero` `HasSum.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `NormedSpace.expSeries_div_hasSum_exp` `RCLike.charZero_rclike` `Real.instCompleteSpace`
`integrable_poissonMeasure_iff` 📖	mathematical	—	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Nat.instMeasurableSpace` `poissonMeasure` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `Real.instMul` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	—	`poissonMeasure.eq_1` `IsScalarTower.right` `MeasureTheory.integrable_sum_dirac_iff` `instCountableNat` `Nat.instMeasurableSingletonClass` `ENNReal.toReal_ofReal` `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`
`integral_poissonMeasure` 📖	mathematical	—	`MeasureTheory.integral` `Nat.instMeasurableSpace` `poissonMeasure` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`poissonMeasure.eq_1` `IsScalarTower.right` `MeasureTheory.integral_sum_dirac` `instCountableNat` `Nat.instMeasurableSingletonClass` `ENNReal.toReal_ofReal` `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`
`integral_poissonMeasure'` 📖	mathematical	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Nat.instMeasurableSpace` `poissonMeasure`	`MeasureTheory.integral` `Nat.instMeasurableSpace` `poissonMeasure` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instNatCast` `Nat.factorial` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_poissonMeasure`
`isProbabilityMeasure_poissonMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `Nat.instMeasurableSpace` `poissonMeasure`	—	`HasSum.isProbabilityMeasure_sum_dirac` `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` `hasSum_one_poissonMeasure`
`measurable_poissonPMFReal` 📖	mathematical	—	`Measurable` `Real` `Nat.instMeasurableSpace` `Real.measurableSpace` `poissonPMFReal`	—	`measurable_from_nat`
`poissonMeasure_real_singleton` 📖	mathematical	—	`MeasureTheory.Measure.real` `Nat.instMeasurableSpace` `poissonMeasure` `Set` `Set.instSingletonSet` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`MeasureTheory.measureReal_def` `poissonMeasure_singleton` `ENNReal.toReal_ofReal` `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`
`poissonMeasure_real_singleton_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instZero`	`Real` `Real.instLT` `Real.instZero` `MeasureTheory.Measure.real` `Nat.instMeasurableSpace` `poissonMeasure` `Set` `Set.instSingletonSet`	—	`poissonMeasure_real_singleton` `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`
`poissonMeasure_singleton` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Nat.instMeasurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `poissonMeasure` `Set.instSingletonSet` `ENNReal.ofReal` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instMul` `Real.exp` `Real.instNeg` `NNReal.toReal` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`poissonMeasure.eq_1` `IsScalarTower.right` `MeasureTheory.Measure.sum_smul_dirac_singleton` `Nat.instMeasurableSingletonClass`
`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_ofReal_eq_poissonPMF` 📖	mathematical	—	`ENNReal.ofReal` `poissonPMFReal` `DFunLike.coe` `PMF` `ENNReal` `PMF.instFunLike` `poissonPMF`	—	—
`poissonPMFReal_pos` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instZero`	`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