English
Let p, q, r be ENNReal exponents forming a Holder triple. Let E, F, G be normed spaces and B: E × F → G be a continuous bilinear map. If f ∈ L^p(α, μ; E) and g ∈ L^q(α, μ; F), then the pointwise bilinear composition x ↦ B(f(x), g(x)) lies in L^r(α, μ; G).
Русский
Пусть p, q, r образуют тройку Холдэра. Пусть E, F, G — нормированные пространства, и B: E × F → G — непрерывная билинейная карта. Если f ∈ L^p(α, μ; E) и g ∈ L^q(α, μ; F), то функция x ↦ B(f(x), g(x)) принадлежит L^r(α, μ; G).
LaTeX
$$$f \\in L^p(E,\\mu) \\quad\\text{и}\\quad g \\in L^q(F,\\mu) \\implies x \\mapsto B(f(x), g(x)) \\in L^r(G,\\mu).$$$
Lean4
theorem memLp_of_bilin {f : α → E} {g : α → F} (hf : MemLp f p μ) (hg : MemLp g q μ) :
MemLp (fun x ↦ B (f x) (g x)) r μ :=
MeasureTheory.MemLp.of_bilin (r := r) (B · ·) ‖B‖₊ hf hg (B.aestronglyMeasurable_comp₂ hf.1 hg.1)
(.of_forall fun _ ↦ B.le_opNorm₂ _ _)
