locallyIntegrable_iff — Mathlib

English

Assuming locally compact locally metric conditions, f is locally integrable if and only if it is integrable on every compact set.

Русский

При локально компактном локальном метризуемом пространстве f локально интегрируема тогда и только тогда, когда интегрируема на каждом компактном множестве.

LaTeX

$$$\\operatorname{LocallyIntegrable} f\\mu \\iff \\forall k, (\\text{IsCompact } k) \\Rightarrow \\operatorname{IntegrableOn} f k \\mu$$$

Lean4

theorem locallyIntegrable_iff [PseudoMetrizableSpace ε] [LocallyCompactSpace X] :
    LocallyIntegrable f μ ↔ ∀ k : Set X, IsCompact k → IntegrableOn f k μ :=
  ⟨fun hf _k hk => hf.integrableOn_isCompact hk, fun hf x =>
    let ⟨K, hK, h2K⟩ := exists_compact_mem_nhds x
    ⟨K, h2K, hf K hK⟩⟩

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