Fundamental theorem of calculus for set integrals

This file proves a version of the Fundamental theorem of calculus for set integrals. See Filter.Tendsto.integral_sub_linear_isLittleO_ae and its corollaries.

Namely, consider a measurably generated filter l, a measure μ finite at this filter, and a function f that has a finite limit c at l ⊓ ae μ. Then ∫ x in s, f x ∂μ = μ s • c + o(μ s) as s tends to l.smallSets, i.e. for any ε>0 there exists t ∈ l such that ‖∫ x in s, f x ∂μ - μ s • c‖ ≤ ε * μ s whenever s ⊆ t. We also formulate a version of this theorem for a locally finite measure μ and a function f continuous at a point a.

theorem Filter.Tendsto.integral_sub_linear_isLittleO_ae {X : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {μ : MeasureTheory.Measure X} {l : Filter X} [l.IsMeasurablyGenerated] {f : X → E} {b : E} (h : Tendsto f (l ⊓ MeasureTheory.ae μ) (nhds b)) (hfm : StronglyMeasurableAtFilter f l μ) (hμ : μ.FiniteAtFilter l) {s : ι → Set X} {li : Filter ι} (hs : Tendsto s li l.smallSets) (m : ι → ℝ := fun (i : ι) => μ.real (s i)) (hsμ : (fun (i : ι) => μ.real (s i)) =ᶠ[li] m := by rfl) : (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.

theorem ContinuousWithinAt.integral_sub_linear_isLittleO_ae {X : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [TopologicalSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {t : Set X} {f : X → E} (hx : ContinuousWithinAt f t x) (ht : MeasurableSet t) (hfm : StronglyMeasurableAtFilter f (nhdsWithin x t) μ) {s : ι → Set X} {li : Filter ι} (hs : Filter.Tendsto s li (nhdsWithin x t).smallSets) (m : ι → ℝ := fun (i : ι) => μ.real (s i)) (hsμ : (fun (i : ι) => μ.real (s i)) =ᶠ[li] m := by rfl) : (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.

theorem ContinuousAt.integral_sub_linear_isLittleO_ae {X : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [TopologicalSpace X] [OpensMeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {f : X → E} (hx : ContinuousAt f x) (hfm : StronglyMeasurableAtFilter f (nhds x) μ) {s : ι → Set X} {li : Filter ι} (hs : Filter.Tendsto s li (nhds x).smallSets) (m : ι → ℝ := fun (i : ι) => μ.real (s i)) (hsμ : (fun (i : ι) => μ.real (s i)) =ᶠ[li] m := by rfl) : (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.

theorem ContinuousOn.integral_sub_linear_isLittleO_ae {X : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X E] {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {t : Set X} {f : X → E} (hft : ContinuousOn f t) (hx : x ∈ t) (ht : MeasurableSet t) {s : ι → Set X} {li : Filter ι} (hs : Filter.Tendsto s li (nhdsWithin x t).smallSets) (m : ι → ℝ := fun (i : ι) => μ.real (s i)) (hsμ : (fun (i : ι) => μ.real (s i)) =ᶠ[li] m := by rfl) : (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, f is continuous on a measurable set t, and a ∈ t, then ∫ x in (s i), f x ∂μ = μ (s i) • f a + o(μ (s i)) at 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.