locallyIntegrable_const — Mathlib

English

If f is locally integrable and g is AEStronglyMeasurable with a.e. bound by f in norm, then g is locally integrable.

Русский

Если f локально интегрируема и g измерима слабо-строго по почти всей области, а ||g|| ≤ ||f||, тогда g локально интегрируема.

LaTeX

$$$\\operatorname{LocallyIntegrable} f \\mu \\Rightarrow \\forall g,\\ \\operatorname{AEStronglyMeasurable} g \\mu \\rightarrow \\forall^{\\!a.e.} x, \\|g(x)\\| ≤ \\|f(x)\\| \\Rightarrow \\operatorname{LocallyIntegrable} g \\mu$$$

Lean4

theorem locallyIntegrable_const [IsLocallyFiniteMeasure μ] (c : E) : LocallyIntegrable (fun _ => c) μ :=
  locallyIntegrable_const_enorm enorm_ne_top

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