English
The topological sum term_tsum is continuous on [1,∞).
Русский
Верхняя сумма term_tsum непрерывна на [1,∞).
LaTeX
$$$$\\\\text{ContinuousOn} \\,\\\\operatorname{term\\_tsum} \\\\left([1,\\\\infty)\\\\right)$$$$
Lean4
theorem continuousOn_term_tsum : ContinuousOn term_tsum (Ici 1) := by
-- We use dominated convergence, using `fun n ↦ term n 1` as our uniform bound (since `term` is
-- monotone decreasing in `s`.)
refine continuousOn_tsum (fun i ↦ continuousOn_term _) term_tsum_one.summable (fun n s hs ↦ ?_)
rw [term, term, norm_of_nonneg]
· simp_rw [intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc (fun x hx ↦ ?_)
· exact (term_welldef n.succ_pos (zero_lt_one.trans_le hs)).1
· exact (term_welldef n.succ_pos zero_lt_one).1
· have : 1 ≤ x := le_trans (by simp) hx.1.le
gcongr
· exact sub_nonneg.mpr hx.1.le
· assumption
· exact hs
· rw [intervalIntegral.integral_of_le (by linarith)]
refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ div_nonneg ?_ (rpow_nonneg ?_ _))
all_goals linarith [hx.1]
