nnnorm_holder_apply_apply_le — Mathlib

English

The nonnegative norm (nnnorm) of the Holder product is bounded by the product of nnorms of B and its inputs.

Русский

Неотрицательная норма (nnnorm) произведения Холдэра ограничена произведением nnnorm самой карты B и её входов.

LaTeX

$$$\\|B.holder(r)\\ f\\ g\\|_{+} \\le \\|B\\|_{+} \\|f\\|_{+} \\|g\\|_{+}.$$$

Lean4

theorem nnnorm_holder_apply_apply_le (f : Lp E p μ) (g : Lp F q μ) : ‖B.holder r f g‖₊ ≤ ‖B‖₊ * ‖f‖₊ * ‖g‖₊ :=
  by
  simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_mul, ← enorm_eq_nnnorm, Lp.enorm_def]
  apply eLpNorm_congr_ae (coeFn_holder B f g) |>.trans_le
  exact
    eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (Lp.memLp f).1 (Lp.memLp g).1 (B · ·) ‖B‖₊
      (.of_forall fun _ ↦ B.le_opNorm₂ _ _)

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