English
For each 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 term_one {n : ℕ} (hn : 0 < n) : term n 1 = (log (n + 1) - log n) - 1 / (n + 1) :=
by
have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
intro x hx
rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
exact (Nat.cast_pos.mpr hn).trans_le hx.1
calc
term n 1
_ = ∫ x : ℝ in n..(n + 1), (x - n) / x ^ 2 := by
simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
_ = ∫ x : ℝ in n..(n + 1), (1 / x - n / x ^ 2) := (intervalIntegral.integral_congr (fun x hx ↦ by field_simp))
_ = (∫ x : ℝ in n..(n + 1), 1 / x) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 :=
by
simp_rw [← mul_one_div (n : ℝ)]
rw [intervalIntegral.integral_sub]
· simp_rw [intervalIntegral.integral_const_mul]
· exact intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (hv x hx).ne') (by fun_prop)
·
exact
(intervalIntegral.intervalIntegrable_one_div (fun x hx ↦ (sq_pos_of_pos (hv x hx)).ne')
(by fun_prop)).const_mul
_
_ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), 1 / x ^ 2 :=
by
congr 1
rw [integral_one_div_of_pos, log_div]
all_goals positivity
_ = (log (↑n + 1) - log ↑n) - n * ∫ x : ℝ in n..(n + 1), x ^ (-2 : ℝ) :=
by
congr 2
refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
exact (hv x hx).le
_ = log (↑n + 1) - log ↑n - n * (1 / n - 1 / (n + 1)) :=
by
rw [integral_rpow]
· simp_rw [sub_div, (by norm_num : (-2 : ℝ) + 1 = -1), div_neg, div_one, neg_sub_neg, rpow_neg_one, ← one_div]
· refine Or.inr ⟨by simp, notMem_uIcc_of_lt ?_ ?_⟩
all_goals positivity
_ = log (↑n + 1) - log ↑n - 1 / (↑n + 1) := by
congr 1
simp [field]
