lpPairing_eq_integral — Mathlib

English

The lpPairing equals the integral of the bilinear evaluation against μ.

Русский

lpPairing равен интегралу от билинейной оценки по мерe μ.

LaTeX

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

Lean4

theorem lpPairing_eq_integral (f : Lp E p μ) (g : Lp F q μ) : B.lpPairing μ p q f g = ∫ x, B (f x) (g x) ∂μ :=
  by
  change L1.integralCLM _ = _
  rw [← L1.integral_def, L1.integral_eq_integral]
  exact integral_congr_ae <| B.coeFn_holder _ _

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