eLpNormEssSup_indicator_le — Mathlib

English

If a.e. f(x) ∈ [a,b] and f is AES-measurable, then MemLp for any p holds.

Русский

Если почти всюду f лежит в отрезке [a,b] и f измерима, то f ∈ L^p для любого p.

LaTeX

$$$\forall^{\mathrm{a}} x, f(x) \in [a,b] \wedge \text{AEStronglyMeasurable}(f,μ) \rightarrow \forall p, \text{MemLp}(f,p,μ)$$$

Lean4

theorem eLpNormEssSup_indicator_le (s : Set α) (f : α → ε) : eLpNormEssSup (s.indicator f) μ ≤ eLpNormEssSup f μ :=
  by
  refine essSup_mono_ae (Eventually.of_forall fun x => ?_)
  simp_rw [enorm_indicator_eq_indicator_enorm]
  exact Set.indicator_le_self s _ x

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