Theorems · Theorem · sequences and series
Stirling.sqrt_pi_le_stirlingSeq
∀ {n : ℕ}, n ≠ 0 → √Real.pi ≤ Stirling.stirlingSeq nThe Stirling sequence is bounded below by √π, for all positive naturals. Note that this bound
holds for all n > 0, rather than for sufficiently large n: it is effective.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 279 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Real.pistatement and proof · cited by 1,774
- Filter.Tendsto.compproof · cited by 560
- Real.sqrtstatement and proof · cited by 545
- Stirling.stirlingSeqstatement and proof · cited by 22
- Filter.tendsto_add_atTop_natproof · cited by 19
- Antitone.le_of_tendstoproof · cited by 7
- Stirling.stirlingSeq'_antitoneproof · cited by 2
- Stirling.tendsto_stirlingSeq_sqrt_piproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- Stirling.le_factorial_stirlingproof · cited by 1