Documentation Verification Report

PoissonLimitThm

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

Statistics

Metric	Count
Definitions	0
Theorems `binomial_tendsto_poissonPMFReal_atTop`, `tendsto_choose_mul_pow_atTop`, `tendsto_choose_mul_pow_of_tendsto_mul_atTop`, `tendsto_zero_of_tendsto_mul_atTop`	4
Total	4

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`binomial_tendsto_poissonPMFReal_atTop` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `NNReal.instPartialOrder` `NNReal.instOne` `Filter.Tendsto` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NNReal.instSemiring` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Filter.atTop` `Nat.instPreorder` `nhds` `NNReal.instTopologicalSpace`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `PMF` `PMF.instFunLike` `PMF.binomial` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `MeasureTheory.Measure` `Nat.instMeasurableSpace` `Set` `MeasureTheory.Measure.instFunLike` `poissonMeasure` `Set.instSingletonSet`	—	`poissonMeasure_singleton` `ENNReal.tendsto_ofReal` `tendsto_choose_mul_pow_of_tendsto_mul_atTop` `NNReal.coe_natCast` `Filter.Tendsto.congr'` `instIsDirectedOrder` `StarOrderedRing.toIsOrderedRing` `Nat.instStarOrderedRing` `instArchimedeanNat` `PMF.binomial_apply_of_le`
`tendsto_choose_mul_pow_atTop` 📖	mathematical	`Filter.Tendsto` `Real` `Real.instMul` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Tendsto` `Real` `Real.instMul` `Real.instNatCast` `Nat.choose` `Monoid.toPow` `Real.instMonoid` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Nat.factorial`	—	`Asymptotics.IsEquivalent.mul` `isEquivalent_choose` `Asymptotics.IsEquivalent.refl` `Filter.EventuallyEq.isEquivalent` `Filter.EventuallyEq.of_eq` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Nat.factorial_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Asymptotics.IsEquivalent.tendsto_nhds_iff` `div_eq_mul_inv` `Filter.Tendsto.mul_const` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `Filter.Tendsto.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring`
`tendsto_choose_mul_pow_of_tendsto_mul_atTop` 📖	mathematical	`Filter.Tendsto` `Real` `Real.instMul` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Tendsto` `Real` `Real.instMul` `Real.instNatCast` `Nat.choose` `Monoid.toPow` `Real.instMonoid` `Real.instSub` `Real.instOne` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.exp` `Real.instNeg` `Nat.factorial`	—	`mul_div_assoc` `mul_comm` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_choose_mul_pow_atTop` `Nat.instAtLeastTwoHAddOfNat` `Filter.Tendsto.eventually` `tendsto_zero_of_tendsto_mul_atTop` `Iio_mem_nhds` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `pow_sub₀` `Filter.Tendsto.congr'` `Filter.EventuallyEq.symm` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Real.exp_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Real.tendsto_one_add_pow_exp_of_tendsto` `mul_neg` `IsSemitopologicalRing.toContinuousNeg` `IsTopologicalRing.toIsSemitopologicalRing` `Filter.Tendsto.neg` `Filter.Tendsto.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `Filter.Tendsto.pow` `sub_zero` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `tendsto_const_nhds` `one_pow` `NeZero.charZero_one`
`tendsto_zero_of_tendsto_mul_atTop` 📖	mathematical	`Filter.Tendsto` `Real` `Real.instMul` `Real.instNatCast` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Filter.Tendsto` `Real` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `StarOrderedRing.toIsOrderedRing` `Nat.instStarOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `MulZeroClass.mul_zero` `Filter.Tendsto.congr'` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `tendsto_one_div_atTop_nhds_zero_nat` `NNRat.instContinuousSMulOfIsScalarTowerOfRat` `IsScalarTower.nnrat` `Rat.instCharZero` `NNRat.instContinuousSMulRatReal`

---

← Back to Index