eLpNormEssSup_le_of_ae_nnnorm_bound

English

If ∀ᵐ x, ‖f(x)‖ ≤ C for some ENorm bound C, then eLpNormEssSup f μ ≤ C.

Русский

Если функция фрагментно ограничена константой C, essSup не превышает C.

LaTeX

$$$\\forall^* x, \\|f(x)\\| ≤ C \\Rightarrow eLpNormEssSup(f,μ) ≤ C$ (иногда через ENNReal).$$

Lean4

theorem eLpNormEssSup_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : eLpNormEssSup f μ ≤ C :=
  essSup_le_of_ae_le (C : ℝ≥0∞) <| hfC.mono fun _x hx => ENNReal.coe_le_coe.mpr hx

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