instHSMulSubtypeAEEqFunMemAddSubgroup

English

The lpPairing functional equals the integral expression by construction.

Русский

Функционал lpPairing по определению равен выражению через интеграл.

LaTeX

$$$B.lpPairing\\,\\mu\\,p\\,q\\,f\\,g = \\int_\\alpha B(f(x),g(x))\\,d\\mu.$$$

Lean4

/-- Heterogeneous scalar multiplication of `MeasureTheory.Lp` functions by `MeasureTheory.Lp`
functions when the exponents satisfy `ENNReal.HolderTriple p q r`. -/
instance : HSMul (Lp 𝕜 p μ) (Lp E q μ) (Lp E r μ) where hSMul f g := (Lp.memLp g).smul (Lp.memLp f) |>.toLp (⇑f • ⇑g)

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