rpowIntegrand₀₁_one_ge_rpow_sub_two

English

If p ∈ (0,1) and t ≥ 1, then (1/2)·t^(p-2) ≤ rpowIntegrand₀₁(p,t,1).

Русский

Если p ∈ (0,1) и t ≥ 1, тогда (1/2)·t^(p-2) ≤ rpowIntegrand₀₁(p,t,1).

LaTeX

$$$\\frac{1}{2}\\,t^{p-2} \\le rpowIntegrand_{01} p\\, t\\, 1\\quad (p\\in Ioo(0,1),\\ t\\ge 1)$$$

Lean4

theorem rpowIntegrand₀₁_one_ge_rpow_sub_two (hp : p ∈ Ioo 0 1) (ht : 1 ≤ t) :
    (1 : ℝ) / 2 * t ^ (p - 2) ≤ rpowIntegrand₀₁ p t 1 :=
  calc
    _ = t ^ (p - 1) * (1 / 2 * 1 / t) := by
      have : p - 2 = p - 1 - 1 := by ring
      rw [this, Real.rpow_sub (by linarith), Real.rpow_one]
      ring
    _ ≤ t ^ (p - 1) * (1 / (t + 1)) := by
      gcongr t ^ (p - 1) * ?_
      rw [mul_div_assoc, one_div_mul_one_div, one_div_le_one_div (by positivity) (by positivity)]
      linarith
    _ = rpowIntegrand₀₁ p t 1 := by rw [rpowIntegrand₀₁_eq_pow_div hp (by linarith) zero_le_one, mul_div_assoc]

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