rpowIntegrand₀₁_apply_mul_eqOn_Ici

English

There is an equality on the interval [0, ∞) that mirrors the identity on Ioi, linking rpowIntegrand at (x·t) with t and x powers.

Русский

Существуют равенства на интервале [0, ∞), копирующие тождество на Ioi, связывая rpowIntegrand в точке (x·t) с степенями t и x.

LaTeX

$$$(\mathrm{Ici}\ 0).\text{EqOn}(\lambda t, \mathrm{rpowIntegrand}_{01}(p, (x\cdot t), x)\cdot x, \lambda t, \mathrm{rpowIntegrand}_{01}(t,1)\cdot x^{p})$$$

Lean4

theorem rpowIntegrand₀₁_apply_mul_eqOn_Ici (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) :
    (Ici 0).EqOn (fun t => rpowIntegrand₀₁ p (x * t) x * x) (fun t => (rpowIntegrand₀₁ p t 1) * x ^ p) := fun _ ht =>
  rpowIntegrand₀₁_apply_mul' hp ht hx

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