Theorems · Theorem · measure theory

Filter.Tendsto.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] {μ : MeasureTheory.Measure X} {l : Filter X} [l.IsMeasurablyGenerated]
  {f : X → E} {b : E},
  Filter.Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b) →
    StronglyMeasurableAtFilter f l μ →
      μ.FiniteAtFilter l →
        ∀ {s : ι → Set X} {li : Filter ι},
          Filter.Tendsto s li l.smallSets →
            ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
              autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) Filter.Tendsto.integral_sub_linear_isLittleO_ae._auto_1 →
                (fun i => ∫ (x : X) in s i, f x ∂μ - m i • b) =o[li] m

Fundamental theorem of calculus for set integrals: if μ is a measure that is finite at a filter l and f is a measurable function that has a finite limit b at l ⊓ ae μ, then ∫ x in s i, f x ∂μ = μ (s i) • b + o(μ (s i)) at a filter li provided that s i tends to l.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

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNormedAddCommGroupNormedSpaceCompleteSpaceFilter.IsMeasurablyGenerated