Integrals of Riemann, Henstock-Kurzweil, and McShane #
In this file we define the integral of a function over a box in ℝⁿ. The same definition works for
Riemann, Henstock-Kurzweil, and McShane integrals.
As usual, we represent ℝⁿ as the type of functions ι → ℝ for some finite type ι. A rectangular
box (l, u] in ℝⁿ is defined to be the set {x : ι → ℝ | ∀ i, l i < x i ∧ x i ≤ u i}, see
BoxIntegral.Box.
Let vol be a box-additive function on boxes in ℝⁿ with codomain E →L[ℝ] F. Given a function
f : ℝⁿ → E, a box I and a tagged partition π of this box, the integral sum of f over π
with respect to the volume vol is the sum of vol J (f (π.tag J)) over all boxes of π. Here
π.tag J is the point (tag) in ℝⁿ associated with the box J.
The integral is defined as the limit of integral sums along a filter. Different filters correspond
to different integration theories. In order to avoid code duplication, all our definitions and
theorems take an argument l : BoxIntegral.IntegrationParams. This is a type that holds three
boolean values, and encodes eight filters including those corresponding to Riemann,
Henstock-Kurzweil, and McShane integrals.
Following the design of infinite sums (see hasSum and tsum), we define a predicate
BoxIntegral.HasIntegral and a function BoxIntegral.integral that returns a vector satisfying
the predicate or zero if the function is not integrable.
Then we prove some basic properties of box integrals (linearity, a formula for the integral of a
constant). We also prove a version of the Henstock-Sacks inequality (see
BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet and
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq), prove
integrability of continuous functions, and provide a criterion for integrability w.r.t. a
non-Riemann filter (e.g., Henstock-Kurzweil and McShane).
Notation #
ℝⁿ: local notation forι → ℝ
Tags #
integral
Integral sum and its basic properties #
The integral sum of f : ℝⁿ → E over a tagged prepartition π w.r.t. box-additive volume vol
with codomain E →L[ℝ] F is the sum of vol J (f (π.tag J)) over all boxes of π.
Equations
- BoxIntegral.integralSum f vol π = ∑ J ∈ π.boxes, (vol J) (f (π.tag J))
Instances For
Basic integrability theory #
The predicate HasIntegral I l f vol y says that y is the integral of f over I along l
w.r.t. volume vol. This means that integral sums of f tend to 𝓝 y along
BoxIntegral.IntegrationParams.toFilteriUnion I ⊤.
Equations
- BoxIntegral.HasIntegral I l f vol y = Filter.Tendsto (BoxIntegral.integralSum f vol) (l.toFilteriUnion I ⊤) (nhds y)
Instances For
A function is integrable if there exists a vector that satisfies the HasIntegral
predicate.
Equations
- BoxIntegral.Integrable I l f vol = ∃ (y : F), BoxIntegral.HasIntegral I l f vol y
Instances For
The integral of a function f over a box I along a filter l w.r.t. a volume vol.
Returns zero on non-integrable functions.
Equations
- BoxIntegral.integral I l f vol = if h : BoxIntegral.Integrable I l f vol then Exists.choose h else 0
Instances For
Reinterpret BoxIntegral.HasIntegral as Filter.Tendsto, e.g., dot-notation theorems
that are shadowed in the BoxIntegral.HasIntegral namespace.
The ε-δ definition of BoxIntegral.HasIntegral.
Quite often it is more natural to prove an estimate of the form a * ε, not ε in the RHS of
BoxIntegral.hasIntegral_iff, so we provide this auxiliary lemma.
In a complete space, a function is integrable if and only if its integral sums form a Cauchy
net. Here we restate this fact in terms of ∀ ε > 0, ∃ r, ....
The integral of a nonnegative function w.r.t. a volume generated by a locally-finite measure is nonnegative.
If ‖f x‖ ≤ g x on [l, u] and g is integrable, then the norm of the integral of f is less
than or equal to the integral of g.
Henstock-Sacks inequality and integrability on subboxes #
Henstock-Sacks inequality for Henstock-Kurzweil integral says the following. Let f be a function
integrable on a box I; let r : ℝⁿ → (0, ∞) be a function such that for any tagged partition of
I subordinate to r, the integral sum over this partition is ε-close to the integral. Then for
any tagged prepartition (i.e. a finite collections of pairwise disjoint subboxes of I with tagged
points) π, the integral sum over π differs from the integral of f over the part of I covered
by π by at most ε. The actual statement in the library is a bit more complicated to make it work
for any BoxIntegral.IntegrationParams. We formalize several versions of this inequality in
BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet,
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq, and
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet.
Instead of using predicate assumptions on r, we define
BoxIntegral.Integrable.convergenceR (h : integrable I l f vol) (ε : ℝ) (c : ℝ≥0) : ℝⁿ → (0, ∞)
to be a function r such that
- if
l.bRiemann, thenris a constant; - if
ε > 0, then for any tagged partitionπofIsubordinate tor(more precisely, satisfying the predicatel.mem_base_set I c r), the integral sum offoverπdiffers from the integral offoverIby at mostε.
The proof is mostly based on [Russel A. Gordon, The integrals of Lebesgue, Denjoy, Perron, and Henstock][Gordon55].
If ε > 0, then BoxIntegral.Integrable.convergenceR is a function r : ℝ≥0 → ℝⁿ → (0, ∞)
such that for every c : ℝ≥0, for every tagged partition π subordinate to r (and satisfying
additional distortion estimates if BoxIntegral.IntegrationParams.bDistortion l = true), the
corresponding integral sum is ε-close to the integral.
If BoxIntegral.IntegrationParams.bRiemann = true, then r c x does not depend on x. If
ε ≤ 0, then we use r c x = 1.
Equations
- h.convergenceR ε = if hε : 0 < ε then ⋯.choose else fun (x : NNReal) (x : ι → ℝ) => ⟨1, BoxIntegral.Integrable.convergenceR.proof_3⟩
Instances For
Henstock-Sacks inequality. Let r₁ r₂ : ℝⁿ → (0, ∞) be a function such that for any tagged
partition of I subordinate to rₖ, k=1,2, the integral sum of f over this partition differs
from the integral of f by at most εₖ. Then for any two tagged prepartition π₁ π₂ subordinate
to r₁ and r₂ respectively and covering the same part of I, the integral sums of f over these
prepartitions differ from each other by at most ε₁ + ε₂.
The actual statement
- uses
BoxIntegral.Integrable.convergenceRinstead of a predicate assumption onr; - uses
BoxIntegral.IntegrationParams.MemBaseSetinstead of “subordinate tor” to account for additional requirements like being a Henstock partition or having a bounded distortion.
See also BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq and
BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet.
If f is integrable on I along l, then for two sufficiently fine tagged prepartitions
(in the sense of the filter BoxIntegral.IntegrationParams.toFilter l I) such that they cover
the same part of I, the integral sums of f over π₁ and π₂ are very close to each other.
If f is integrable on a box I along l, then for any fixed subset s of I that can be
represented as a finite union of boxes, the integral sums of f over tagged prepartitions that
cover exactly s form a Cauchy “sequence” along l.
If f is integrable on a box I, then it is integrable on any subbox of I.
If f is integrable on a box I, then integral sums of f over tagged prepartitions
that cover exactly a subbox J ≤ I tend to the integral of f over J along l.
Henstock-Sacks inequality. Let r : ℝⁿ → (0, ∞) be a function such that for any tagged
partition of I subordinate to r, the integral sum of f over this partition differs from the
integral of f by at most ε. Then for any tagged prepartition π subordinate to r, the
integral sum of f over this prepartition differs from the integral of f over the part of I
covered by π by at most ε.
The actual statement
- uses
BoxIntegral.Integrable.convergenceRinstead of a predicate assumption onr; - uses
BoxIntegral.IntegrationParams.MemBaseSetinstead of “subordinate tor” to account for additional requirements like being a Henstock partition or having a bounded distortion; - takes an extra argument
π₀ : prepartition Iand an assumptionπ.Union = π₀.Unioninstead of usingπ.to_prepartition.
Henstock-Sacks inequality. Let r : ℝⁿ → (0, ∞) be a function such that for any tagged
partition of I subordinate to r, the integral sum of f over this partition differs from the
integral of f by at most ε. Then for any tagged prepartition π subordinate to r, the
integral sum of f over this prepartition differs from the integral of f over the part of I
covered by π by at most ε.
The actual statement
- uses
BoxIntegral.Integrable.convergenceRinstead of a predicate assumption onr; - uses
BoxIntegral.IntegrationParams.MemBaseSetinstead of “subordinate tor” to account for additional requirements like being a Henstock partition or having a bounded distortion;
Integral sum of f over a tagged prepartition π such that π.Union = π₀.Union tends to the
sum of integrals of f over the boxes of π₀.
If f is integrable on I, then fun J ↦ integral J l f vol is box-additive on subboxes of
I: if π₁, π₂ are two prepartitions of I covering the same part of I, the sum of integrals
of f over the boxes of π₁ is equal to the sum of integrals of f over the boxes of π₂.
See also BoxIntegral.Integrable.toBoxAdditive for a bundled version.
If f is integrable on I, then fun J ↦ integral J l f vol is box-additive on subboxes of
I: if π₁, π₂ are two prepartitions of I covering the same part of I, the sum of integrals
of f over the boxes of π₁ is equal to the sum of integrals of f over the boxes of π₂.
See also BoxIntegral.Integrable.sum_integral_congr for an unbundled version.
Equations
- h.toBoxAdditive = { toFun := fun (J : BoxIntegral.Box ι) => BoxIntegral.integral J l f vol, sum_partition_boxes' := ⋯ }
Instances For
Integrability conditions #
A continuous function is box-integrable with respect to any locally finite measure.
This is true for any volume with bounded variation.
This is an auxiliary lemma used to prove two statements at once. Use one of the next two lemmas instead.
A function f has Henstock (or ⊥) integral over I is equal to the value of a box-additive
function g on I provided that vol J (f x) is sufficiently close to g J for sufficiently
small boxes J ∋ x. This lemma is useful to prove, e.g., to prove the Divergence theorem for
integral along ⊥.
Let l be either BoxIntegral.IntegrationParams.Henstock or ⊥. Let g a box-additive function
on subboxes of I. Suppose that there exists a nonnegative box-additive function B and a
countable set s with the following property.
For every c : ℝ≥0, a point x ∈ I.Icc, and a positive ε there exists δ > 0 such that for any
box J ≤ I such that
x ∈ J.Icc ⊆ Metric.closedBall x δ;- if
l.bDistortion(i.e.,l = ⊥), then the distortion ofJis less than or equal toc,
the distance between the term vol J (f x) of an integral sum corresponding to J and g J is
less than or equal to ε if x ∈ s and is less than or equal to ε * B J otherwise.
Then f is integrable on I along l with integral g I.
Suppose that there exists a nonnegative box-additive function B with the following property.
For every c : ℝ≥0, a point x ∈ I.Icc, and a positive ε there exists δ > 0 such that for any
box J ≤ I such that
J.Icc ⊆ Metric.closedBall x δ;- if
l.bDistortion(i.e.,l = ⊥), then the distortion ofJis less than or equal toc,
the distance between the term vol J (f x) of an integral sum corresponding to J and g J is
less than or equal to ε * B J.
Then f is McShane integrable on I with integral g I.