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

• ℝⁿ: local notation for ι → ℝ

## Tags #

integral

### Integral sum and its basic properties #

def BoxIntegral.integralSum {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (f : (ι)E) (vol : ) :
F

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
• = Jπ.boxes, (vol J) (f (π.tag J))
Instances For
theorem BoxIntegral.integralSum_biUnionTagged {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (f : (ι)E) (vol : ) (π : ) (πi : ) :
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} [] [] {I : } (f : (ι)E) (vol : ) (πi : (J : ) → ) (hπi : Jπ, (πi J).IsPartition) :
BoxIntegral.integralSum f vol (π.biUnionPrepartition πi) =
theorem BoxIntegral.integralSum_inf_partition {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (f : (ι)E) (vol : ) {π' : } (h : π'.IsPartition) :
BoxIntegral.integralSum f vol (π.infPrepartition π') =
theorem BoxIntegral.integralSum_fiberwise {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } {α : Type u_1} (g : α) (f : (ι)E) (vol : ) :
yFinset.image g π.boxes, BoxIntegral.integralSum f vol (π.filter fun (x : ) => g x = y) =
theorem BoxIntegral.integralSum_sub_partitions {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (f : (ι)E) (vol : ) {π₁ : } {π₂ : } (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} [] [] {I : } (f : (ι)E) (vol : ) {π₁ : } {π₂ : } (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} [] [] {I : } (f : (ι)E) (g : (ι)E) (vol : ) :
@[simp]
theorem BoxIntegral.integralSum_neg {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (f : (ι)E) (vol : ) :
@[simp]
theorem BoxIntegral.integralSum_smul {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } (c : ) (f : (ι)E) (vol : ) :

### Basic integrability theory #

def BoxIntegral.HasIntegral {ι : Type u} {E : Type v} {F : Type w} [] [] [] (I : ) (f : (ι)E) (vol : ) (y : F) :

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
def BoxIntegral.Integrable {ι : Type u} {E : Type v} {F : Type w} [] [] [] (I : ) (f : (ι)E) (vol : ) :

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

Equations
Instances For
def BoxIntegral.integral {ι : Type u} {E : Type v} {F : Type w} [] [] [] (I : ) (f : (ι)E) (vol : ) :
F

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
theorem BoxIntegral.HasIntegral.tendsto {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (h : BoxIntegral.HasIntegral I l f vol y) :
Filter.Tendsto () (l.toFilteriUnion I ) (nhds y)

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} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} :
BoxIntegral.HasIntegral I l f vol y ε > 0, ∃ (r : NNReal(ι)()), (∀ (c : NNReal), l.RCond (r c)) ∀ (c : NNReal) (π : ), l.MemBaseSet I c (r c) ππ.IsPartitiondist () y ε

The ε-δ definition of BoxIntegral.HasIntegral.

theorem BoxIntegral.HasIntegral.of_mul {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (a : ) (h : ∀ (ε : ), 0 < ε∃ (r : NNReal(ι)()), (∀ (c : NNReal), l.RCond (r c)) ∀ (c : NNReal) (π : ), l.MemBaseSet I c (r c) ππ.IsPartitiondist () 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 {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } [] :
BoxIntegral.Integrable I l f vol Cauchy (Filter.map () (l.toFilteriUnion I ))
theorem BoxIntegral.integrable_iff_cauchy_basis {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } [] :
BoxIntegral.Integrable I l f vol ε > 0, ∃ (r : NNReal(ι)()), (∀ (c : NNReal), l.RCond (r c)) ∀ (c₁ c₂ : NNReal) (π₁ π₂ : ), 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} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (h : BoxIntegral.HasIntegral I l₁ f vol y) (hl : l₂ l₁) :
theorem BoxIntegral.Integrable.hasIntegral {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (h : BoxIntegral.Integrable I l f vol) :
theorem BoxIntegral.Integrable.mono {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (h : BoxIntegral.Integrable I l f vol) (hle : l' l) :
theorem BoxIntegral.HasIntegral.unique {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {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.integrable {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (h : BoxIntegral.HasIntegral I l f vol y) :
theorem BoxIntegral.HasIntegral.integral_eq {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (h : BoxIntegral.HasIntegral I l f vol y) :
theorem BoxIntegral.HasIntegral.add {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } {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} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } (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} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } (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} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (hf : BoxIntegral.HasIntegral I l f vol y) :
theorem BoxIntegral.Integrable.neg {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (hf : BoxIntegral.Integrable I l f vol) :
theorem BoxIntegral.Integrable.of_neg {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (hf : BoxIntegral.Integrable I l (-f) vol) :
@[simp]
theorem BoxIntegral.integrable_neg {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } :
@[simp]
theorem BoxIntegral.integral_neg {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } :
theorem BoxIntegral.HasIntegral.sub {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } {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} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } (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} [] [] {I : } [] {f : (ι)E} {g : (ι)E} {vol : } (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} [] [] {I : } [] {vol : } (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} [] [] {I : } [] {vol : } (c : E) :
BoxIntegral.integral I l (fun (x : ι) => c) vol = (vol I) c
theorem BoxIntegral.integrable_const {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {vol : } (c : E) :
BoxIntegral.Integrable I l (fun (x : ι) => c) vol
theorem BoxIntegral.hasIntegral_zero {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {vol : } :
BoxIntegral.HasIntegral I l (fun (x : ι) => 0) vol 0
theorem BoxIntegral.integrable_zero {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {vol : } :
BoxIntegral.Integrable I l (fun (x : ι) => 0) vol
theorem BoxIntegral.integral_zero {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {vol : } :
BoxIntegral.integral I l (fun (x : ι) => 0) vol = 0
theorem BoxIntegral.HasIntegral.sum {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {vol : } {α : Type u_1} {s : } {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} [] [] {I : } [] {f : (ι)E} {vol : } {y : F} (hf : BoxIntegral.HasIntegral I l f vol y) (c : ) :
BoxIntegral.HasIntegral I l (c f) vol (c y)
theorem BoxIntegral.Integrable.smul {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (hf : BoxIntegral.Integrable I l f vol) (c : ) :
theorem BoxIntegral.Integrable.of_smul {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {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} [] [] {I : } [] {f : (ι)E} {vol : } (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 : } [] {g : (ι)} (hg : xBoxIntegral.Box.Icc I, 0 g x) (μ : MeasureTheory.Measure (ι)) :
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} [] {I : } [] {f : (ι)E} {g : (ι)} (hle : xBoxIntegral.Box.Icc I, f x g x) (μ : MeasureTheory.Measure (ι)) (hg : BoxIntegral.Integrable 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} [] {I : } [] {f : (ι)E} {c : } (hc : xBoxIntegral.Box.Icc I, f x c) (μ : MeasureTheory.Measure (ι)) :
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

• if l.bRiemann, then r is a constant;
• if ε > 0, then for any tagged partition π of I subordinate to r (more precisely, satisfying the predicate l.mem_base_set I c r), the integral sum of f over π differs from the integral of f over I by at most ε.

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

def BoxIntegral.Integrable.convergenceR {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (h : BoxIntegral.Integrable I l f vol) (ε : ) :
NNReal(ι)()

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
• h.convergenceR ε = if hε : 0 < ε then .choose else fun (x : NNReal) (x : ι) =>
Instances For
theorem BoxIntegral.Integrable.convergenceR_cond {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (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} [] [] {I : } [] {f : (ι)E} {vol : } {c : NNReal} {ε : } (h : BoxIntegral.Integrable I l f vol) (h₀ : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) (hπp : π.IsPartition) :
dist () (BoxIntegral.integral I l f vol) ε
theorem BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {c₁ : NNReal} {c₂ : NNReal} {ε₁ : } {ε₂ : } {π₁ : } {π₂ : } (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

• uses BoxIntegral.Integrable.convergenceR instead of a predicate assumption on r;
• uses BoxIntegral.IntegrationParams.MemBaseSet instead of “subordinate to r” to account for additional requirements like being a Henstock partition or having a bounded distortion.

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

theorem BoxIntegral.Integrable.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (h : BoxIntegral.Integrable I l f vol) :
Filter.Tendsto (fun (π : ) => (BoxIntegral.integralSum f vol π.1, BoxIntegral.integralSum f vol π.2)) (l.toFilter I ×ˢ l.toFilter I Filter.principal {π : | π.1.iUnion = π.2.iUnion}) ()

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.

theorem BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } (h : BoxIntegral.Integrable I l f vol) (π₀ : ) :
Cauchy (Filter.map () (l.toFilteriUnion I π₀))

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.

theorem BoxIntegral.Integrable.to_subbox_aux {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } {J : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) (hJ : J I) :
∃ (y : F), BoxIntegral.HasIntegral J l f vol y Filter.Tendsto () (l.toFilteriUnion I ()) (nhds y)
theorem BoxIntegral.Integrable.to_subbox {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } {J : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) (hJ : J I) :

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

theorem BoxIntegral.Integrable.tendsto_integralSum_toFilteriUnion_single {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } {J : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) (hJ : J I) :
Filter.Tendsto () (l.toFilteriUnion I ()) (nhds (BoxIntegral.integral J l f vol))

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} [] [] {I : } [] {f : (ι)E} {vol : } {c : NNReal} {ε : } [] (h : BoxIntegral.Integrable I l f vol) (h0 : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) {π₀ : } (hU : π.iUnion = π₀.iUnion) :
dist () (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

• uses BoxIntegral.Integrable.convergenceR instead of a predicate assumption on r;
• uses BoxIntegral.IntegrationParams.MemBaseSet instead of “subordinate to r” to account for additional requirements like being a Henstock partition or having a bounded distortion;
• takes an extra argument π₀ : prepartition I and an assumption π.Union = π₀.Union instead of using π.to_prepartition.
theorem BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } {c : NNReal} {ε : } [] (h : BoxIntegral.Integrable I l f vol) (h0 : 0 < ε) (hπ : l.MemBaseSet I c (h.convergenceR ε c) π) :
dist () (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

• uses BoxIntegral.Integrable.convergenceR instead of a predicate assumption on r;
• uses BoxIntegral.IntegrationParams.MemBaseSet instead of “subordinate to r” to account for additional requirements like being a Henstock partition or having a bounded distortion;
theorem BoxIntegral.Integrable.tendsto_integralSum_sum_integral {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) (π₀ : ) :
Filter.Tendsto () (l.toFilteriUnion I π₀) (nhds (Jπ₀.boxes, BoxIntegral.integral J l f vol))

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} [] [] {I : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) {π₁ : } {π₂ : } (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]
theorem BoxIntegral.Integrable.toBoxAdditive_apply {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I l f vol) (J : ) :
h.toBoxAdditive J = BoxIntegral.integral J l f vol
def BoxIntegral.Integrable.toBoxAdditive {ι : Type u} {E : Type v} {F : Type w} [] [] {I : } [] {f : (ι)E} {vol : } [] (h : BoxIntegral.Integrable I 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.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} [] [] [] {I : } {f : (ι)E} (hb : ∃ (C : ), xBoxIntegral.Box.Icc I, f x C) (μ : MeasureTheory.Measure (ι)) (hc : ∀ᵐ (x : ι) ∂μ.restrict (BoxIntegral.Box.Icc I), ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) :

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} [] [] [] {I : } {f : (ι)E} (hb : ∃ (C : ), xBoxIntegral.Box.Icc I, f x C) (μ : MeasureTheory.Measure (ι)) (hc : ∀ᵐ (x : ι) ∂μ, ) :

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} [] [] [] {I : } {f : (ι)E} (hc : ContinuousOn f (BoxIntegral.Box.Icc I)) (μ : MeasureTheory.Measure (ι)) :

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} [] [] {I : } [] {f : (ι)E} {vol : } (hl : l.bRiemann = false) (B : ) (hB0 : ∀ (J : ), 0 B J) (g : ) (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 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 (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} [] [] {I : } [] {f : (ι)E} {vol : } (B : ) (hB0 : ∀ (J : ), 0 B J) (g : ) (s : Set (ι)) (hs : s.Countable) (H₁ : ∀ (c : NNReal), xBoxIntegral.Box.Icc I s, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J 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 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} [] [] {I : } [] {f : (ι)E} {vol : } (B : ) (hB0 : ∀ (J : ), 0 B J) (g : ) (H : NNRealxBoxIntegral.Box.Icc I, ε > 0, δ > 0, JI, BoxIntegral.Box.Icc J 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.