Theorems · Theorem · measure theory

MeasureTheory.integrableOn_Ioc_of_intervalIntegral_norm_bounded

∀ {ι : Type u_1} {E : Type u_2} {l : Filter ι} [l.NeBot] [l.IsCountablyGenerated] [inst : NormedAddCommGroup E]
  {a b : ι → ℝ} {f : ℝ → E} {I a₀ b₀ : ℝ},
  (∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) MeasureTheory.volume) →
    Filter.Tendsto a l (nhds a₀) →
      Filter.Tendsto b l (nhds b₀) →
        (∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc (a i) (b i), ‖f x‖ ≤ I) →
          MeasureTheory.IntegrableOn f (Set.Ioc a₀ b₀) MeasureTheory.volume

Defined in

Mathlib.MeasureTheory.Integral.IntegralEqImproper

Cited by

2 results in Mathlib

Foundations

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

Assumes

Filter.NeBotFilter.IsCountablyGeneratedNormedAddCommGroup