Documentation

Mathlib.Analysis.BoxIntegral.Partition.Filter

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:

Well-known sets of parameters #

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

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

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.

Implementation details #

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 : BoxIntegral.IntegrationParams) (y : BoxIntegral.IntegrationParams) :
x = y x.bRiemann = y.bRiemann x.bHenstock = y.bHenstock x.bDistortion = y.bDistortion
theorem BoxIntegral.IntegrationParams.ext (x : BoxIntegral.IntegrationParams) (y : BoxIntegral.IntegrationParams) (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

      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

              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∃ (π' : BoxIntegral.Prepartition I), π'.iUnion = I \ π.iUnion π'.distortion c
              Instances For
                theorem BoxIntegral.IntegrationParams.MemBaseSet.isSubordinate {ι : Type u_1} [Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I} (self : l.MemBaseSet I c r π) :
                π.IsSubordinate r
                theorem BoxIntegral.IntegrationParams.MemBaseSet.isHenstock {ι : Type u_1} [Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I} (self : l.MemBaseSet I c r π) :
                l.bHenstock = trueπ.IsHenstock
                theorem BoxIntegral.IntegrationParams.MemBaseSet.distortion_le {ι : Type u_1} [Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I} (self : l.MemBaseSet I c r π) :
                l.bDistortion = trueπ.distortion c
                theorem BoxIntegral.IntegrationParams.MemBaseSet.exists_compl {ι : Type u_1} [Fintype ι] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I} (self : l.MemBaseSet I c r π) :
                l.bDistortion = true∃ (π' : BoxIntegral.Prepartition I), π'.iUnion = I \ π.iUnion π'.distortion c

                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
                  Instances For

                    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

                      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
                      Instances For

                        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} (l : BoxIntegral.IntegrationParams) (hl : l.bRiemann = false) {r : (ι)(Set.Ioi 0)} :
                          l.RCond r
                          theorem BoxIntegral.IntegrationParams.toFilter_inf_iUnion_eq {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I) :
                          l.toFilter I Filter.principal {π : BoxIntegral.TaggedPrepartition I | π.iUnion = π₀.iUnion} = l.toFilteriUnion I π₀
                          theorem BoxIntegral.IntegrationParams.MemBaseSet.mono' {ι : Type u_1} [Fintype ι] {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (I : BoxIntegral.Box ι) (h : l₁ l₂) (hc : c₁ c₂) {π : BoxIntegral.TaggedPrepartition I} (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} [Fintype ι] {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (I : BoxIntegral.Box ι) (h : l₁ l₂) (hc : c₁ c₂) {π : BoxIntegral.TaggedPrepartition I} (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} [Fintype ι] {I : BoxIntegral.Box ι} {c₁ : NNReal} {c₂ : NNReal} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} {l : BoxIntegral.IntegrationParams} (h₁ : l.MemBaseSet I c₁ r₁ π₁) (h₂ : l.MemBaseSet I c₂ r₂ π₂) (hU : π₁.iUnion = π₂.iUnion) :
                          ∃ (π : BoxIntegral.Prepartition I), π.iUnion = I \ π₁.iUnion (l.bDistortion = trueπ.distortion c₁) (l.bDistortion = trueπ.distortion c₂)
                          theorem BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} {π₁ : BoxIntegral.TaggedPrepartition I} {l : BoxIntegral.IntegrationParams} (hπ₁ : l.MemBaseSet I c r₁ π₁) (hle : xBoxIntegral.Box.Icc I, r₂ x r₁ x) {π₂ : BoxIntegral.Prepartition I} (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} [Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {π : BoxIntegral.TaggedPrepartition I} {l : BoxIntegral.IntegrationParams} (hπ : l.MemBaseSet I c r π) (p : BoxIntegral.Box ιProp) :
                          l.MemBaseSet I c r (π.filter p)
                          theorem BoxIntegral.IntegrationParams.biUnionTagged_memBaseSet {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {r : (ι)(Set.Ioi 0)} {l : BoxIntegral.IntegrationParams} {π : BoxIntegral.Prepartition I} {πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J} (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 {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} {ι : Type u_2} {r : (ι)(Set.Ioi 0)} (h : l₁ l₂) (hr : l₂.RCond r) :
                          l₁.RCond r
                          theorem BoxIntegral.IntegrationParams.RCond.min {l : BoxIntegral.IntegrationParams} {ι : Type u_2} {r₁ : (ι)(Set.Ioi 0)} {r₂ : (ι)(Set.Ioi 0)} (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} [Fintype ι] {c₁ : NNReal} {c₂ : NNReal} {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (I : BoxIntegral.Box ι) (h : l₁ l₂) (hc : c₁ c₂) :
                          l₁.toFilterDistortion I c₁ l₂.toFilterDistortion I c₂
                          theorem BoxIntegral.IntegrationParams.toFilter_mono {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (h : l₁ l₂) :
                          l₁.toFilter I l₂.toFilter I
                          theorem BoxIntegral.IntegrationParams.toFilteriUnion_mono {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (h : l₁ l₂) (π₀ : BoxIntegral.Prepartition I) :
                          l₁.toFilteriUnion I π₀ l₂.toFilteriUnion I π₀
                          theorem BoxIntegral.IntegrationParams.toFilteriUnion_congr {ι : Type u_1} [Fintype ι] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams) {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (h : π₁.iUnion = π₂.iUnion) :
                          l.toFilteriUnion I π₁ = l.toFilteriUnion I π₂
                          theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortion {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal) :
                          (l.toFilterDistortion I c).HasBasis l.RCond fun (r : (ι)(Set.Ioi 0)) => {π : BoxIntegral.TaggedPrepartition I | l.MemBaseSet I c r π}
                          theorem BoxIntegral.IntegrationParams.hasBasis_toFilterDistortioniUnion {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal) (π₀ : BoxIntegral.Prepartition I) :
                          (l.toFilterDistortioniUnion I c π₀).HasBasis l.RCond fun (r : (ι)(Set.Ioi 0)) => {π : BoxIntegral.TaggedPrepartition I | l.MemBaseSet I c r π π.iUnion = π₀.iUnion}
                          theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I) :
                          (l.toFilteriUnion I π₀).HasBasis (fun (r : NNReal(ι)(Set.Ioi 0)) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)(Set.Ioi 0)) => {π : BoxIntegral.TaggedPrepartition I | ∃ (c : NNReal), l.MemBaseSet I c (r c) π π.iUnion = π₀.iUnion}
                          theorem BoxIntegral.IntegrationParams.hasBasis_toFilteriUnion_top {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) :
                          (l.toFilteriUnion I ).HasBasis (fun (r : NNReal(ι)(Set.Ioi 0)) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)(Set.Ioi 0)) => {π : BoxIntegral.TaggedPrepartition I | ∃ (c : NNReal), l.MemBaseSet I c (r c) π π.IsPartition}
                          theorem BoxIntegral.IntegrationParams.hasBasis_toFilter {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) :
                          (l.toFilter I).HasBasis (fun (r : NNReal(ι)(Set.Ioi 0)) => ∀ (c : NNReal), l.RCond (r c)) fun (r : NNReal(ι)(Set.Ioi 0)) => {π : BoxIntegral.TaggedPrepartition I | ∃ (c : NNReal), l.MemBaseSet I c (r c) π}
                          theorem BoxIntegral.IntegrationParams.exists_memBaseSet_le_iUnion_eq {ι : Type u_1} [Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} (l : BoxIntegral.IntegrationParams) (π₀ : BoxIntegral.Prepartition I) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) (r : (ι)(Set.Ioi 0)) :
                          ∃ (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c r π π.toPrepartition π₀ π.iUnion = π₀.iUnion
                          theorem BoxIntegral.IntegrationParams.exists_memBaseSet_isPartition {ι : Type u_1} [Fintype ι] {c : NNReal} (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (hc : I.distortion c) (r : (ι)(Set.Ioi 0)) :
                          ∃ (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c r π π.IsPartition
                          theorem BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot {ι : Type u_1} [Fintype ι] {c : NNReal} (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I) (hc₁ : π₀.distortion c) (hc₂ : π₀.compl.distortion c) :
                          (l.toFilterDistortioniUnion I c π₀).NeBot
                          instance BoxIntegral.IntegrationParams.toFilterDistortioniUnion_neBot' {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I) :
                          (l.toFilterDistortioniUnion I (max π₀.distortion π₀.compl.distortion) π₀).NeBot
                          Equations
                          • =
                          instance BoxIntegral.IntegrationParams.toFilterDistortion_neBot {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) :
                          (l.toFilterDistortion I I.distortion).NeBot
                          Equations
                          • =
                          instance BoxIntegral.IntegrationParams.toFilter_neBot {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) :
                          (l.toFilter I).NeBot
                          Equations
                          • =
                          instance BoxIntegral.IntegrationParams.toFilteriUnion_neBot {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (π₀ : BoxIntegral.Prepartition I) :
                          (l.toFilteriUnion I π₀).NeBot
                          Equations
                          • =
                          theorem BoxIntegral.IntegrationParams.eventually_isPartition {ι : Type u_1} [Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) :
                          ∀ᶠ (π : BoxIntegral.TaggedPrepartition I) in l.toFilteriUnion I , π.IsPartition