rpowIntegrand₀₁ — Mathlib

English

The Real rpowIntegrand function is defined as a function of t with parameters p and x, representing x^p times (t^{-1} - (t+x)^{-1}).

Русский

Функция Real rpowIntegrand представляет собой зависимость по t: p, x, x^p( t^{-1} - (t+x)^{-1}).

LaTeX

$$$\mathrm{rpowIntegrand}_{01}(p,t,x) = t^{p} (t^{-1} - (t+x)^{-1})$$$

Lean4

/-- Integrand for representing `x ↦ x ^ p` for `p ∈ (0,1)` -/
noncomputable def rpowIntegrand₀₁ (p t x : ℝ) : ℝ :=
  t ^ p * (t⁻¹ - (t + x)⁻¹)

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