English
Integrability on Iio(a) is equivalent to integrability at bottom, integrability at nhdsWithin(a, Iio(a)), and local integrability on Iio(a).
Русский
Интегрируемость на Iio(a) эквивалентна интегрируемости на atBot, интегрируемости на nhdsWithin(a, Iio(a)) и локальной интегрируемости на Iio(a).
LaTeX
$$$\operatorname{IntegrableOn}(f, \mathrm{Iio}(a), \mu) \iff \bigl( \operatorname{IntegrableAtFilter}(f, \text{atBot}, \mu) \land \operatorname{IntegrableAtFilter}(f, \mathcal{nhdsWithin}(a, \mathrm{Iio}(a)), \mu) \land \operatorname{LocallyIntegrableOn}(f, \mathrm{Iio}(a), \mu) \bigr)$$$
Lean4
theorem integrableOn_Iio_iff_integrableAtFilter_atBot_nhdsWithin [LinearOrder X] [CompactIccSpace X] [NoMinOrder X]
[OrderTopology X] :
IntegrableOn f (Iio a) μ ↔
IntegrableAtFilter f atBot μ ∧ IntegrableAtFilter f (𝓝[<] a) μ ∧ LocallyIntegrableOn f (Iio a) μ :=
by
constructor
· intro h
exact ⟨⟨Iio a, Iio_mem_atBot a, h⟩, ⟨Iio a, self_mem_nhdsWithin, h⟩, h.locallyIntegrableOn⟩
· intro ⟨hbot, ⟨s, hsl, hs⟩, hlocal⟩
obtain ⟨s', ⟨hs'_mono, hs'⟩⟩ := mem_nhdsLT_iff_exists_Ioo_subset.mp hsl
refine (integrableOn_union.mpr ⟨?_, hs.mono hs' le_rfl⟩).mono Iio_subset_Iic_union_Ioo le_rfl
exact integrableOn_Iic_iff_integrableAtFilter_atBot.mpr ⟨hbot, hlocal.mono_set (Iic_subset_Iio.mpr hs'_mono)⟩
