# mathlibdocumentation

analysis.box_integral.partition.filter

# Filters used in box-based integrals #

First we define a structure box_integral.integration_params. This structure will be used as an argument in the definition of box_integral.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 mathlib. 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 : box_integral.integration_params and a rectangular box I : box_integral.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 box_integral.integration_params with a bounded_order structure such that larger integration_params produce larger filters.

## Main definitions #

### Integration parameters #

The structure box_integral.integration_params has 3 boolean fields with the following meaning:

• bRiemann: the value tt 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 ff means that the estimate may depend on the position of the tag.

• bHenstock: the value tt means that we require that each tag belongs to its own closed box; the value ff means that we only require that tags belong to the ambient box.

• bDistortion: the value tt 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 ⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}.

### Well-known sets of parameters #

Out of eight possible values of box_integral.integration_params, the following four are used in the library.

• box_integral.integration_params.Riemann (bRiemann = tt, bHenstock = tt, bDistortion = ff): 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.

• box_integral.integration_params.Henstock (bRiemann = ff, bHenstock = tt, bDistortion = ff): 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.

• box_integral.integration_params.McShane (bRiemann = ff, bHenstock = ff, bDistortion = ff): 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.

• ⊥ (bRiemann = ff, bHenstock = tt, bDistortion = tt): 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 ⊥-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 tagged_prepartition I#

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

structure box_integral.integration_params.mem_base_set (l : box_integral.integration_params)
(I : box_integral.box ι) (c : ℝ≥0) (r : (ι → ℝ) → Ioi (0 : ℝ))
(π : box_integral.tagged_prepartition I) : Prop :=


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 \ π.Union.

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

Then we define a predicate box_integral.integration_params.r_cond 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., box_integral.integration_params.r_cond.min says that the pointwise minimum of two functions that satisfy this condition satisfies this condition as well.

Then we define four filters on box_integral.tagged_prepartition I.

• box_integral.integration_params.to_filter_distortion: an auxiliary filter that takes parameters (l : box_integral.integration_params) (I : box_integral.box ι) (c : ℝ≥0) and returns the filter generated by all sets {π | mem_base_set l I c r π}, where r is a function satisfying the predicate box_integral.integration_params.r_cond l;

• box_integral.integration_params.to_filter l I: the supremum of l.to_filter_distortion I c over all c : ℝ≥0;

• box_integral.integration_params.to_filter_distortion_Union l I c π₀, where π₀ is a prepartition of I: the infimum of l.to_filter_distortion I c and the principal filter generated by {π | π.Union = π₀.Union};

• box_integral.integration_params.to_filter_Union l I π₀: the supremum of l.to_filter_distortion_Union 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 box_integral.integration_params.to_filter_Union l I ⊤. While it is possible to define the integral with a general filter on box_integral.tagged_prepartition 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 box_integral.integration_params.to_filter_Union l I ⊤ and partitions of a box, some lemmas (e.g., the Henstock-Sacks lemmas) are best formulated in terms of the predicate mem_base_set and other filters defined above.

• We use bool instead of Prop for the fields of integration_params in order to have decidable equality and inequalities.

## TODO #

Currently, box_integral.integration_params.mem_base_set explicitly requires that there exists a partition of the complement I \ π.Union with distortion ≤ c. For c > 1, this condition is always true but the proof of this fact requires more API about box_integral.prepartition.split_many. 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

@[ext]
structure box_integral.integration_params  :
Type

An integration_params 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 tt 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 ff means that the estimate may depend on the position of the tag.

• bHenstock: the value tt means that we require that each tag belongs to its own closed box; the value ff means that we only require that tags belong to the ambient box.

• bDistortion: the value tt 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 ⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}.

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

Equations
@[protected, instance]
Equations

Auxiliary order_iso with a product type used to lift a bounded_order structure.

Equations
@[protected, instance]
Equations
@[protected, instance]

The value ⊥ (bRiemann = ff, bHenstock = tt, bDistortion = tt) 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
@[protected, instance]
Equations

The box_integral.integration_params 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

The box_integral.integration_params 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

The box_integral.integration_params 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
structure box_integral.integration_params.mem_base_set {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (c : ℝ≥0) (r : (ι → )(set.Ioi 0))  :
Prop

The predicate corresponding to a base set of the filter defined by an integration_params. 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 \ π.Union.

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.

def box_integral.integration_params.r_cond {ι : Type u_1} (r : (ι → )(set.Ioi 0)) :
Prop

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

Equations

A set s : set (tagged_prepartition I) belongs to l.to_filter_distortion I c if there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = tt) such that s contains each prepartition π such that l.mem_base_set I c r π.

