mathlib documentation

analysis.box_integral.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 box_integral.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 : box_integral.integration_params. 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 has_sum and tsum), we define a predicate box_integral.has_integral and a function box_integral.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 box_integral.integrable.dist_integral_sum_le_of_mem_base_set and box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_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 #

noncomputable def box_integral.integral_sum {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) :
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
theorem box_integral.integral_sum_bUnion_tagged {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.prepartition I) (πi : Π (J : box_integral.box ι), box_integral.tagged_prepartition J) :
box_integral.integral_sum f vol («π».bUnion_tagged πi) = ∑ (J : box_integral.box ι) in «π».boxes, box_integral.integral_sum f vol (πi J)
theorem box_integral.integral_sum_bUnion_partition {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) (πi : Π (J : box_integral.box ι), box_integral.prepartition J) (hπi : ∀ (J : box_integral.box ι), J «π»(πi J).is_partition) :
theorem box_integral.integral_sum_inf_partition {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) {π' : box_integral.prepartition I} (h : π'.is_partition) :
theorem box_integral.integral_sum_fiberwise {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} {α : Type u_1} (g : box_integral.box ι → α) (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) :
∑ (y : α) in finset.image g «π».to_prepartition.boxes, box_integral.integral_sum f vol («π».filter (λ (x : box_integral.box ι), g x = y)) = box_integral.integral_sum f vol «π»
theorem box_integral.integral_sum_sub_partitions {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) {π₁ π₂ : box_integral.tagged_prepartition I} (h₁ : π₁.is_partition) (h₂ : π₂.is_partition) :
box_integral.integral_sum f vol π₁ - box_integral.integral_sum f vol π₂ = ∑ (J : box_integral.box ι) in (π₁.to_prepartition π₂.to_prepartition).boxes, ((vol J) (f ((π₁.inf_prepartition π₂.to_prepartition).tag J)) - (vol J) (f ((π₂.inf_prepartition π₁.to_prepartition).tag J)))
@[simp]
theorem box_integral.integral_sum_disj_union {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) {π₁ π₂ : box_integral.tagged_prepartition I} (h : disjoint π₁.Union π₂.Union) :
@[simp]
theorem box_integral.integral_sum_add {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f g : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) :
@[simp]
theorem box_integral.integral_sum_neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) :
@[simp]
theorem box_integral.integral_sum_smul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} (c : ) (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (π : box_integral.tagged_prepartition I) :

Basic integrability theory #

def box_integral.has_integral {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] [fintype ι] (I : box_integral.box ι) (l : box_integral.integration_params) (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) (y : F) :
Prop

The predicate has_integral 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 box_integral.integration_params.to_filter_Union I ⊤.

Equations
def box_integral.integrable {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] [fintype ι] (I : box_integral.box ι) (l : box_integral.integration_params) (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) :
Prop

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

Equations
noncomputable def box_integral.integral {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] [fintype ι] (I : box_integral.box ι) (l : box_integral.integration_params) (f : (ι → ) → E) (vol : ι →ᵇᵃ E →L[] F) :
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
theorem box_integral.has_integral.tendsto {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (h : box_integral.has_integral I l f vol y) :

Reinterpret box_integral.has_integral as filter.tendsto, e.g., dot-notation theorems that are shadowed in the box_integral.has_integral namespace.

theorem box_integral.has_integral_iff {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} :
box_integral.has_integral I l f vol y ∀ (ε : ), ε > 0(∃ (r : ℝ≥0(ι → )(set.Ioi 0)), (∀ (c : ℝ≥0), l.r_cond (r c)) ∀ (c : ℝ≥0) («π» : box_integral.tagged_prepartition I), l.mem_base_set I c (r c) «π»«π».is_partitiondist (box_integral.integral_sum f vol «π») y ε)

The ε-δ definition of box_integral.has_integral.

theorem box_integral.has_integral_of_mul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (a : ) (h : ∀ (ε : ), 0 < ε(∃ (r : ℝ≥0(ι → )(set.Ioi 0)), (∀ (c : ℝ≥0), l.r_cond (r c)) ∀ (c : ℝ≥0) («π» : box_integral.tagged_prepartition I), l.mem_base_set I c (r c) «π»«π».is_partitiondist (box_integral.integral_sum f vol «π») y a * ε)) :

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

theorem box_integral.integrable_iff_cauchy_basis {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] :
box_integral.integrable I l f vol ∀ (ε : ), ε > 0(∃ (r : ℝ≥0(ι → )(set.Ioi 0)), (∀ (c : ℝ≥0), l.r_cond (r c)) ∀ (c₁ c₂ : ℝ≥0) (π₁ π₂ : box_integral.tagged_prepartition I), l.mem_base_set I c₁ (r c₁) π₁π₁.is_partitionl.mem_base_set I c₂ (r c₂) π₂π₂.is_partitiondist (box_integral.integral_sum f vol π₁) (box_integral.integral_sum 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 box_integral.has_integral.mono {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} {l₁ l₂ : box_integral.integration_params} (h : box_integral.has_integral I l₁ f vol y) (hl : l₂ l₁) :
@[protected]
theorem box_integral.integrable.has_integral {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (h : box_integral.integrable I l f vol) :
theorem box_integral.integrable.mono {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {l' : box_integral.integration_params} (h : box_integral.integrable I l f vol) (hle : l' l) :
theorem box_integral.has_integral.unique {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y y' : F} (h : box_integral.has_integral I l f vol y) (h' : box_integral.has_integral I l f vol y') :
y = y'
theorem box_integral.has_integral.integrable {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (h : box_integral.has_integral I l f vol y) :
theorem box_integral.has_integral.integral_eq {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (h : box_integral.has_integral I l f vol y) :
theorem box_integral.has_integral.add {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y y' : F} (h : box_integral.has_integral I l f vol y) (h' : box_integral.has_integral I l g vol y') :
box_integral.has_integral I l (f + g) vol (y + y')
theorem box_integral.integrable.add {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) (hg : box_integral.integrable I l g vol) :
theorem box_integral.integral_add {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) (hg : box_integral.integrable I l g vol) :
theorem box_integral.has_integral.neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (hf : box_integral.has_integral I l f vol y) :
theorem box_integral.integrable.neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) :
theorem box_integral.integrable.of_neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l (-f) vol) :
@[simp]
theorem box_integral.integrable_neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} :
@[simp]
theorem box_integral.integral_neg {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} :
theorem box_integral.has_integral.sub {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y y' : F} (h : box_integral.has_integral I l f vol y) (h' : box_integral.has_integral I l g vol y') :
box_integral.has_integral I l (f - g) vol (y - y')
theorem box_integral.integrable.sub {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) (hg : box_integral.integrable I l g vol) :
theorem box_integral.integral_sub {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) (hg : box_integral.integrable I l g vol) :
theorem box_integral.has_integral_const {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} (c : E) :
box_integral.has_integral I l (λ (_x : ι → ), c) vol ((vol I) c)
@[simp]
theorem box_integral.integral_const {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} (c : E) :
box_integral.integral I l (λ (_x : ι → ), c) vol = (vol I) c
theorem box_integral.integrable_const {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} (c : E) :
box_integral.integrable I l (λ (_x : ι → ), c) vol
theorem box_integral.has_integral_zero {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} :
box_integral.has_integral I l (λ (_x : ι → ), 0) vol 0
theorem box_integral.integrable_zero {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} :
box_integral.integrable I l (λ (_x : ι → ), 0) vol
theorem box_integral.integral_zero {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} :
box_integral.integral I l (λ (_x : ι → ), 0) vol = 0
theorem box_integral.has_integral_sum {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : ι →ᵇᵃ E →L[] F} {α : Type u_1} {s : finset α} {f : α → (ι → ) → E} {g : α → F} (h : ∀ (i : α), i sbox_integral.has_integral I l (f i) vol (g i)) :
box_integral.has_integral I l (λ (x : ι → ), ∑ (i : α) in s, f i x) vol (∑ (i : α) in s, g i)
theorem box_integral.has_integral.smul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {y : F} (hf : box_integral.has_integral I l f vol y) (c : ) :
box_integral.has_integral I l (c f) vol (c y)
theorem box_integral.integrable.smul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hf : box_integral.integrable I l f vol) (c : ) :
theorem box_integral.integrable.of_smul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {c : } (hf : box_integral.integrable I l (c f) vol) (hc : c 0) :
@[simp]
theorem box_integral.integral_smul {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (c : ) :
box_integral.integral I l (λ (x : ι → ), c f x) vol = c box_integral.integral I l f vol

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

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.

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 box_integral.integration_params. We formalize several versions of this inequality in box_integral.integrable.dist_integral_sum_le_of_mem_base_set, box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq, and box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set.

Instead of using predicate assumptions on r, we define box_integral.integrable.convergence_r (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.

noncomputable def box_integral.integrable.convergence_r {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (h : box_integral.integrable I l f vol) (ε : ) :
ℝ≥0(ι → )(set.Ioi 0)

If ε > 0, then box_integral.integrable.convergence_r 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 box_integral.integration_params.bDistortion l = tt), the corresponding integral sum is ε-close to the integral.

If box.integral.integration_params.bRiemann = tt, then r c x does not depend on x. If ε ≤ 0, then we use r c x = 1.

Equations
theorem box_integral.integrable.convergence_r_cond {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (h : box_integral.integrable I l f vol) (ε : ) (c : ℝ≥0) :
theorem box_integral.integrable.dist_integral_sum_integral_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {c : ℝ≥0} {ε : } (h : box_integral.integrable I l f vol) (h₀ : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) «π») (hπp : «π».is_partition) :
theorem box_integral.integrable.dist_integral_sum_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {c₁ c₂ : ℝ≥0} {ε₁ ε₂ : } {π₁ π₂ : box_integral.tagged_prepartition I} (h : box_integral.integrable I l f vol) (hpos₁ : 0 < ε₁) (hpos₂ : 0 < ε₂) (h₁ : l.mem_base_set I c₁ (h.convergence_r ε₁ c₁) π₁) (h₂ : l.mem_base_set I c₂ (h.convergence_r ε₂ c₂) π₂) (HU : π₁.Union = π₂.Union) :
dist (box_integral.integral_sum f vol π₁) (box_integral.integral_sum f vol π₂) ε₁ + ε₂

Henstock-Sacks inequality. Let r₁ r₂ : ℝⁿ → (0, ∞) be 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 box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq and box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set.

If f is integrable on I along l, then for two sufficiently fine tagged prepartitions (in the sense of the filter box_integral.integration_params.to_filter 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.

theorem box_integral.integrable.to_subbox_aux {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I J : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.integrable I l f vol) (hJ : J I) :
theorem box_integral.integrable.to_subbox {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I J : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.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.

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 box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {c : ℝ≥0} {ε : } [complete_space F] (h : box_integral.integrable I l f vol) (h0 : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) «π») {π₀ : box_integral.prepartition I} (hU : «π».Union = π₀.Union) :
dist (box_integral.integral_sum f vol «π») (∑ (J : box_integral.box ι) in π₀.boxes, box_integral.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 box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} {π : box_integral.tagged_prepartition I} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} {c : ℝ≥0} {ε : } [complete_space F] (h : box_integral.integrable I l f vol) (h0 : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) «π») :
dist (box_integral.integral_sum f vol «π») (∑ (J : box_integral.box ι) in «π».to_prepartition.boxes, box_integral.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 box_integral.integrable.tendsto_integral_sum_sum_integral {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.integrable I l f vol) (π₀ : box_integral.prepartition I) :

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 box_integral.integrable.sum_integral_congr {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.integrable I l f vol) {π₁ π₂ : box_integral.prepartition I} (hU : π₁.Union = π₂.Union) :
∑ (J : box_integral.box ι) in π₁.boxes, box_integral.integral J l f vol = ∑ (J : box_integral.box ι) in π₂.boxes, box_integral.integral J l f vol

If f is integrable on I, then λ 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, then 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 box_integral.integrable.to_box_additive for a bundled version.

@[simp]
theorem box_integral.integrable.to_box_additive_apply {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.integrable I l f vol) (J : box_integral.box ι) :
noncomputable def box_integral.integrable.to_box_additive {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} [complete_space F] (h : box_integral.integrable I l f vol) :

If f is integrable on I, then λ 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, then 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 box_integral.integrable.sum_integral_congr for an unbundled version.

Equations

Integrability conditions #

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

This is true for any volume with bounded variation.

theorem box_integral.has_integral_of_bRiemann_eq_ff_of_forall_is_o {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hl : l.bRiemann = ff) (B : ι →ᵇᵃ[I] ) (hB0 : ∀ (J : box_integral.box ι), 0 B J) (g : ι →ᵇᵃ[I] F) (s : set (ι → )) (hs : s.countable) (hlH : s.nonemptyl.bHenstock = tt) (H₁ : ∀ (c : ℝ≥0) (x : ι → ), x box_integral.box.Icc I s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (J : box_integral.box ι), J Ibox_integral.box.Icc J metric.closed_ball x δx box_integral.box.Icc J((l.bDistortion) → J.distortion c)dist ((vol J) (f x)) (g J) ε)) (H₂ : ∀ (c : ℝ≥0) (x : ι → ), x box_integral.box.Icc I \ s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (J : box_integral.box ι), J Ibox_integral.box.Icc J metric.closed_ball x δ((l.bHenstock) → x box_integral.box.Icc J)((l.bDistortion) → J.distortion c)dist ((vol J) (f x)) (g J) ε * B J)) :

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

theorem box_integral.has_integral_of_le_Henstock_of_forall_is_o {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (hl : l box_integral.integration_params.Henstock) (B : ι →ᵇᵃ[I] ) (hB0 : ∀ (J : box_integral.box ι), 0 B J) (g : ι →ᵇᵃ[I] F) (s : set (ι → )) (hs : s.countable) (H₁ : ∀ (c : ℝ≥0) (x : ι → ), x box_integral.box.Icc I s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (J : box_integral.box ι), J Ibox_integral.box.Icc J metric.closed_ball x δx box_integral.box.Icc J((l.bDistortion) → J.distortion c)dist ((vol J) (f x)) (g J) ε)) (H₂ : ∀ (c : ℝ≥0) (x : ι → ), x box_integral.box.Icc I \ s∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (J : box_integral.box ι), J Ibox_integral.box.Icc J metric.closed_ball x δx box_integral.box.Icc J((l.bDistortion) → J.distortion c)dist ((vol J) (f x)) (g J) ε * B J)) :

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 box_integral.integration_params.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.closed_ball 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 alonglwith integralg I`.

theorem box_integral.has_integral_McShane_of_forall_is_o {ι : Type u} {E : Type v} {F : Type w} [normed_group E] [normed_space E] [normed_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {f : (ι → ) → E} {vol : ι →ᵇᵃ E →L[] F} (B : ι →ᵇᵃ[I] ) (hB0 : ∀ (J : box_integral.box ι), 0 B J) (g : ι →ᵇᵃ[I] F) (H : ℝ≥0∀ (x : ι → ), x box_integral.box.Icc I∀ (ε : ), ε > 0(∃ (δ : ) (H : δ > 0), ∀ (J : box_integral.box ι), J Ibox_integral.box.Icc J metric.closed_ball 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.closed_ball 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.