English
For n > 0 and s > 0, the interval integral defining term is well-defined on [n, n+1].
Русский
При n > 0 и s > 0 интеграл на промежутке [n, n+1], задающий term, существует.
LaTeX
$$$\\\\text{IntervalIntegrable}\\left( x \\mapsto \\frac{x-n}{x^{s+1}} \\right)\\text{ on } [n,n+1]$$$
Lean4
theorem term_welldef {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : 0 < s) :
IntervalIntegrable (fun x : ℝ ↦ (x - n) / x ^ (s + 1)) volume n (n + 1) :=
by
rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)]
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc
· fun_prop
· apply continuousAt_id.rpow_const (Or.inr <| by linarith)
· exact (rpow_pos_of_pos ((Nat.cast_pos.mpr hn).trans_le hx.1) _).ne'
