eLpNormEssSup_const_smul_le' — Mathlib

English

If f and g are functions, with a.e. bound by c then eLpNormEssSup f ≤ c · eLpNormEssSup g.

Русский

Если f и g связаны неравенством almost everywhere с константой c, то eLpNormEssSup f ≤ c · eLpNormEssSup g.

LaTeX

$$$\\forall f,g,\\; (\\forall^{\\ast} x, \\|f(x)\\| ≤ c \\|g(x)\\|) \\Rightarrow eLpNormEssSup(f) ≤ c · eLpNormEssSup(g)$$$

Lean4

theorem eLpNormEssSup_const_smul_le' : eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * eLpNormEssSup f μ :=
  eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' (Eventually.of_forall fun _ => by simp [enorm_smul])

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