mathlib documentation

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:

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]
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]

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

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 ι] (l : box_integral.integration_params) (I : box_integral.box ι) (c : ℝ≥0) (r : (ι → )(set.Ioi 0)) (π : box_integral.tagged_prepartition I) :
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} (l : box_integral.integration_params) (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.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₂) {π : 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₂ : ℝ≥0} {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 Ir₁ 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} {l : box_integral.integration_params} (h₁ : l.mem_base_set I c₁ r₁ π₁) (h₂ : l.mem_base_set I c₂ r₂ π₂) (hU : π₁.Union = π₂.Union) :
∃ («π» : box_integral.prepartition I), «π».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)} {π₁ : 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 Ir₂ 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.mem_base_set.filter {ι : Type u_1} [fintype ι] {I : box_integral.box ι} {c : ℝ≥0} {r : (ι → )(set.Ioi 0)} {π : box_integral.tagged_prepartition I} {l : box_integral.integration_params} (hπ : l.mem_base_set I c r «π») (p : box_integral.box ι → 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)} {l : box_integral.integration_params} {π : box_integral.prepartition I} {πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J} (h : ∀ (J : box_integral.box ι), J «π»l.mem_base_set J c r (πi J)) (hp : ∀ (J : box_integral.box ι), 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 {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 : ι → ), 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₂) :
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.has_basis_to_filter_Union {ι : Type u_1} [fintype ι] (l : box_integral.integration_params) (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)), {«π» : box_integral.tagged_prepartition I | ∃ (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 ι] (l : box_integral.integration_params) (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)), {«π» : box_integral.tagged_prepartition I | ∃ (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 ι] (l : box_integral.integration_params) (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)), {«π» : box_integral.tagged_prepartition I | ∃ (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} (l : box_integral.integration_params) (π₀ : box_integral.prepartition I) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) (r : (ι → )(set.Ioi 0)) :
∃ («π» : box_integral.tagged_prepartition I), l.mem_base_set I c r «π» «π».to_prepartition π₀ «π».Union = π₀.Union