rpowIntegrand₀₁_le_rpow_sub_one

English

For hp ∈ (0,1), ht > 0 and hx ≥ 0 we have rpowIntegrand₀₁(p,t,x) ≤ t^(p-1) for t > 0 and x ≥ 0, and in particular rpowIntegrand₀₁(p,t,1) ≤ t^(p-1).

Русский

Пусть hp ∈ (0,1), ht > 0 и hx ≥ 0. Тогда rpowIntegrand₀₁(p,t,x) ≤ t^(p-1) при t > 0, x ≥ 0, и в частности rpowIntegrand₀₁(p,t,1) ≤ t^(p-1).

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-1}$$$

Lean4

theorem rpowIntegrand₀₁_le_rpow_sub_one (hp : p ∈ Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) :
    rpowIntegrand₀₁ p t x ≤ t ^ (p - 1) := by
  by_cases hx_zero : x = 0
  case pos =>
    simp only [rpowIntegrand₀₁, hx_zero, add_zero, sub_self, mul_zero]
    positivity
  case neg =>
    calc
      _ = t ^ (p - 1) * x / (t + x) := by rw [rpowIntegrand₀₁_eq_pow_div hp ht hx]
      _ ≤ t ^ (p - 1) * x / x := by gcongr; linarith
      _ = t ^ (p - 1) * (x / x) := by ring
      _ = t ^ (p - 1) * 1 := by congr; exact (div_eq_one_iff_eq hx_zero).mpr rfl
      _ = _ := by simp

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