English
If f has a finite limit at l', and certain regularity holds (measurability, generation), then for u, v tending to l, IntervalIntegrable f μ (u t) (v t) holds eventually.
Русский
Если у функции f есть конечный предел при l' и соблюдены необходимые условия, тогда для функций u и v, стремящихся к l, выполняется условие IntervalIntegrable f μ (u t) (v t) для больших t.
LaTeX
$$∃t0, ∀ t ≥ t0, IntervalIntegrable(f, μ, u(t), v(t))$$
Lean4
/-- Let `l'` be a measurably generated filter; let `l` be a of filter such that each `s ∈ l'`
eventually includes `Ioc u v` as both `u` and `v` tend to `l`. Let `μ` be a measure finite at `l'`.
Suppose that `f : ℝ → E` has a finite limit at `l' ⊓ ae μ`. Then `f` is interval integrable on
`u..v` provided that both `u` and `v` tend to `l`.
Typeclass instances allow Lean to find `l'` based on `l` but not vice versa, so
`apply Tendsto.eventually_intervalIntegrable_ae` will generate goals `Filter ℝ` and
`TendstoIxxClass Ioc ?m_1 l'`. -/
theorem eventually_intervalIntegrable_ae {f : ℝ → E} {μ : Measure ℝ} {l l' : Filter ℝ}
(hfm : StronglyMeasurableAtFilter f l' μ) [TendstoIxxClass Ioc l l'] [IsMeasurablyGenerated l']
(hμ : μ.FiniteAtFilter l') {c : E} (hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)) {u v : ι → ℝ} {lt : Filter ι}
(hu : Tendsto u lt l) (hv : Tendsto v lt l) : ∀ᶠ t in lt, IntervalIntegrable f μ (u t) (v t) :=
have := (hf.integrableAtFilter_ae hfm hμ).eventually
((hu.Ioc hv).eventually this).and <| (hv.Ioc hu).eventually this