Equations

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

Equations

A set s : set (tagged_prepartition I) belongs to l.to_filter_distortion_Union I c π₀ if there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = tt) such that s contains each prepartition π such that l.mem_base_set I c r π and π.Union = π₀.Union.

Equations

A set s : set (tagged_prepartition I) belongs to l.to_filter_Union I π₀ if for any c : ℝ≥0 there exists a function r : ℝⁿ → (0, ∞) (or a constant r if l.bRiemann = tt) such that s contains each prepartition π such that l.mem_base_set I c r π and π.Union = π₀.Union.

Equations
theorem box_integral.integration_params.r_cond_of_bRiemann_eq_ff {ι : Type u_1} (hl : l.bRiemann = ff) {r : (ι → )(set.Ioi 0)} :
l.r_cond r
theorem box_integral.integration_params.to_filter_inf_Union_eq {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (π₀ : box_integral.prepartition I) :
l.to_filter I 𝓟 {«π» : | «π».Union = π₀.Union} = π₀
theorem box_integral.integration_params.mem_base_set.mono' {ι : Type u_1} [fintype ι] {c₁ c₂ : ℝ≥0} {r₁ r₂ : (ι → )(set.Ioi 0)} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : c₁ c₂) (hr : ∀ (J : , J «π»r₁ («π».tag J) r₂ («π».tag J)) (hπ : l₁.mem_base_set I c₁ r₁ «π») :
l₂.mem_base_set I c₂ r₂ «π»
theorem box_integral.integration_params.mem_base_set.mono {ι : Type u_1} [fintype ι] {c₁ c₂ : ℝ≥0} {r₁ r₂ : (ι → )(set.Ioi 0)} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : c₁ c₂) (hr : ∀ (x : ι → ), r₁ x r₂ x) (hπ : l₁.mem_base_set I c₁ r₁ «π») :
l₂.mem_base_set I c₂ r₂ «π»
theorem box_integral.integration_params.mem_base_set.exists_common_compl {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c₁ c₂ : ℝ≥0} {r₁ r₂ : (ι → )(set.Ioi 0)} {π₁ π₂ : box_integral.tagged_prepartition I} (h₁ : l.mem_base_set I c₁ r₁ π₁) (h₂ : l.mem_base_set I c₂ r₂ π₂) (hU : π₁.Union = π₂.Union) :
∃ («π» : , «π».Union = I \ π₁.Union ((l.bDistortion) → «π».distortion c₁) ((l.bDistortion) → «π».distortion c₂)
@[protected]
theorem box_integral.integration_params.mem_base_set.union_compl_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : ℝ≥0} {r₁ r₂ : (ι → )(set.Ioi 0)} (hπ₁ : l.mem_base_set I c r₁ π₁) (hle : ∀ (x : ι → ), r₂ x r₁ x) {π₂ : box_integral.prepartition I} (hU : π₂.Union = I \ π₁.Union) (hc : (l.bDistortion) → π₂.distortion c) :
l.mem_base_set I c r₁ hU r₂)
@[protected]
theorem box_integral.integration_params.mem_base_set.filter {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : ℝ≥0} {r : (ι → )(set.Ioi 0)} (hπ : l.mem_base_set I c r «π») (p : → Prop) :
l.mem_base_set I c r («π».filter p)
theorem box_integral.integration_params.bUnion_tagged_mem_base_set {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : ℝ≥0} {r : (ι → )(set.Ioi 0)} {πi : Π (J : , } (h : ∀ (J : , J «π»l.mem_base_set J c r (πi J)) (hp : ∀ (J : , J «π»(πi J).is_partition) (hc : (l.bDistortion) → «π».compl.distortion c) :
l.mem_base_set I c r («π».bUnion_tagged πi)
theorem box_integral.integration_params.r_cond.mono {l₁ l₂ : box_integral.integration_params} {ι : Type u_1} {r : (ι → )(set.Ioi 0)} (h : l₁ l₂) (hr : l₂.r_cond r) :
l₁.r_cond r
theorem box_integral.integration_params.r_cond.min {ι : Type u_1} {r₁ r₂ : (ι → )(set.Ioi 0)} (h₁ : l.r_cond r₁) (h₂ : l.r_cond r₂) :
l.r_cond (λ (x : ι → ), min (r₁ x) (r₂ x))
theorem box_integral.integration_params.to_filter_distortion_mono {ι : Type u_1} [fintype ι] {c₁ c₂ : ℝ≥0} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : c₁ c₂) :
c₁ c₂
theorem box_integral.integration_params.to_filter_mono {ι : Type u_1} [fintype ι] (I : box_integral.box ι) {l₁ l₂ : box_integral.integration_params} (h : l₁ l₂) :
l₁.to_filter I l₂.to_filter I
theorem box_integral.integration_params.to_filter_Union_mono {ι : Type u_1} [fintype ι] (I : box_integral.box ι) {l₁ l₂ : box_integral.integration_params} (h : l₁ l₂) (π₀ : box_integral.prepartition I) :
l₁.to_filter_Union I π₀ l₂.to_filter_Union I π₀
theorem box_integral.integration_params.to_filter_Union_congr {ι : Type u_1} [fintype ι] (I : box_integral.box ι) {π₁ π₂ : box_integral.prepartition I} (h : π₁.Union = π₂.Union) :
π₁ = π₂
theorem box_integral.integration_params.has_basis_to_filter_distortion {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (c : ℝ≥0) :
c).has_basis l.r_cond (λ (r : (ι → )(set.Ioi 0)), {«π» : | l.mem_base_set I c r «π»})
theorem box_integral.integration_params.has_basis_to_filter_distortion_Union {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (c : ℝ≥0) (π₀ : box_integral.prepartition I) :
π₀).has_basis l.r_cond (λ (r : (ι → )(set.Ioi 0)), {«π» : | l.mem_base_set I c r «π» «π».Union = π₀.Union})
theorem box_integral.integration_params.has_basis_to_filter_Union {ι : Type u_1} [fintype ι] (I : box_integral.box ι) (π₀ : box_integral.prepartition I) :
(l.to_filter_Union I π₀).has_basis (λ (r : ℝ≥0(ι → )(set.Ioi 0)), ∀ (c : ℝ≥0), l.r_cond (r c)) (λ (r : ℝ≥0(ι → )(set.Ioi 0)), {«π» : | ∃ (c : ℝ≥0), l.mem_base_set I c (r c) «π» «π».Union = π₀.Union})
theorem box_integral.integration_params.has_basis_to_filter_Union_top {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :
(l.to_filter_Union I ).has_basis (λ (r : ℝ≥0(ι → )(set.Ioi 0)), ∀ (c : ℝ≥0), l.r_cond (r c)) (λ (r : ℝ≥0(ι → )(set.Ioi 0)), {«π» : | ∃ (c : ℝ≥0), l.mem_base_set I c (r c) «π» «π».is_partition})
theorem box_integral.integration_params.has_basis_to_filter {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :
(l.to_filter I).has_basis (λ (r : ℝ≥0(ι → )(set.Ioi 0)), ∀ (c : ℝ≥0), l.r_cond (r c)) (λ (r : ℝ≥0(ι → )(set.Ioi 0)), {«π» : | ∃ (c : ℝ≥0), l.mem_base_set I c (r c) «π»})
theorem box_integral.integration_params.exists_mem_base_set_le_Union_eq {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : ℝ≥0} (π₀ : box_integral.prepartition I) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) (r : (ι → )(set.Ioi 0)) :
∃ («π» : , l.mem_base_set I c r «π» «π».to_prepartition π₀ «π».Union = π₀.Union
theorem box_integral.integration_params.exists_mem_base_set_is_partition {ι : Type u_1} [fintype ι] {c : ℝ≥0} (I : box_integral.box ι) (hc : I.distortion c) (r : (ι → )(set.Ioi 0)) :
∃ («π» : , l.mem_base_set I c r «π» «π».is_partition
theorem box_integral.integration_params.to_filter_distortion_Union_ne_bot {ι : Type u_1} [fintype ι] {c : ℝ≥0} (I : box_integral.box ι) (π₀ : box_integral.prepartition I) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) :
π₀).ne_bot
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem box_integral.integration_params.eventually_is_partition {ι : Type u_1} [fintype ι] (I : box_integral.box ι) :
∀ᶠ («π» : in , «π».is_partition