English
The interval integral on [a,b] equals the integral over Ioc a b up to a sign depending on a ≤ b.
Русский
Интервальный интеграл на отрезке [a,b] равен интегралу по Ioc a b с знаком, зависящим от того, выполняется ли a ≤ b.
LaTeX
$$$\\int x \\in a..b f(x) \\mathrm{d}\\mu = (\\text{sign}) \\; \\int x \\in Ι a b f(x) \\mathrm{d}\\mu$ with sign = 1 if a ≤ b and -1 otherwise.$$
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`. 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` will generate goals `Filter ℝ` and
`TendstoIxxClass Ioc ?m_1 l'`. -/
theorem eventually_intervalIntegrable {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' (𝓝 c)) {u v : ι → ℝ} {lt : Filter ι} (hu : Tendsto u lt l)
(hv : Tendsto v lt l) : ∀ᶠ t in lt, IntervalIntegrable f μ (u t) (v t) :=
(hf.mono_left inf_le_left).eventually_intervalIntegrable_ae hfm hμ hu hv
