locallyIntegrable — Mathlib

English

Integrability of f is equivalent to integrability at cocompact filter together with local integrability.

Русский

Интегрируемость f эквивалентна интегрируемости на коккомпакт-фильтр вместе с локальной интегрируемостью.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \iff (\operatorname{IntegrableAtFilter}(f, \text{cocompact } X, \mu) \land \operatorname{LocallyIntegrable}(f, \mu))$$$

Lean4

/-- A continuous function `f` is locally integrable with respect to any locally finite measure. -/
theorem locallyIntegrable [IsLocallyFiniteMeasure μ] [SecondCountableTopologyEither X E] (hf : Continuous f) :
    LocallyIntegrable f μ :=
  hf.integrableAt_nhds

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