holderₗ — Mathlib

English

The HolderL operator has operator norm bounded by the norm of B: ||holderL|| ≤ ||B||.

Русский

Оператор ХолдерL имеет норму-оператора не превосходящую норму B.

LaTeX

$$$\\|\\mathrm{holderL}(B)\\| \\le \\|B\\|.$$$

Lean4

/-- `MeasureTheory.Lp.holder` as a bilinear map. -/
@[simps! apply_apply]
def holderₗ : Lp E p μ →ₗ[𝕜] Lp F q μ →ₗ[𝕜] Lp G r μ :=
  .mk₂ 𝕜 (B.holder r) B.holder_add_left B.holder_smul_left B.holder_add_right B.holder_smul_right

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