integrableOn_Iic_iff_integrableAtFilter_atBot

English

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

Русский

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

LaTeX

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

Lean4

theorem integrableOn_Iic_iff_integrableAtFilter_atBot [LinearOrder X] [CompactIccSpace X] :
    IntegrableOn f (Iic a) μ ↔ IntegrableAtFilter f atBot μ ∧ LocallyIntegrableOn f (Iic a) μ :=
  by
  refine ⟨fun h ↦ ⟨⟨Iic a, Iic_mem_atBot a, h⟩, h.locallyIntegrableOn⟩, fun ⟨⟨s, hsl, hs⟩, h⟩ ↦ ?_⟩
  haveI : Nonempty X := Nonempty.intro a
  obtain ⟨a', ha'⟩ := mem_atBot_sets.mp hsl
  refine (integrableOn_union.mpr ⟨hs.mono ha' le_rfl, ?_⟩).mono Iic_subset_Iic_union_Icc le_rfl
  exact h.integrableOn_compact_subset Icc_subset_Iic_self isCompact_Icc

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