# 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`.

source
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.

source
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.

source
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.

source
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.