rpowIntegrand₀₁_eq_pow_div — Mathlib

English

If p ∈ Ioo 0 1 and t,x ≥ 0, then rpowIntegrand equals a certain div form, as above.

Русский

Если p ∈ (0,1) и t,x ≥ 0, то rpowIntegrand принимает форму деления, как выше.

LaTeX

$$$\text{rpowIntegrand}_{01}(p,t,x) = t^{p-1} \cdot \dfrac{x}{t+x}$ for $p\in(0,1)$, $t\ge 0$, $x\ge 0$$$

Lean4

theorem rpowIntegrand₀₁_eq_pow_div (hp : p ∈ Ioo 0 1) (ht : 0 ≤ t) (hx : 0 ≤ x) :
    rpowIntegrand₀₁ p t x = t ^ (p - 1) * x / (t + x) :=
  by
  by_cases ht' : t = 0
  case neg =>
    have hxt : t + x ≠ 0 := by positivity
    calc
      _ = (t : ℝ) ^ p * (t⁻¹ - (t + x)⁻¹) := rfl
      _ = (t : ℝ) ^ p * ((t + x - t) / (t * (t + x))) :=
        by
        simp only [inv_eq_one_div]
        rw [div_sub_div _ _ (by cutsat) (by cutsat)]
        simp
      _ = t ^ p / t * x / (t + x) := by simp [field]
      _ = t ^ (p - 1) * x / (t + x) := by congr; exact (Real.rpow_sub_one ht' p).symm
  case pos =>
    simp only [mem_Ioo] at hp
    have hp₂ : p - 1 ≠ 0 := by linarith
    simp [rpowIntegrand₀₁, ht', hp.1.ne', hp₂]

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