eLpNorm'_const_smul_le' — Mathlib

English

If |f| ≤ c|g| a.e., then eLpNorm' f p μ ≤ c · eLpNorm' g p μ for p ∈ [0,∞], including variants with real c.

Русский

Если |f| ≤ c|g| почти всюду, то eLpNorm' f p μ ≤ c · eLpNorm' g p μ для p в [0,∞].

LaTeX

$$$\forall p>0: \; eLpNorm'(f,p,μ) ≤ c \cdot eLpNorm'(g,p,μ)$$$

Lean4

theorem eLpNorm'_const_smul_le' (hq : 0 < q) : eLpNorm' (c • f) q μ ≤ ‖c‖ₑ * eLpNorm' f q μ :=
  eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' (Eventually.of_forall fun _ ↦ le_of_eq (enorm_smul ..)) hq

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