Filters used in box-based integrals #

First we define a structure BoxIntegral.IntegrationParams. This structure will be used as an argument in the definition of BoxIntegral.integral in order to use the same definition for a few well-known definitions of integrals based on partitions of a rectangular box into subboxes (Riemann integral, Henstock-Kurzweil integral, and McShane integral).

This structure holds three Boolean values (see below), and encodes eight different sets of parameters; only four of these values are used somewhere in mathlib4. Three of them correspond to the integration theories listed above, and one is a generalization of the one-dimensional Henstock-Kurzweil integral such that the divergence theorem works without additional integrability assumptions.

Finally, for each set of parameters l : BoxIntegral.IntegrationParams and a rectangular box I : BoxIntegral.Box ι, we define several Filters that will be used either in the definition of the corresponding integral, or in the proofs of its properties. We equip BoxIntegral.IntegrationParams with a BoundedOrder structure such that larger IntegrationParams produce larger filters.

Main definitions #

Integration parameters #

The structure BoxIntegral.IntegrationParams has 3 Boolean fields with the following meaning:

bRiemann: the value true means that the filter corresponds to a Riemann-style integral, i.e. in the definition of integrability we require a constant upper estimate r on the size of boxes of a tagged partition; the value false means that the estimate may depend on the position of the tag.
bHenstock: the value true means that we require that each tag belongs to its own closed box; the value false means that we only require that tags belong to the ambient box.
bDistortion: the value true means that r can depend on the maximal ratio of sides of the same box of a partition. Presence of this case make quite a few proofs harder but we can prove the divergence theorem only for the filter BoxIntegral.IntegrationParams.GP = ⊥ = {bRiemann := false, bHenstock := true, bDistortion := true}.

Well-known sets of parameters #

Out of eight possible values of BoxIntegral.IntegrationParams, the following four are used in the library.

BoxIntegral.IntegrationParams.Riemann (bRiemann = true, bHenstock = true, bDistortion = false): this value corresponds to the Riemann integral; in the corresponding filter, we require that the diameters of all boxes J of a tagged partition are bounded from above by a constant upper estimate that may not depend on the geometry of J, and each tag belongs to the corresponding closed box.
BoxIntegral.IntegrationParams.Henstock (bRiemann = false, bHenstock = true, bDistortion = false): this value corresponds to the most natural generalization of Henstock-Kurzweil integral to higher dimension; the only (but important!) difference between this theory and Riemann integral is that instead of a constant upper estimate on the size of all boxes of a partition, we require that the partition is subordinate to a possibly discontinuous function r : (ι → ℝ) → {x : ℝ | 0 < x}, i.e. each box J is included in a closed ball with center π.tag J and radius r J.
BoxIntegral.IntegrationParams.McShane (bRiemann = false, bHenstock = false, bDistortion = false): this value corresponds to the McShane integral; the only difference with the Henstock integral is that we allow tags to be outside of their boxes; the tags still have to be in the ambient closed box, and the partition still has to be subordinate to a function.
BoxIntegral.IntegrationParams.GP = ⊥ (bRiemann = false, bHenstock = true, bDistortion = true): this is the least integration theory in our list, i.e., all functions integrable in any other theory is integrable in this one as well. This is a non-standard generalization of the Henstock-Kurzweil integral to higher dimension. In dimension one, it generates the same filter as Henstock. In higher dimension, this generalization defines an integration theory such that the divergence of any Fréchet differentiable function f is integrable, and its integral is equal to the sum of integrals of f over the faces of the box, taken with appropriate signs.

A function f is GP-integrable if for any ε > 0 and c : ℝ≥0 there exists r : (ι → ℝ) → {x : ℝ | 0 < x} such that for any tagged partition π subordinate to r, if each tag belongs to the corresponding closed box and for each box J ∈ π, the maximal ratio of its sides is less than or equal to c, then the integral sum of f over π is ε-close to the integral.

Filters and predicates on `TaggedPrepartition I` #

For each value of IntegrationParams and a rectangular box I, we define a few filters on TaggedPrepartition I. First, we define a predicate

structure BoxIntegral.IntegrationParams.MemBaseSet (l : BoxIntegral.IntegrationParams)
  (I : BoxIntegral.Box ι) (c : ℝ≥0) (r : (ι → ℝ) → Ioi (0 : ℝ))
  (π : BoxIntegral.TaggedPrepartition I) : Prop where

This predicate says that

if l.bHenstock, then π is a Henstock prepartition, i.e. each tag belongs to the corresponding closed box;
π is subordinate to r;
if l.bDistortion, then the distortion of each box in π is less than or equal to c;
if l.bDistortion, then there exists a prepartition π' with distortion ≤ c that covers exactly I \ π.iUnion.

The last condition is always true for c > 1, see TODO section for more details.

Then we define a predicate BoxIntegral.IntegrationParams.RCond on functions r : (ι → ℝ) → {x : ℝ | 0 < x}. If l.bRiemann, then this predicate requires r to be a constant function, otherwise it imposes no restrictions on r. We introduce this definition to prove a few dot-notation lemmas: e.g., BoxIntegral.IntegrationParams.RCond.min says that the pointwise minimum of two functions that satisfy this condition satisfies this condition as well.

Then we define four filters on BoxIntegral.TaggedPrepartition I.

BoxIntegral.IntegrationParams.toFilterDistortion: an auxiliary filter that takes parameters (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : ℝ≥0) and returns the filter generated by all sets {π | MemBaseSet l I c r π}, where r is a function satisfying the predicate BoxIntegral.IntegrationParams.RCond l;
BoxIntegral.IntegrationParams.toFilter l I: the supremum of l.toFilterDistortion I c over all c : ℝ≥0;
BoxIntegral.IntegrationParams.toFilterDistortioniUnion l I c π₀, where π₀ is a prepartition of I: the infimum of l.toFilterDistortion I c and the principal filter generated by {π | π.iUnion = π₀.iUnion};
BoxIntegral.IntegrationParams.toFilteriUnion l I π₀: the supremum of l.toFilterDistortioniUnion l I c π₀ over all c : ℝ≥0. This is the filter (in the case π₀ = ⊤ is the one-box partition of I) used in the definition of the integral of a function over a box.

Implementation details #

Later we define the integral of a function over a rectangular box as the limit (if it exists) of the integral sums along BoxIntegral.IntegrationParams.toFilteriUnion l I ⊤. While it is possible to define the integral with a general filter on BoxIntegral.TaggedPrepartition I as a parameter, many lemmas (e.g., Sacks-Henstock lemma and most results about integrability of functions) require the filter to have a predictable structure. So, instead of adding assumptions about the filter here and there, we define this auxiliary type that can encode all integration theories we need in practice.
While the definition of the integral only uses the filter BoxIntegral.IntegrationParams.toFilteriUnion l I ⊤ and partitions of a box, some lemmas (e.g., the Henstock-Sacks lemmas) are best formulated in terms of the predicate MemBaseSet and other filters defined above.
We use Bool instead of Prop for the fields of IntegrationParams in order to have decidable equality and inequalities.

TODO #

Currently, BoxIntegral.IntegrationParams.MemBaseSet explicitly requires that there exists a partition of the complement I \ π.iUnion with distortion ≤ c. For c > 1, this condition is always true but the proof of this fact requires more API about BoxIntegral.Prepartition.splitMany. We should formalize this fact, then either require c > 1 everywhere, or replace ≤ c with < c so that we automatically get c > 1 for a non-trivial prepartition (and consider the special case π = ⊥ separately if needed).

Tags #

integral, rectangular box, partition, filter