English
ContinuousOn term_tsum on [1, ∞).
Русский
Непрерывность на отрезке [1, ∞) выражения term_tsum.
LaTeX
$$$\\\\text{ContinuousOn} \\,\\\\operatorname{term\\_tsum} \\, [1,\\\\infty)$$$
Lean4
/-- 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 `γ`.
-/
theorem term_tsum_one : HasSum (fun n ↦ term (n + 1) 1) (1 - γ) :=
by
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) 1)]
change Tendsto (fun N ↦ term_sum 1 N) atTop _
simp_rw [term_sum_one, sub_eq_neg_add]
refine Tendsto.add ?_ tendsto_const_nhds
have := (tendsto_eulerMascheroniSeq'.comp (tendsto_add_atTop_nat 1)).neg
refine this.congr' (Eventually.of_forall (fun n ↦ ?_))
simp_rw [Function.comp_apply, eulerMascheroniSeq', reduceCtorEq, if_false]
push_cast
abel
