Documentation

Mathlib.Analysis.BoxIntegral.Basic

Integrals of Riemann, Henstock-Kurzweil, and McShane #

In this file we define the integral of a function over a box in ℝⁿ. The same definition works for Riemann, Henstock-Kurzweil, and McShane integrals.

As usual, we represent ℝⁿ as the type of functions ι → ℝ for some finite type ι. A rectangular box (l, u] in ℝⁿ is defined to be the set {x : ι → ℝ | ∀ i, l i < x i ∧ x i ≤ u i}, see BoxIntegral.Box.

Let vol be a box-additive function on boxes in ℝⁿ with codomain E →L[ℝ] F. Given a function f : ℝⁿ → E, a box I and a tagged partition π of this box, the integral sum of f over π with respect to the volume vol is the sum of vol J (f (π.tag J)) over all boxes of π. Here π.tag J is the point (tag) in ℝⁿ associated with the box J.

The integral is defined as the limit of integral sums along a filter. Different filters correspond to different integration theories. In order to avoid code duplication, all our definitions and theorems take an argument l : BoxIntegral.IntegrationParams. This is a type that holds three boolean values, and encodes eight filters including those corresponding to Riemann, Henstock-Kurzweil, and McShane integrals.

Following the design of infinite sums (see hasSum and tsum), we define a predicate BoxIntegral.HasIntegral and a function BoxIntegral.integral that returns a vector satisfying the predicate or zero if the function is not integrable.

Then we prove some basic properties of box integrals (linearity, a formula for the integral of a constant). We also prove a version of the Henstock-Sacks inequality (see BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet and BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq), prove integrability of continuous functions, and provide a criterion for integrability w.r.t. a non-Riemann filter (e.g., Henstock-Kurzweil and McShane).

Notation #

Tags #

integral

Integral sum and its basic properties #

The integral sum of f : ℝⁿ → E over a tagged prepartition π w.r.t. box-additive volume vol with codomain E →L[ℝ] F is the sum of vol J (f (π.tag J)) over all boxes of π.

