mathlib3 documentation

analysis.box_integral.partition.filter

Filters used in box-based integrals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

Well-known sets of parameters #

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

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

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.

Implementation details #

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]

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 box_integral.integration_params.GP = ⊥ = {bRiemann := ff, bHenstock := tt, bDistortion := tt}.

Instances for box_integral.integration_params

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

Equations
@[protected, instance]

The value box_integral.integration_params.GP = ⊥ (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

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

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

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.

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
Instances for box_integral.integration_params.to_filter_distortion

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
Instances for box_integral.integration_params.to_filter

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
Instances for box_integral.integration_params.to_filter_distortion_Union

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
Instances for box_integral.integration_params.to_filter_Union
theorem box_integral.integration_params.mem_base_set.mono' {ι : Type u_1} [fintype ι] {c₁ c₂ : nnreal} {r₁ r₂ : ) (set.Ioi 0)} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : c₁ c₂) {π : box_integral.tagged_prepartition I} (hr : (J : box_integral.box ι), 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₂ : nnreal} {r₁ r₂ : ) (set.Ioi 0)} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : c₁ c₂) {π : box_integral.tagged_prepartition I} (hr : (x : ι ), x box_integral.box.Icc I 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₂ : nnreal} {r₁ r₂ : ) (set.Ioi 0)} {π₁ π₂ : box_integral.tagged_prepartition I} {l : box_integral.integration_params} (h₁ : l.mem_base_set I c₁ r₁ π₁) (h₂ : l.mem_base_set I c₂ r₂ π₂) (hU : π₁.Union = π₂.Union) :
@[protected]
theorem box_integral.integration_params.mem_base_set.union_compl_to_subordinate {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : nnreal} {r₁ r₂ : ) (set.Ioi 0)} {π₁ : box_integral.tagged_prepartition I} {l : box_integral.integration_params} (hπ₁ : l.mem_base_set I c r₁ π₁) (hle : (x : ι ), x box_integral.box.Icc I r₂ x r₁ x) {π₂ : box_integral.prepartition I} (hU : π₂.Union = I \ π₁.Union) (hc : (l.bDistortion) π₂.distortion c) :
l.mem_base_set I c r₁ (π₁.union_compl_to_subordinate π₂ hU r₂)
@[protected]
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 {l : box_integral.integration_params} {ι : Type u_1} {r₁ r₂ : ) (set.Ioi 0)} (h₁ : l.r_cond r₁) (h₂ : l.r_cond r₂) :
l.r_cond (λ (x : ι ), linear_order.min (r₁ x) (r₂ x))
theorem box_integral.integration_params.to_filter_distortion_mono {ι : Type u_1} [fintype ι] {c₁ c₂ : nnreal} {l₁ l₂ : box_integral.integration_params} (I : box_integral.box ι) (h : l₁ l₂) (hc : 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