Theorems · Theorem · sequences and series
Stirling.log_stirlingSeq_sdiff_hasSum
∀ (m : ℕ),
HasSum (fun k => 1 / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ (k + 1))
(Real.log (Stirling.stirlingSeq (m + 1)) - Real.log (Stirling.stirlingSeq (m + 2)))The sequence log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) has the series expansion
∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1)).
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites44
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
- TopologicalSpaceproof · cited by 24,529
- AddCommMonoidproof · cited by 12,281
- Finset.sumproof · cited by 5,195
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Nat.cast_oneproof · cited by 2,501
- SummationFilter.unconditionalstatement and proof · cited by 2,068
- Nat.cast_zeroproof · cited by 1,870
- Finset.rangeproof · cited by 1,341
- le_of_ltproof · cited by 1,175
- Real.logstatement and proof · cited by 939
Cited by4
Results whose statement or proof uses this declaration.
- Stirling.log_stirlingSeq_sdiff_leproof · cited by 3
- Stirling.log_stirlingSeq'_antitoneproof · cited by 1
- Stirling.log_stirlingSeq_sdiff_le_geo_sumproof · cited by 1
- Stirling.log_stirlingSeq_diff_hasSumproof · cited by 0