Theorems · Theorem · real analysis

intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae

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

Fundamental theorem of calculus-1, strict differentiability at filter in both endpoints. If f is a measurable function integrable on a..b, (la, la') is an intervalIntegral.FTCFilter pair around a, and (lb, lb') is an intervalIntegral.FTCFilter pair around b, and f has finite limits ca and cb almost surely at la' and lb', respectively, then (∫ x in va..vb, f x) - ∫ x in ua..ub, f x = (vb - ub) • cb - (va - ua) • ca + o(‖va - ua‖ + ‖vb - ub‖) as ua and va tend to la while ub and vb tend to lb. This lemma could've been formulated using HasStrictFDerivAtFilter if we had this definition.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpaceintervalIntegral.FTCFilterintervalIntegral.FTCFilter