Theorems · Theorem · measure theory

ContinuousAt.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} {f : X → E},
  ContinuousAt f x →
    StronglyMeasurableAtFilter f (nhds x) μ →
      ∀ {s : ι → Set X} {li : Filter ι},
        Filter.Tendsto s li (nhds x).smallSets →
          ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
            autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousAt.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, nhds version: if μ is a locally finite measure and f is an almost everywhere measurable function that is continuous at a point a, then ∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i)) at li provided that s tends to (𝓝 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

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpaceOpensMeasurableSpaceMeasureTheory.IsLocallyFiniteMeasure