integrable_iff_integrableAtFilter_cocompact

English

For suitable spaces, integrability of f with respect to μ is equivalent to integrability at cocompact filter together with local integrability.

Русский

Для подходящих пространств интегрируемость f по μ эквивалентна интегрируемости на коккомпакт-фильтре вместе с локальной интегрируемостью.

LaTeX

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

Lean4

theorem integrable_iff_integrableAtFilter_cocompact :
    Integrable f μ ↔ (IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ) :=
  by
  refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩
  obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc
  rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]
  exact ⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩

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