Theorems · Theorem · probability

ProbabilityTheory.tendsto_choose_mul_pow_atTop

∀ {p : ℕ → ℝ} {r : ℝ} (k : ℕ),
  Filter.Tendsto (fun n => ↑n * p n) Filter.atTop (nhds r) →
    Filter.Tendsto (fun n => ↑(n.choose k) * p n ^ k) Filter.atTop (nhds (r ^ k / ↑k.factorial))

Defined in: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm
Cited by: 1 results in Mathlib
Foundations: Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites23

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
nhdsstatement and proof · cited by 5,554
mul_oneproof · cited by 3,885
Filter.Tendstostatement and proof · cited by 3,814
one_mulproof · cited by 2,841
Filter.atTopstatement and proof · cited by 2,405
one_ne_zeroproof · cited by 885
div_eq_mul_invproof · cited by 715
ne_of_gtproof · cited by 637
div_oneproof · cited by 629
Nat.factorialstatement and proof · cited by 616
Nat.choosestatement and proof · cited by 494

Cited by1

Results whose statement or proof uses this declaration.

ProbabilityTheory.tendsto_choose_mul_pow_of_tendsto_mul_atTopproof · cited by 1