Theorems · Theorem · real analysis

intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right

∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {c : E} {lb lb' : Filter ℝ} {lt : Filter ι} {a b : ℝ} {u v : ι → ℝ} [intervalIntegral.FTCFilter b lb lb'],
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f lb' MeasureTheory.volume →
      Filter.Tendsto f (lb' ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        Filter.Tendsto u lt lb →
          Filter.Tendsto v lt lb →
            (fun t => ((∫ (x : ℝ) in a..v t, f x) - ∫ (x : ℝ) in a..u t, f x) - (v t - u t) • c) =o[lt] (v - u)

Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. If f is a measurable function integrable on a..b, (lb, lb') is an intervalIntegral.FTCFilter pair around b, and f has a finite limit c almost surely at lb', then (∫ x in a..v, f x) - ∫ x in a..u, f x = (v - u) • c + o(‖v - u‖) as u and v tend to lb. This lemma could've been formulated using HasStrictDerivAtFilter if we had this definition.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceintervalIntegral.FTCFilter