Theorems · Definition · sequences and series
Stirling.stirlingSeq
ℕ → ℝ
Define stirlingSeq n as $\frac{n!}{\sqrt{2n}(\frac{n}{e})^n}$.
Stirling's formula states that this sequence has limit $\sqrt(π)$.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Real.expproof · cited by 871
- Nat.factorialproof · cited by 616
- Real.sqrtproof · cited by 545
Cited by22
Results whose statement or proof uses this declaration.
- Stirling.log_stirlingSeq_sdiff_hasSumstatement and proof · cited by 4
- Stirling.log_stirlingSeq_sdiff_lestatement and proof · cited by 3
- Stirling.stirlingSeq'_antitonestatement · cited by 2
- Stirling.stirlingSeq'_posstatement · cited by 2
- Stirling.stirlingSeq_onestatement · cited by 2
- Stirling.stirlingSeq_zerostatement · cited by 2
- Stirling.tendsto_stirlingSeq_sqrt_pistatement and proof · cited by 2
- Stirling.log_stirlingSeq_bounded_by_constantstatement and proof · cited by 1
- Stirling.log_stirlingSeq_formulastatement · cited by 1
- Stirling.log_stirlingSeq_sdiff_le_geo_sumstatement · cited by 1
- Stirling.second_wallis_limitstatement and proof · cited by 1
- Stirling.sqrt_pi_le_stirlingSeqstatement and proof · cited by 1