integrable_iff_integrableAtFilter_atBot_atTop

English

If f is integrable, then it is integrable at the bottom filter together with local integrability.

Русский

Если f интегрируема, то она интегрируема на фильтре atBot и локально интегрируема.

LaTeX

$$$\operatorname{Integrable}(f, \mu) \Rightarrow \bigl( \operatorname{IntegrableAtFilter}(f, \text{atBot}, \mu) \land \operatorname{LocallyIntegrable}(f, \mu) \bigr)$$$

Lean4

theorem integrable_iff_integrableAtFilter_atBot_atTop [PseudoMetrizableSpace ε''] {f : X → ε''} [LinearOrder X]
    [CompactIccSpace X] :
    Integrable f μ ↔ (IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f atTop μ) ∧ LocallyIntegrable f μ :=
  by
  constructor
  · exact fun hf ↦ ⟨⟨hf.integrableAtFilter _, hf.integrableAtFilter _⟩, hf.locallyIntegrable⟩
  · refine fun h ↦ integrable_iff_integrableAtFilter_cocompact.mpr ⟨?_, h.2⟩
    exact (IntegrableAtFilter.sup_iff.mpr h.1).filter_mono cocompact_le_atBot_atTop

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