English
There is a continuous bilinear map (the Holder operator) that sends a pair (f,g) with f ∈ L^p and g ∈ L^q into an element of L^r by evaluating a bilinear map B pointwise.
Русский
Существуют непрерывные билинейные отображения, задаваемые Холдером, которые позволяют получить из пары функций f ∈ L^p и g ∈ L^q элемент в L^r путём покомпонентного применения билинейной карты B.
LaTeX
$$$\\text{holder}(f,g) = x \\mapsto B(f(x), g(x)) \\in L^r(G,\\mu).$$$
Lean4
/-- The map between `MeasureTheory.Lp` spaces satisfying `ENNReal.HolderTriple`
induced by a continuous bilinear map on the underlying spaces. -/
def holder (f : Lp E p μ) (g : Lp F q μ) : Lp G r μ :=
(B.memLp_of_bilin r (Lp.memLp f) (Lp.memLp g)).toLp
