locallyIntegrable — Mathlib

English

If f is locally integrable, there exists a sequence of open sets that cover the space, on each of which f is integrable.

Русский

Если f локально интегрируема, существует последовательность открытых множеств, которые покрывают пространство, на каждом из которых f интегрируема.

LaTeX

$$$\\exists u: \\mathbb{N} \\to \\mathrm{Set} X, (\\forall n, \\text{IsOpen}(u(n))) \\land (\\bigcup_n u(n)=\\mathrm{univ}) \\land (\\forall n, \\operatorname{IntegrableOn} f (u(n)) \\mu)$$$

Lean4

theorem locallyIntegrable [IsLocallyFiniteMeasure μ] {p : ℝ≥0∞} (hf : MemLp f p μ) (hp : 1 ≤ p) :
    LocallyIntegrable f μ := by
  intro x
  rcases μ.finiteAt_nhds x with ⟨U, hU, h'U⟩
  have : Fact (μ U < ⊤) := ⟨h'U⟩
  refine ⟨U, hU, ?_⟩
  rw [IntegrableOn, ← memLp_one_iff_integrable]
  apply (hf.restrict U).mono_exponent hp

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