rpowIntegrand₀₁_le_rpow_sub_two_mul_self

English

For hp ∈ (0,1), ht > 0 and hx ≥ 0, one has rpowIntegrand₀₁(p,t,x) ≤ t^(p-2)·x for t > 0, x ≥ 0.

Русский

Для hp ∈ (0,1), ht > 0 и hx ≥ 0 выполняется неравенство rpowIntegrand₀₁(p,t,x) ≤ t^(p-2)·x при t > 0, x ≥ 0.

LaTeX

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

Lean4

theorem rpowIntegrand₀₁_le_rpow_sub_two_mul_self (hp : p ∈ Ioo 0 1) (ht : 0 < t) (hx : 0 ≤ x) :
    rpowIntegrand₀₁ p t x ≤ t ^ (p - 2) * x :=
  calc
    _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]
    _ ≤ t ^ (p - 1) * x / t := by gcongr; linarith
    _ = t ^ (p - 1) / t * x := by ring
    _ = t ^ (p - 2) * x := by
      congr
      rw [← Real.rpow_sub_one (by positivity)]
      congr 1
      ring

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