# 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

theorem BoxIntegral.IntegrationParams.ext_iff :
x = y x.bRiemann = y.bRiemann x.bHenstock = y.bHenstock x.bDistortion = y.bDistortion
theorem BoxIntegral.IntegrationParams.ext (bRiemann : x.bRiemann = y.bRiemann) (bHenstock : x.bHenstock = y.bHenstock) (bDistortion : x.bDistortion = y.bDistortion) :
x = y

An IntegrationParams is a structure holding 3 boolean values used to define a filter to be used in the definition of a box-integrable function.

• 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 makes 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}.

Instances For

Auxiliary equivalence with a product type used to lift an order.

Equations
• One or more equations did not get rendered due to their size.
Instances For

Auxiliary OrderIso with a product type used to lift a BoundedOrder structure.

Equations
Instances For
Equations

The value BoxIntegral.IntegrationParams.GP = ⊥ (bRiemann = false, bHenstock = true, bDistortion = true) corresponds to a generalization of the Henstock integral such that the Divergence theorem holds true without additional integrability assumptions, see the module docstring for details.

Equations
Equations
• x✝.instDecidableRelLe x = And.decidable
Equations
• x.instDecidableEq y = decidable_of_iff (x.bRiemann = y.bRiemann x.bHenstock = y.bHenstock x.bDistortion = y.bDistortion)

The BoxIntegral.IntegrationParams corresponding 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.

Equations
Instances For

The BoxIntegral.IntegrationParams corresponding to the Henstock-Kurzweil integral. In the corresponding filter, we require that the tagged partition is subordinate to a (possibly, discontinuous) positive function r and each tag belongs to the corresponding closed box.

Equations
Instances For

The BoxIntegral.IntegrationParams corresponding to the McShane integral. In the corresponding filter, we require that the tagged partition is subordinate to a (possibly, discontinuous) positive function r; the tags may be outside of the corresponding closed box (but still inside the ambient closed box I.Icc).

Equations
Instances For

The BoxIntegral.IntegrationParams corresponding to the generalized Perron integral. In the corresponding filter, we require that the tagged partition is subordinate to a (possibly, discontinuous) positive function r and each tag belongs to the corresponding closed box. We also require an upper estimate on the distortion of all boxes of the partition.

Equations
Instances For
structure BoxIntegral.IntegrationParams.MemBaseSet {ι : Type u_1} [] (I : ) (c : NNReal) (r : (ι)()) :

The predicate corresponding to a base set of the filter defined by an IntegrationParams. It 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 automatically verified for partitions, and is used in the proof of the Sacks-Henstock inequality to compare two prepartitions covering the same part of the box.

It is also automatically satisfied for any c > 1, see TODO section of the module docstring for details.

• isSubordinate : π.IsSubordinate r
• isHenstock : l.bHenstock = trueπ.IsHenstock
• distortion_le : l.bDistortion = trueπ.distortion c
• exists_compl : l.bDistortion = true∃ (π' : ), π'.iUnion = I \ π.iUnion π'.distortion c
Instances For
theorem BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} (self : l.MemBaseSet I c r π) :
π.IsSubordinate r
theorem BoxIntegral.IntegrationParams.MemBaseSet.isHenstock {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} (self : l.MemBaseSet I c r π) :
l.bHenstock = trueπ.IsHenstock
theorem BoxIntegral.IntegrationParams.MemBaseSet.distortion_le {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} (self : l.MemBaseSet I c r π) :
l.bDistortion = trueπ.distortion c
theorem BoxIntegral.IntegrationParams.MemBaseSet.exists_compl {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} (self : l.MemBaseSet I c r π) :
l.bDistortion = true∃ (π' : ), π'.iUnion = I \ π.iUnion π'.distortion c
def BoxIntegral.IntegrationParams.RCond {ι : Type u_2} (r : (ι)()) :

A predicate saying that in case l.bRiemann = true, the function r is a constant.

Equations
• l.RCond r = (l.bRiemann = true∀ (x : ι), r x = r 0)
Instances For

A set s : Set (TaggedPrepartition I) belongs to l.toFilterDistortion I c if there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = true) such that s contains each prepartition π such that l.MemBaseSet I c r π.

Equations
• l.toFilterDistortion I c = ⨅ (r : (ι)()), ⨅ (_ : l.RCond r), Filter.principal {π : | l.MemBaseSet I c r π}
Instances For
def BoxIntegral.IntegrationParams.toFilter {ι : Type u_1} [] (I : ) :

