English
The value of lpPairing on f,g equals the integral of the pointwise B(f(x),g(x)).
Русский
Значение lpPairing на f,g равно интегралу по x от B(f(x),g(x)).
LaTeX
$$$\\mathrm{lpPairing}(B)\\,f\\,g = \\int_\\alpha B(f(x),g(x))\\,d\\mu.$$$
Lean4
/-- The natural pairing between `Lp E p μ` and `Lp F q μ` (for Hölder conjugate `p q : ℝ≥0∞`) with
values in a space `G` induced by a bilinear map `B : E →L[𝕜] F →L[𝕜] G`.
This is given by `∫ x, B (f x) (g x) ∂μ`.
In the special case when `B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip`, which is
definitionally the same as `B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜)`, this is the
natural map `Lp (StrongDual 𝕜 E) p μ →L[𝕜] StrongDual 𝕜 (Lp E q μ)`. -/
def lpPairing (B : E →L[𝕜] F →L[𝕜] G) : Lp E p μ →L[𝕜] Lp F q μ →L[𝕜] G :=
(L1.integralCLM' 𝕜 |>.postcomp <| Lp F q μ) ∘L (B.holderL μ p q 1)
