integrableOn_rpowIntegrand₀₁_Ioi

English

For hp ∈ (0,1) and x ≥ 0, the function t ↦ rpowIntegrand₀₁(p,t)·x is integrable on the interval (0,∞).

Русский

Для hp ∈ (0,1) и x ≥ 0 функция t ↦ rpowIntegrand₀₁(p,t)·x является интегрируемой на промежутке (0, ∞).

LaTeX

$$$\\text{IntegrableOn}\\bigl( t \\mapsto rpowIntegrand_{01} p\\, t\\, x\\bigr)\\,(Ioi\\,0)\\;\\text{Real.measureSpace.volume}$$$

Lean4

theorem integrableOn_rpowIntegrand₀₁_Ioi (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
    IntegrableOn (rpowIntegrand₀₁ p · x) (Ioi 0) := by
  /- The integral converges because it is `O(t ^ (p-1))` at the origin and `O(t ^ (p-2))` at
    infinity. Hence we break the integral into two parts. -/

  rw [← Set.Ioc_union_Ioi_eq_Ioi zero_le_one]
  exact IntegrableOn.union (integrableOn_rpowIntegrand₀₁_Ioc hp hx) (integrableOn_rpowIntegrand₀₁_Ioi_one hp hx)

Похожие утверждения