locallyIntegrable_const_enorm — Mathlib

English

If f is locally integrable and g is a.e. bounded by f in norm, then g is locally integrable.

Русский

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

LaTeX

$$$\\operatorname{LocallyIntegrable} f \\mu \\Rightarrow \\forall g,\\ \\operatorname{AEStronglyMeasurable} g \\mu \\rightarrow \\operatorname{ae}\\ \\|g\\| ≤ \\|f\\| \\Rightarrow \\operatorname{LocallyIntegrable} g \\mu$$$

Lean4

theorem locallyIntegrable_const_enorm [IsLocallyFiniteMeasure μ] {c : ε} (hc : ‖c‖ₑ ≠ ∞) :
    LocallyIntegrable (fun _ => c) μ :=
  (memLp_top_const_enorm hc).locallyIntegrable le_top

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