integrableOn_rpowIntegrand₀₁_Ici

English

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

Русский

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

LaTeX

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

Lean4

theorem integrableOn_rpowIntegrand₀₁_Ici (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
    IntegrableOn (rpowIntegrand₀₁ p · x) (Ici 0) :=
  integrableOn_rpowIntegrand₀₁_Ioi hp hx |>.congr_set_ae Ioi_ae_eq_Ici.symm

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