coeFn_holder — Mathlib

English

The Holder map coincides almost everywhere with the pointwise evaluation given by the bilinear map B.

Русский

Карта Холдер почти везде совпадает с покомпонентной оценкой по билинейной карте B.

LaTeX

$$$(B.holder(r)\\, f\\, g)(x) = B(f(x),g(x)) \\quad\\text{для почти всех } x.$$$

Lean4

theorem coeFn_holder (f : Lp E p μ) (g : Lp F q μ) : B.holder r f g =ᵐ[μ] fun x ↦ B (f x) (g x) :=
  by
  rw [holder]
  exact MemLp.coeFn_toLp _

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