Theorems · Theorem · sequences and series
Stirling.second_wallis_limit
∀ (a : ℝ),
a ≠ 0 →
Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds a) →
Filter.Tendsto Real.Wallis.W Filter.atTop (nhds (a ^ 2 / 2))Suppose the sequence stirlingSeq (defined above) has the limit a ≠ 0.
Then the Wallis sequence W n has limit a^2 / 2.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
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
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.atTopstatement and proof · cited by 2,405
- one_divproof · cited by 624
- Filter.Tendsto.compproof · cited by 560
- pow_ne_zeroproof · cited by 208
- Filter.tendsto_idproof · cited by 180
- Filter.Tendsto.congr'proof · cited by 154
- Filter.eventually_atTopproof · cited by 112
- Filter.Tendsto.mulproof · cited by 74
- two_posproof · cited by 68
Cited by1
Results whose statement or proof uses this declaration.
- Stirling.tendsto_stirlingSeq_sqrt_piproof · cited by 2