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