Theorems · Theorem · number theory
ZetaAsymptotics.term_tsum_one
HasSum (fun n => ZetaAsymptotics.term (n + 1) 1) (1 - Real.eulerMascheroniConstant)
The topological sum of ZetaAsymptotics.term (n + 1) 1 over all n : ℕ is 1 - γ. This is
proved by directly evaluating the sum of the first N terms and using the limit definition of γ.
- Defined in
- Mathlib.NumberTheory.Harmonic.ZetaAsymp
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 275 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- Nat.cast_oneproof · cited by 2,501
- Filter.atTopproof · cited by 2,405
- SummationFilter.unconditionalstatement · cited by 2,068
- Real.logproof · cited by 939
- Nat.cast_addproof · cited by 586
- Filter.Tendsto.compproof · cited by 560
- Filter.Eventually.of_forallproof · cited by 526
- HasSumstatement · cited by 518
- tendsto_const_nhdsproof · cited by 330
Cited by2
Results whose statement or proof uses this declaration.
- ZetaAsymptotics.continuousOn_termTSumproof · cited by 2
- ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_rightproof · cited by 1