Equations
Instances For
    theorem BoxIntegral.integralSum_biUnionTagged {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) (π : BoxIntegral.Prepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.TaggedPrepartition J) :
    BoxIntegral.integralSum f vol (π.biUnionTagged πi) = Jπ.boxes, BoxIntegral.integralSum f vol (πi J)
    theorem BoxIntegral.integralSum_biUnion_partition {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) (π : BoxIntegral.TaggedPrepartition I) (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J) (hπi : Jπ, (πi J).IsPartition) :
    BoxIntegral.integralSum f vol (π.biUnionPrepartition πi) = BoxIntegral.integralSum f vol π
    theorem BoxIntegral.integralSum_inf_partition {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) (π : BoxIntegral.TaggedPrepartition I) {π' : BoxIntegral.Prepartition I} (h : π'.IsPartition) :
    BoxIntegral.integralSum f vol (π.infPrepartition π') = BoxIntegral.integralSum f vol π
    theorem BoxIntegral.integralSum_fiberwise {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} {α : Type u_1} (g : BoxIntegral.Box ια) (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) (π : BoxIntegral.TaggedPrepartition I) :
    yFinset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun (x : BoxIntegral.Box ι) => g x = y) = BoxIntegral.integralSum f vol π
    theorem BoxIntegral.integralSum_sub_partitions {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h₁ : π₁.IsPartition) (h₂ : π₂.IsPartition) :
    BoxIntegral.integralSum f vol π₁ - BoxIntegral.integralSum f vol π₂ = J(π₁.toPrepartition π₂.toPrepartition).boxes, ((vol J) (f ((π₁.infPrepartition π₂.toPrepartition).tag J)) - (vol J) (f ((π₂.infPrepartition π₁.toPrepartition).tag J)))
    @[simp]
    theorem BoxIntegral.integralSum_disjUnion {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : Disjoint π₁.iUnion π₂.iUnion) :
    BoxIntegral.integralSum f vol (π₁.disjUnion π₂ h) = BoxIntegral.integralSum f vol π₁ + BoxIntegral.integralSum f vol π₂
    @[simp]
    theorem BoxIntegral.integralSum_add {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} (f : (ι)E) (g : (ι)E) (vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) ) (π : BoxIntegral.TaggedPrepartition I) :

    Basic integrability theory #

    The predicate HasIntegral I l f vol y says that y is the integral of f over I along l w.r.t. volume vol. This means that integral sums of f tend to 𝓝 y along BoxIntegral.IntegrationParams.toFilteriUnion I ⊤.

    Equations
    Instances For

      A function is integrable if there exists a vector that satisfies the HasIntegral predicate.

      Equations
      Instances For

        The integral of a function f over a box I along a filter l w.r.t. a volume vol. Returns zero on non-integrable functions.

        Equations
        Instances For

          Reinterpret BoxIntegral.HasIntegral as Filter.Tendsto, e.g., dot-notation theorems that are shadowed in the BoxIntegral.HasIntegral namespace.

          theorem BoxIntegral.hasIntegral_iff {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} :
          BoxIntegral.HasIntegral I l f vol y ε > 0, ∃ (r : NNReal(ι)(Set.Ioi 0)), (∀ (c : NNReal), l.RCond (r c)) ∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c (r c) ππ.IsPartitiondist (BoxIntegral.integralSum f vol π) y ε

          The ε-δ definition of BoxIntegral.HasIntegral.

          theorem BoxIntegral.HasIntegral.of_mul {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} (a : ) (h : ∀ (ε : ), 0 < ε∃ (r : NNReal(ι)(Set.Ioi 0)), (∀ (c : NNReal), l.RCond (r c)) ∀ (c : NNReal) (π : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c (r c) ππ.IsPartitiondist (BoxIntegral.integralSum f vol π) y a * ε) :

          Quite often it is more natural to prove an estimate of the form a * ε, not ε in the RHS of BoxIntegral.hasIntegral_iff, so we provide this auxiliary lemma.

          theorem BoxIntegral.integrable_iff_cauchy_basis {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } [CompleteSpace F] :
          BoxIntegral.Integrable I l f vol ε > 0, ∃ (r : NNReal(ι)(Set.Ioi 0)), (∀ (c : NNReal), l.RCond (r c)) ∀ (c₁ c₂ : NNReal) (π₁ π₂ : BoxIntegral.TaggedPrepartition I), l.MemBaseSet I c₁ (r c₁) π₁π₁.IsPartitionl.MemBaseSet I c₂ (r c₂) π₂π₂.IsPartitiondist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ε

          In a complete space, a function is integrable if and only if its integral sums form a Cauchy net. Here we restate this fact in terms of ∀ ε > 0, ∃ r, ....

          theorem BoxIntegral.HasIntegral.mono {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} {l₁ : BoxIntegral.IntegrationParams} {l₂ : BoxIntegral.IntegrationParams} (h : BoxIntegral.HasIntegral I l₁ f vol y) (hl : l₂ l₁) :
          theorem BoxIntegral.HasIntegral.unique {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} {y' : F} (h : BoxIntegral.HasIntegral I l f vol y) (h' : BoxIntegral.HasIntegral I l f vol y') :
          y = y'
          theorem BoxIntegral.HasIntegral.add {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} {y' : F} (h : BoxIntegral.HasIntegral I l f vol y) (h' : BoxIntegral.HasIntegral I l g vol y') :
          BoxIntegral.HasIntegral I l (f + g) vol (y + y')
          theorem BoxIntegral.Integrable.add {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hf : BoxIntegral.Integrable I l f vol) (hg : BoxIntegral.Integrable I l g vol) :
          theorem BoxIntegral.integral_add {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hf : BoxIntegral.Integrable I l f vol) (hg : BoxIntegral.Integrable I l g vol) :
          theorem BoxIntegral.HasIntegral.neg {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} (hf : BoxIntegral.HasIntegral I l f vol y) :
          theorem BoxIntegral.HasIntegral.sub {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} {y' : F} (h : BoxIntegral.HasIntegral I l f vol y) (h' : BoxIntegral.HasIntegral I l g vol y') :
          BoxIntegral.HasIntegral I l (f - g) vol (y - y')
          theorem BoxIntegral.Integrable.sub {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hf : BoxIntegral.Integrable I l f vol) (hg : BoxIntegral.Integrable I l g vol) :
          theorem BoxIntegral.integral_sub {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hf : BoxIntegral.Integrable I l f vol) (hg : BoxIntegral.Integrable I l g vol) :
          theorem BoxIntegral.hasIntegral_const {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (c : E) :
          BoxIntegral.HasIntegral I l (fun (x : ι) => c) vol ((vol I) c)
          @[simp]
          theorem BoxIntegral.integral_const {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (c : E) :
          BoxIntegral.integral I l (fun (x : ι) => c) vol = (vol I) c
          theorem BoxIntegral.HasIntegral.sum {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {α : Type u_1} {s : Finset α} {f : α(ι)E} {g : αF} (h : is, BoxIntegral.HasIntegral I l (f i) vol (g i)) :
          BoxIntegral.HasIntegral I l (fun (x : ι) => is, f i x) vol (∑ is, g i)
          theorem BoxIntegral.HasIntegral.smul {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {y : F} (hf : BoxIntegral.HasIntegral I l f vol y) (c : ) :
          BoxIntegral.HasIntegral I l (c f) vol (c y)
          theorem BoxIntegral.Integrable.of_smul {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {c : } (hf : BoxIntegral.Integrable I l (c f) vol) (hc : c 0) :
          @[simp]
          theorem BoxIntegral.integral_smul {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (c : ) :
          BoxIntegral.integral I l (fun (x : ι) => c f x) vol = c BoxIntegral.integral I l f vol
          theorem BoxIntegral.integral_nonneg {ι : Type u} {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {g : (ι)} (hg : xBoxIntegral.Box.Icc I, 0 g x) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] :
          0 BoxIntegral.integral I l g μ.toBoxAdditive.toSMul

          The integral of a nonnegative function w.r.t. a volume generated by a locally-finite measure is nonnegative.

          theorem BoxIntegral.norm_integral_le_of_norm_le {ι : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace E] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {g : (ι)} (hle : xBoxIntegral.Box.Icc I, f x g x) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] (hg : BoxIntegral.Integrable I l g μ.toBoxAdditive.toSMul) :
          BoxIntegral.integral I l f μ.toBoxAdditive.toSMul BoxIntegral.integral I l g μ.toBoxAdditive.toSMul

          If ‖f x‖ ≤ g x on [l, u] and g is integrable, then the norm of the integral of f is less than or equal to the integral of g.

          theorem BoxIntegral.norm_integral_le_of_le_const {ι : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace E] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {c : } (hc : xBoxIntegral.Box.Icc I, f x c) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] :
          BoxIntegral.integral I l f μ.toBoxAdditive.toSMul (μ I).toReal * c

          Henstock-Sacks inequality and integrability on subboxes #

          Henstock-Sacks inequality for Henstock-Kurzweil integral says the following. Let f be a function integrable on a box I; let r : ℝⁿ → (0, ∞) be a function such that for any tagged partition of I subordinate to r, the integral sum over this partition is ε-close to the integral. Then for any tagged prepartition (i.e. a finite collections of pairwise disjoint subboxes of I with tagged points) π, the integral sum over π differs from the integral of f over the part of I covered by π by at most ε. The actual statement in the library is a bit more complicated to make it work for any BoxIntegral.IntegrationParams. We formalize several versions of this inequality in BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet, BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq, and BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet.

          Instead of using predicate assumptions on r, we define BoxIntegral.Integrable.convergenceR (h : integrable I l f vol) (ε : ℝ) (c : ℝ≥0) : ℝⁿ → (0, ∞) to be a function r such that

          The proof is mostly based on [Russel A. Gordon, The integrals of Lebesgue, Denjoy, Perron, and Henstock][Gordon55].

          def BoxIntegral.Integrable.convergenceR {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (h : BoxIntegral.Integrable I l f vol) (ε : ) :
          NNReal(ι)(Set.Ioi 0)

          If ε > 0, then BoxIntegral.Integrable.convergenceR is a function r : ℝ≥0 → ℝⁿ → (0, ∞) such that for every c : ℝ≥0, for every tagged partition π subordinate to r (and satisfying additional distortion estimates if BoxIntegral.IntegrationParams.bDistortion l = true), the corresponding integral sum is ε-close to the integral.

          If BoxIntegral.IntegrationParams.bRiemann = true, then r c x does not depend on x. If ε ≤ 0, then we use r c x = 1.

          Equations
          Instances For
            theorem BoxIntegral.Integrable.convergenceR_cond {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (h : BoxIntegral.Integrable I l f vol) (ε : ) (c : NNReal) :
            l.RCond (h.convergenceR ε c)
            theorem BoxIntegral.Integrable.dist_integralSum_integral_le_of_memBaseSet {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {c : NNReal} {ε : } (h : BoxIntegral.Integrable I l f vol) (h₀ : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) (hπp : π.IsPartition) :
            theorem BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {c₁ : NNReal} {c₂ : NNReal} {ε₁ : } {ε₂ : } {π₁ : BoxIntegral.TaggedPrepartition I} {π₂ : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.Integrable I l f vol) (hpos₁ : 0 < ε₁) (hpos₂ : 0 < ε₂) (h₁ : l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁) (h₂ : l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂) (HU : π₁.iUnion = π₂.iUnion) :
            dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ε₁ + ε₂

            Henstock-Sacks inequality. Let r₁ r₂ : ℝⁿ → (0, ∞) be a function such that for any tagged partition of I subordinate to rₖ, k=1,2, the integral sum of f over this partition differs from the integral of f by at most εₖ. Then for any two tagged prepartition π₁ π₂ subordinate to r₁ and r₂ respectively and covering the same part of I, the integral sums of f over these prepartitions differ from each other by at most ε₁ + ε₂.

            The actual statement

            See also BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq and BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet.

            If f is integrable on I along l, then for two sufficiently fine tagged prepartitions (in the sense of the filter BoxIntegral.IntegrationParams.toFilter l I) such that they cover the same part of I, the integral sums of f over π₁ and π₂ are very close to each other.

            If f is integrable on a box I along l, then for any fixed subset s of I that can be represented as a finite union of boxes, the integral sums of f over tagged prepartitions that cover exactly s form a Cauchy “sequence” along l.

            If f is integrable on a box I, then it is integrable on any subbox of I.

            If f is integrable on a box I, then integral sums of f over tagged prepartitions that cover exactly a subbox J ≤ I tend to the integral of f over J along l.

            theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {c : NNReal} {ε : } [CompleteSpace F] (h : BoxIntegral.Integrable I l f vol) (h0 : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) {π₀ : BoxIntegral.Prepartition I} (hU : π.iUnion = π₀.iUnion) :
            dist (BoxIntegral.integralSum f vol π) (∑ Jπ₀.boxes, BoxIntegral.integral J l f vol) ε

            Henstock-Sacks inequality. Let r : ℝⁿ → (0, ∞) be a function such that for any tagged partition of I subordinate to r, the integral sum of f over this partition differs from the integral of f by at most ε. Then for any tagged prepartition π subordinate to r, the integral sum of f over this prepartition differs from the integral of f over the part of I covered by π by at most ε.

            The actual statement

            theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } {c : NNReal} {ε : } [CompleteSpace F] (h : BoxIntegral.Integrable I l f vol) (h0 : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) :
            dist (BoxIntegral.integralSum f vol π) (∑ Jπ.boxes, BoxIntegral.integral J l f vol) ε

            Henstock-Sacks inequality. Let r : ℝⁿ → (0, ∞) be a function such that for any tagged partition of I subordinate to r, the integral sum of f over this partition differs from the integral of f by at most ε. Then for any tagged prepartition π subordinate to r, the integral sum of f over this prepartition differs from the integral of f over the part of I covered by π by at most ε.

            The actual statement

            Integral sum of f over a tagged prepartition π such that π.Union = π₀.Union tends to the sum of integrals of f over the boxes of π₀.

            theorem BoxIntegral.Integrable.sum_integral_congr {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } [CompleteSpace F] (h : BoxIntegral.Integrable I l f vol) {π₁ : BoxIntegral.Prepartition I} {π₂ : BoxIntegral.Prepartition I} (hU : π₁.iUnion = π₂.iUnion) :
            Jπ₁.boxes, BoxIntegral.integral J l f vol = Jπ₂.boxes, BoxIntegral.integral J l f vol

            If f is integrable on I, then fun J ↦ integral J l f vol is box-additive on subboxes of I: if π₁, π₂ are two prepartitions of I covering the same part of I, the sum of integrals of f over the boxes of π₁ is equal to the sum of integrals of f over the boxes of π₂.

            See also BoxIntegral.Integrable.toBoxAdditive for a bundled version.

            @[simp]

            If f is integrable on I, then fun J ↦ integral J l f vol is box-additive on subboxes of I: if π₁, π₂ are two prepartitions of I covering the same part of I, the sum of integrals of f over the boxes of π₁ is equal to the sum of integrals of f over the boxes of π₂.

            See also BoxIntegral.Integrable.sum_integral_congr for an unbundled version.

            Equations
            Instances For

              Integrability conditions #

              theorem BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAt {ι : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace E] [Fintype ι] (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι)E} (hb : ∃ (C : ), xBoxIntegral.Box.Icc I, f x C) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] (hc : ∀ᵐ (x : ι) ∂μ.restrict (BoxIntegral.Box.Icc I), ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) :
              BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul

              A function that is bounded and a.e. continuous on a box I is integrable on I.

              theorem BoxIntegral.integrable_of_bounded_and_ae_continuous {ι : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace E] [Fintype ι] (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι)E} (hb : ∃ (C : ), xBoxIntegral.Box.Icc I, f x C) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] (hc : ∀ᵐ (x : ι) ∂μ, ContinuousAt f x) :
              BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul

              A function that is bounded on a box I and a.e. continuous is integrable on I.

              This is a version of integrable_of_bounded_and_ae_continuousWithinAt with a stronger continuity assumption so that the user does not need to specialize the continuity assumption to each box on which the theorem is to be applied.

              theorem BoxIntegral.integrable_of_continuousOn {ι : Type u} {E : Type v} [NormedAddCommGroup E] [NormedSpace E] [Fintype ι] (l : BoxIntegral.IntegrationParams) [CompleteSpace E] {I : BoxIntegral.Box ι} {f : (ι)E} (hc : ContinuousOn f (BoxIntegral.Box.Icc I)) (μ : MeasureTheory.Measure (ι)) [MeasureTheory.IsLocallyFiniteMeasure μ] :
              BoxIntegral.Integrable I l f μ.toBoxAdditive.toSMul

              A continuous function is box-integrable with respect to any locally finite measure.

              This is true for any volume with bounded variation.

              theorem BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hl : l.bRiemann = false) (B : BoxIntegral.BoxAdditiveMap ι I) (hB0 : ∀ (J : BoxIntegral.Box ι), 0 B J) (g : BoxIntegral.BoxAdditiveMap ι F I) (s : Set (ι)) (hs : s.Countable) (hlH : s.Nonemptyl.bHenstock = true) (H₁ : ∀ (c : NNReal), xBoxIntegral.Box.Icc I s, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J Metric.closedBall x δx BoxIntegral.Box.Icc J(l.bDistortion = trueJ.distortion c)dist ((vol J) (f x)) (g J) ε) (H₂ : ∀ (c : NNReal), xBoxIntegral.Box.Icc I \ s, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J Metric.closedBall x δ(l.bHenstock = truex BoxIntegral.Box.Icc J)(l.bDistortion = trueJ.distortion c)dist ((vol J) (f x)) (g J) ε * B J) :
              BoxIntegral.HasIntegral I l f vol (g I)

              This is an auxiliary lemma used to prove two statements at once. Use one of the next two lemmas instead.

              theorem BoxIntegral.HasIntegral.of_le_Henstock_of_forall_isLittleO {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {l : BoxIntegral.IntegrationParams} {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (hl : l BoxIntegral.IntegrationParams.Henstock) (B : BoxIntegral.BoxAdditiveMap ι I) (hB0 : ∀ (J : BoxIntegral.Box ι), 0 B J) (g : BoxIntegral.BoxAdditiveMap ι F I) (s : Set (ι)) (hs : s.Countable) (H₁ : ∀ (c : NNReal), xBoxIntegral.Box.Icc I s, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J Metric.closedBall x δx BoxIntegral.Box.Icc J(l.bDistortion = trueJ.distortion c)dist ((vol J) (f x)) (g J) ε) (H₂ : ∀ (c : NNReal), xBoxIntegral.Box.Icc I \ s, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J Metric.closedBall x δx BoxIntegral.Box.Icc J(l.bDistortion = trueJ.distortion c)dist ((vol J) (f x)) (g J) ε * B J) :
              BoxIntegral.HasIntegral I l f vol (g I)

              A function f has Henstock (or ) integral over I is equal to the value of a box-additive function g on I provided that vol J (f x) is sufficiently close to g J for sufficiently small boxes J ∋ x. This lemma is useful to prove, e.g., to prove the Divergence theorem for integral along .

              Let l be either BoxIntegral.IntegrationParams.Henstock or . Let g a box-additive function on subboxes of I. Suppose that there exists a nonnegative box-additive function B and a countable set s with the following property.

              For every c : ℝ≥0, a point x ∈ I.Icc, and a positive ε there exists δ > 0 such that for any box J ≤ I such that

              • x ∈ J.Icc ⊆ Metric.closedBall x δ;
              • if l.bDistortion (i.e., l = ⊥), then the distortion of J is less than or equal to c,

              the distance between the term vol J (f x) of an integral sum corresponding to J and g J is less than or equal to ε if x ∈ s and is less than or equal to ε * B J otherwise.

              Then f is integrable on I along l with integral g I.

              theorem BoxIntegral.HasIntegral.mcShane_of_forall_isLittleO {ι : Type u} {E : Type v} {F : Type w} [NormedAddCommGroup E] [NormedSpace E] [NormedAddCommGroup F] [NormedSpace F] {I : BoxIntegral.Box ι} [Fintype ι] {f : (ι)E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[] F) } (B : BoxIntegral.BoxAdditiveMap ι I) (hB0 : ∀ (J : BoxIntegral.Box ι), 0 B J) (g : BoxIntegral.BoxAdditiveMap ι F I) (H : NNRealxBoxIntegral.Box.Icc I, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J Metric.closedBall x δdist ((vol J) (f x)) (g J) ε * B J) :

              Suppose that there exists a nonnegative box-additive function B with the following property.

              For every c : ℝ≥0, a point x ∈ I.Icc, and a positive ε there exists δ > 0 such that for any box J ≤ I such that

              • J.Icc ⊆ Metric.closedBall x δ;
              • if l.bDistortion (i.e., l = ⊥), then the distortion of J is less than or equal to c,

              the distance between the term vol J (f x) of an integral sum corresponding to J and g J is less than or equal to ε * B J.

              Then f is McShane integrable on I with integral g I.