holder_smul_left — Mathlib

English

There is a natural bilinear map lpPairing giving a pairing between Lp(E,p) and Lp(F,q) into Lp(G,r) via B.

Русский

Существует естественная билинейная пара между Lp(E,p) и Lp(F,q) в Lp(G,r) через B.

LaTeX

$$$\\text{lpPairing}(B) : L^p(E,p,\\mu) \\to L^q(F,q,\\mu) \\to L^r(G,r,\\mu),\\quad (f,g) \\mapsto x \\mapsto B(f(x),g(x)).$$$

Lean4

theorem holder_smul_left (c : 𝕜) (f : Lp E p μ) (g : Lp F q μ) : B.holder r (c • f) g = c • B.holder r f g :=
  by
  simp only [holder, ← MemLp.toLp_const_smul]
  apply MemLp.toLp_congr
  filter_upwards [Lp.coeFn_smul c f] with x hx
  simp [hx]

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