Theorems · Theorem · measure theory

Filter.Tendsto.eventually_intervalIntegrable

∀ {ι : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {l l' : Filter ℝ},
  StronglyMeasurableAtFilter f l' μ →
    ∀ [Filter.TendstoIxxClass Set.Ioc l l'] [l'.IsMeasurablyGenerated],
      μ.FiniteAtFilter l' →
        ∀ {c : E},
          Filter.Tendsto f l' (nhds c) →
            ∀ {u v : ι → ℝ} {lt : Filter ι},
              Filter.Tendsto u lt l → Filter.Tendsto v lt l → ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)

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'.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupFilter.TendstoIxxClassFilter.IsMeasurablyGenerated