English
For a < -1 and c > 0, ∫_{c}^{∞} t^a dt = -c^{a+1}/(a+1).
Русский
Для a < -1 и c > 0 верно: ∫_{c}^{∞} t^{a} dt = - c^{a+1}/(a+1).
LaTeX
$$$\\int_{c}^{\\infty} t^{a} \\, dt = -\\dfrac{c^{a+1}}{a+1}$, \\; a < -1,\\; c > 0$$
Lean4
theorem integral_Ioi_rpow_of_lt {a : ℝ} (ha : a < -1) {c : ℝ} (hc : 0 < c) :
∫ t : ℝ in Ioi c, t ^ a = -c ^ (a + 1) / (a + 1) :=
by
have hd : ∀ x ∈ Ici c, HasDerivAt (fun t => t ^ (a + 1) / (a + 1)) (x ^ a) x :=
by
intro x hx
convert (hasDerivAt_rpow_const (p := a + 1) (Or.inl (hc.trans_le hx).ne')).div_const _ using 1
simp [show a + 1 ≠ 0 from ne_of_lt (by linarith), mul_comm]
have ht : Tendsto (fun t => t ^ (a + 1) / (a + 1)) atTop (𝓝 (0 / (a + 1))) :=
by
apply Tendsto.div_const
simpa only [neg_neg] using tendsto_rpow_neg_atTop (by linarith : 0 < -(a + 1))
convert integral_Ioi_of_hasDerivAt_of_tendsto' hd (integrableOn_Ioi_rpow_of_lt ha hc) ht using 1
simp only [neg_div, zero_div, zero_sub]
