English
If a < -1 and -m < c, then (x + m)^a is integrable on (c, ∞).
Русский
Если a < -1 и -m < c, то (x + m)^a интегрируемо на (c, ∞).
LaTeX
$$$\\text{IntegrableOn} \\big( x \\mapsto (x+m)^a \\big) (Ioi\\ c)$, \\; a < -1,\\; -m < c$$
Lean4
/-- If `-m < c`, then `(fun t : ℝ ↦ (t + m) ^ a)` is integrable on `(c, ∞)` for all `a < -1`. -/
theorem integrableOn_add_rpow_Ioi_of_lt {a c m : ℝ} (ha : a < -1) (hc : -m < c) :
IntegrableOn (fun (x : ℝ) ↦ (x + m) ^ a) (Ioi c) :=
by
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t ↦ (t + m) ^ (a + 1) / (a + 1)) ((x + m) ^ a) x :=
by
intro x hx
convert (((hasDerivAt_id _).add_const _).rpow_const _).div_const _ using 1
simp [show a + 1 ≠ 0 by linarith]
left; linarith [mem_Ici.mp hx, id_eq x]
have ht : Tendsto (fun t ↦ ((t + m) ^ (a + 1)) / (a + 1)) atTop (nhds (0 / (a + 1))) :=
by
rw [← neg_neg (a + 1)]
exact (tendsto_rpow_neg_atTop (by linarith)).comp (tendsto_atTop_add_const_right _ m tendsto_id) |>.div_const _
exact integrableOn_Ioi_deriv_of_nonneg' hd (fun t ht ↦ rpow_nonneg (by linarith [mem_Ioi.mp ht]) a) ht
