rpowIntegrand₀₁_eqOn_pow_div — Mathlib

English

On the positive reals, the equality rpowIntegrand₀₁ p t x equals t^(p-1) x/(t+x) holds for p ∈ Ioo(0,1) with t>0, x≥0.

Русский

На положительных вещественных числах равенство rpowIntegrand₀₁ p t x = t^(p-1) x/(t+x) выполняется для p ∈ Ioo(0,1) при t>0, x≥0.

LaTeX

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

Lean4

theorem rpowIntegrand₀₁_eqOn_pow_div (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
    Set.EqOn (rpowIntegrand₀₁ p · x) (fun t => t ^ (p - 1) * x / (t + x)) (Ioi 0) :=
  by
  intro t ht
  simp [rpowIntegrand₀₁_eq_pow_div hp (le_of_lt ht) hx]

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