English
For every n, the map s ↦ term(n+1,s) is continuous on [1,∞).
Русский
Для каждого n отображение s ↦ term(n+1,s) непрерывно на [1,∞).
LaTeX
$$$$\\\\text{ContinuousOn}(s \\mapsto \\\\operatorname{term}(n+1,s), [1,\\\\infty))$$$$
Lean4
theorem continuousOn_term (n : ℕ) : ContinuousOn (fun x ↦ term (n + 1) x) (Ici 1) := by
-- TODO: can this be shortened using the lemma
-- `continuous_parametric_intervalIntegral_of_continuous'` from https://github.com/leanprover-community/mathlib4/pull/11185?
simp only [term, intervalIntegral.integral_of_le (by linarith : (↑(n + 1) : ℝ) ≤ ↑(n + 1) + 1)]
apply continuousOn_of_dominated (bound := fun x ↦ (x - ↑(n + 1)) / x ^ (2 : ℝ))
· exact fun s hs ↦ (term_welldef (by simp) (zero_lt_one.trans_le hs)).1.1
· intro s (hs : 1 ≤ s)
rw [ae_restrict_iff' measurableSet_Ioc]
filter_upwards with x hx
have : 1 < x := lt_of_le_of_lt (by simp) hx.1
rw [norm_of_nonneg (div_nonneg (sub_nonneg.mpr hx.1.le) (by positivity)), Nat.cast_add_one]
gcongr
· exact_mod_cast sub_nonneg.mpr hx.1.le
· exact this.le
· linarith
· rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le (by linarith)]
exact_mod_cast term_welldef (by cutsat : 0 < (n + 1)) zero_lt_one
· rw [ae_restrict_iff' measurableSet_Ioc]
filter_upwards with x hx
refine continuousOn_of_forall_continuousAt (fun s (hs : 1 ≤ s) ↦ continuousAt_const.div ?_ ?_)
· exact continuousAt_const.rpow (continuousAt_id.add continuousAt_const) (Or.inr (by linarith))
· exact (rpow_pos_of_pos ((Nat.cast_pos.mpr (by simp)).trans hx.1) _).ne'
