Theorems · Theorem · measure theory

ContinuousWithinAt.integral_sub_linear_isLittleO_ae

∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {t : Set X} {f : X → E},
  ContinuousWithinAt f t x →
    MeasurableSet t →
      StronglyMeasurableAtFilter f (nhdsWithin x t) μ →
        ∀ {s : ι → Set X} {li : Filter ι},
          Filter.Tendsto s li (nhdsWithin x t).smallSets →
            ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
              autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousWithinAt.integral_sub_linear_isLittleO_ae._auto_1 →
                (fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m

Fundamental theorem of calculus for set integrals, nhdsWithin version: if μ is a locally finite measure and f is an almost everywhere measurable function that is continuous at a point a within a measurable set t, then ∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i)) at a filter li provided that s i tends to (𝓝[t] a).smallSets along li. Since μ (s i) is an ℝ≥0∞ number, we use μ.real (s i) in the actual statement. Often there is a good formula for μ.real (s i), so the formalization can take an optional argument m with this formula and a proof of (fun i => μ.real (s i)) =ᶠ[li] m. Without these arguments, m i = μ.real (s i) is used in the output.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsLocallyFiniteMeasure