mathlib3 documentation

analysis.box_integral.basic

Integrals of Riemann, Henstock-Kurzweil, and McShane #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

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

Basic integrability theory #

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

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

Equations

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

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_of_mul {ι : Type u} {E : Type v} {F : Type w} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : ) E} {vol : box_integral.box_additive_map ι (E →L[] F) } {y : F} (a : ) (h : (ε : ), 0 < ε ( (r : nnreal ) (set.Ioi 0)), ( (c : nnreal), l.r_cond (r c)) (c : nnreal) (π : box_integral.tagged_prepartition I), l.mem_base_set I c (r c) π π.is_partition has_dist.dist (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_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : ) E} {vol : box_integral.box_additive_map ι (E →L[] F) } [complete_space F] :
box_integral.integrable I l f vol (ε : ), ε > 0 ( (r : nnreal ) (set.Ioi 0)), ( (c : nnreal), l.r_cond (r c)) (c₁ c₂ : nnreal) (π₁ π₂ : box_integral.tagged_prepartition I), l.mem_base_set I c₁ (r c₁) π₁ π₁.is_partition l.mem_base_set I c₂ (r c₂) π₂ π₂.is_partition has_dist.dist (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_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : box_integral.box_additive_map ι (E →L[] F) } {y : F} {l₁ l₂ : box_integral.integration_params} (h : box_integral.has_integral I l₁ f vol y) (hl : l₂ l₁) :
theorem box_integral.has_integral.add {ι : Type u} {E : Type v} {F : Type w} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : ) E} {vol : box_integral.box_additive_map ι (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.has_integral.sub {ι : Type u} {E : Type v} {F : Type w} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f g : ) E} {vol : box_integral.box_additive_map ι (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.has_integral_sum {ι : Type u} {E : Type v} {F : Type w} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {vol : box_integral.box_additive_map ι (E →L[] F) } {α : Type u_1} {s : finset α} {f : α ) E} {g : α F} (h : (i : α), i s box_integral.has_integral I l (f i) vol (g i)) :
box_integral.has_integral I l (λ (x : ι ), s.sum (λ (i : α), f i x)) vol (s.sum (λ (i : α), g i))
@[simp]

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.

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.dist_integral_sum_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [normed_add_comm_group E] [normed_space E] [normed_add_comm_group F] [normed_space F] {I : box_integral.box ι} [fintype ι] {l : box_integral.integration_params} {f : ) E} {vol : box_integral.box_additive_map ι (E →L[] F) } {c₁ c₂ : nnreal} {ε₁ ε₂ : } {π₁ π₂ : 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) :

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.

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.

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

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 π₀.

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.

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.

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

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`.

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.