A set s : Set (TaggedPrepartition I) belongs to l.toFilter I if for any c : ℝ≥0 there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = true) such that s contains each prepartition π such that l.MemBaseSet I c r π.

Equations
• l.toFilter I = ⨆ (c : NNReal), l.toFilterDistortion I c
Instances For
def BoxIntegral.IntegrationParams.toFilterDistortioniUnion {ι : Type u_1} [] (I : ) (c : NNReal) (π₀ : ) :

A set s : Set (TaggedPrepartition I) belongs to l.toFilterDistortioniUnion I c π₀ if there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = true) such that s contains each prepartition π such that l.MemBaseSet I c r π and π.iUnion = π₀.iUnion.

Equations
• l.toFilterDistortioniUnion I c π₀ = l.toFilterDistortion I c Filter.principal {π : | π.iUnion = π₀.iUnion}
Instances For
def BoxIntegral.IntegrationParams.toFilteriUnion {ι : Type u_1} [] (I : ) (π₀ : ) :

A set s : Set (TaggedPrepartition I) belongs to l.toFilteriUnion I π₀ if for any c : ℝ≥0 there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = true) such that s contains each prepartition π such that l.MemBaseSet I c r π and π.iUnion = π₀.iUnion.

Equations
• l.toFilteriUnion I π₀ = ⨆ (c : NNReal), l.toFilterDistortioniUnion I c π₀
Instances For
theorem BoxIntegral.IntegrationParams.rCond_of_bRiemann_eq_false {ι : Type u_2} (hl : l.bRiemann = false) {r : (ι)()} :
l.RCond r
theorem BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq {ι : Type u_1} [] (I : ) (π₀ : ) :
l.toFilter I Filter.principal {π : | π.iUnion = π₀.iUnion} = l.toFilteriUnion I π₀
theorem BoxIntegral.IntegrationParams.MemBaseSet.mono' {ι : Type u_1} [] {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)()} {r₂ : (ι)()} (I : ) (h : l₁ l₂) (hc : c₁ c₂) (hr : Jπ, r₁ (π.tag J) r₂ (π.tag J)) (hπ : l₁.MemBaseSet I c₁ r₁ π) :
l₂.MemBaseSet I c₂ r₂ π
theorem BoxIntegral.IntegrationParams.MemBaseSet.mono {ι : Type u_1} [] {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)()} {r₂ : (ι)()} (I : ) (h : l₁ l₂) (hc : c₁ c₂) (hr : xBoxIntegral.Box.Icc I, r₁ x r₂ x) (hπ : l₁.MemBaseSet I c₁ r₁ π) :
l₂.MemBaseSet I c₂ r₂ π
theorem BoxIntegral.IntegrationParams.MemBaseSet.exists_common_compl {ι : Type u_1} [] {I : } {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)()} {r₂ : (ι)()} {π₁ : } {π₂ : } (h₁ : l.MemBaseSet I c₁ r₁ π₁) (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) :
∃ (π : ), π.iUnion = I \ π₁.iUnion (l.bDistortion = trueπ.distortion c₁) (l.bDistortion = trueπ.distortion c₂)
theorem BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate {ι : Type u_1} [] {I : } {c : NNReal} {r₁ : (ι)()} {r₂ : (ι)()} {π₁ : } (hπ₁ : l.MemBaseSet I c r₁ π₁) (hle : xBoxIntegral.Box.Icc I, r₂ x r₁ x) {π₂ : } (hU : π₂.iUnion = I \ π₁.iUnion) (hc : l.bDistortion = trueπ₂.distortion c) :
l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂)
theorem BoxIntegral.IntegrationParams.MemBaseSet.filter {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} (hπ : l.MemBaseSet I c r π) (p : ) :
l.MemBaseSet I c r (π.filter p)
theorem BoxIntegral.IntegrationParams.biUnionTagged_memBaseSet {ι : Type u_1} [] {I : } {c : NNReal} {r : (ι)()} {π : } {πi : } (h : Jπ, l.MemBaseSet J c r (πi J)) (hp : Jπ, (πi J).IsPartition) (hc : l.bDistortion = trueπ.compl.distortion c) :
l.MemBaseSet I c r (π.biUnionTagged πi)
theorem BoxIntegral.IntegrationParams.RCond.mono {ι : Type u_2} {r : (ι)()} (h : l₁ l₂) (hr : l₂.RCond r) :
l₁.RCond r
theorem BoxIntegral.IntegrationParams.RCond.min {ι : Type u_2} {r₁ : (ι)()} {r₂ : (ι)()} (h₁ : l.RCond r₁) (h₂ : l.RCond r₂) :
l.RCond fun (x : ι) => min (r₁ x) (r₂ x)
theorem BoxIntegral.IntegrationParams.toFilterDistortion_mono {ι : Type u_1} [] {c₁ : NNReal} {c₂ : NNReal} (I : ) (h : l₁ l₂) (hc : c₁ c₂) :
l₁.toFilterDistortion I c₁ l₂.toFilterDistortion I c₂
theorem BoxIntegral.IntegrationParams.toFilter_mono {ι : Type u_1} [] (I : ) (h : l₁ l₂) :
l₁.toFilter I l₂.toFilter I
theorem BoxIntegral.IntegrationParams.toFilteriUnion_mono {ι : Type u_1} [] (I : ) (h : l₁ l₂) (π₀ : ) :
l₁.toFilteriUnion I π₀ l₂.toFilteriUnion I π₀
theorem BoxIntegral.IntegrationParams.toFilteriUnion_congr {ι : Type u_1} [] (I : ) {π₁ : } {π₂ : } (h : π₁.iUnion = π₂.iUnion) :
l.toFilteriUnion I π₁ = l.toFilteriUnion I π₂
theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion {ι : Type u_1} [] (I : ) (c : NNReal) :
(l.toFilterDistortion I c).HasBasis l.RCond fun (r : (ι)()) => {π : | l.MemBaseSet I c r π}
theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion {ι : Type u_1} [] (I : ) (c : NNReal) (π₀ : ) :
(l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun (r : (ι)()) => {π : | l.MemBaseSet I c r π π.iUnion = π₀.iUnion}
theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion {ι : Type u_1} [] (I : ) (π₀ : ) :
(l.toFilteriUnion I π₀).HasBasis (fun (r : NNReal(ι)()) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)()) => {π : | ∃ (c : NNReal), l.MemBaseSet I c (r c) π π.iUnion = π₀.iUnion}
theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top {ι : Type u_1} [] (I : ) :
(l.toFilteriUnion I ).HasBasis (fun (r : NNReal(ι)()) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)()) => {π : | ∃ (c : NNReal), l.MemBaseSet I c (r c) π π.IsPartition}
theorem BoxIntegral.IntegrationParams.hasBasis_toFilter {ι : Type u_1} [] (I : ) :
(l.toFilter I).HasBasis (fun (r : NNReal(ι)()) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)()) => {π : | ∃ (c : NNReal), l.MemBaseSet I c (r c) π}
theorem BoxIntegral.IntegrationParams.tendsto_embedBox_toFilteriUnion_top {ι : Type u_1} [] {I : } {J : } (h : I J) :
Filter.Tendsto () (l.toFilteriUnion I ) (l.toFilteriUnion J ())
theorem BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq {ι : Type u_1} [] {I : } {c : NNReal} (π₀ : ) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) (r : (ι)()) :
∃ (π : ), l.MemBaseSet I c r π π.toPrepartition π₀ π.iUnion = π₀.iUnion
theorem BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition {ι : Type u_1} [] {c : NNReal} (I : ) (hc : I.distortion c) (r : (ι)()) :
∃ (π : ), l.MemBaseSet I c r π π.IsPartition
theorem BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot {ι : Type u_1} [] {c : NNReal} (I : ) (π₀ : ) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) :
(l.toFilterDistortioniUnion I c π₀).NeBot
instance BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot' {ι : Type u_1} [] (I : ) (π₀ : ) :
(l.toFilterDistortioniUnion I (max π₀.distortion π₀.compl.distortion) π₀).NeBot
Equations
• =
instance BoxIntegral.IntegrationParams.toFilterDistortion_neBot {ι : Type u_1} [] (I : ) :
(l.toFilterDistortion I I.distortion).NeBot
Equations
• =
instance BoxIntegral.IntegrationParams.toFilter_neBot {ι : Type u_1} [] (I : ) :
(l.toFilter I).NeBot
Equations
• =
instance BoxIntegral.IntegrationParams.toFilteriUnion_neBot {ι : Type u_1} [] (I : ) (π₀ : ) :
(l.toFilteriUnion I π₀).NeBot
Equations
• =
theorem BoxIntegral.IntegrationParams.eventually_isPartition {ι : Type u_1} [] (I : ) :
∀ᶠ (π : ) in l.toFilteriUnion I , π.IsPartition