integral_rpowIntegrand₀₁_one_pos

English

For hp ∈ (0,1) and x ≥ 0, the integral of rpowIntegrand₀₁ t x over (0,∞) equals x^p times the integral of rpowIntegrand₀₁ t 1 over (0,∞).

Русский

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

LaTeX

$$$\\int_{0}^{\\infty} rpowIntegrand_{01} p\\, t\\, x \\, dt = x^{p} \\int_{0}^{\\infty} rpowIntegrand_{01} p\\, t\\, 1 \\, dt$$$

Lean4

theorem integral_rpowIntegrand₀₁_one_pos (hp : p ∈ Ioo 0 1) : 0 < ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 :=
  calc
    0 < -1 / (2 * (p - 1)) := by
      rw [neg_div, neg_pos, one_div_neg]
      simp only [mem_Ioo] at hp
      linarith
    _ ≤ ∫ t in Ioi 0, rpowIntegrand₀₁ p t 1 := le_integral_rpowIntegrand₀₁_one hp

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