mathlib3documentation

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 #

• `ℝⁿ`: local notation for `ι → ℝ`

Tags #

integral

Integral sum and its basic properties #

noncomputable def box_integral.integral_sum {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (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
theorem box_integral.integral_sum_bUnion_tagged {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : ) (πi : Π (J : , ) :
(π.bUnion_tagged πi) = π.boxes.sum (λ (J : , (πi J))
theorem box_integral.integral_sum_bUnion_partition {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : ) (πi : Π (J : , ) (hπi : (J : , J π (πi J).is_partition) :
(π.bUnion_prepartition πi) = π
theorem box_integral.integral_sum_inf_partition {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : ) {π' : box_integral.prepartition I} (h : π'.is_partition) :
(π.inf_prepartition π') = π
theorem box_integral.integral_sum_fiberwise {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} {α : Type u_1} (g : α) (f : ) E) (vol : )  :
.sum (λ (y : α), (π.filter (λ (x : , g x = y))) = π
theorem box_integral.integral_sum_sub_partitions {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : ) {π₁ π₂ : box_integral.tagged_prepartition I} (h₁ : π₁.is_partition) (h₂ : π₂.is_partition) :
π₁ - π₂ = (π₁.to_prepartition π₂.to_prepartition).boxes.sum (λ (J : , (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} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : ) {π₁ π₂ : box_integral.tagged_prepartition I} (h : π₂.Union) :
(π₁.disj_union π₂ h) = π₁ + π₂
@[simp]
theorem box_integral.integral_sum_add {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f g : ) E) (vol : )  :
vol π = π + π
@[simp]
theorem box_integral.integral_sum_neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (f : ) E) (vol : )  :
vol π = - π
@[simp]
theorem box_integral.integral_sum_smul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} (c : ) (f : ) E) (vol : )  :
vol π = c π

Basic integrability theory #

def box_integral.has_integral {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] [fintype ι] (I : box_integral.box ι) (f : ) E) (vol : ) (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} [ E] [ F] [fintype ι] (I : box_integral.box ι) (f : ) E) (vol : ) :
Prop

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

Equations
• vol = (y : F), vol y
noncomputable def box_integral.integral {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] [fintype ι] (I : box_integral.box ι) (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
• vol = dite f vol) (λ (h : vol), (λ (h : ¬ vol), 0)
theorem box_integral.has_integral.tendsto {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (h : 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} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} :
vol y (ε : ), ε > 0 ( (r : nnreal ) (set.Ioi 0)), ( (c : nnreal), l.r_cond (r c)) (c : nnreal) (π : , l.mem_base_set I c (r c) π π.is_partition has_dist.dist π) y ε)

The `ε`-`δ` definition of `box_integral.has_integral`.

theorem box_integral.has_integral_of_mul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (a : ) (h : (ε : ), 0 < ε ( (r : nnreal ) (set.Ioi 0)), ( (c : nnreal), l.r_cond (r c)) (c : nnreal) (π : , l.mem_base_set I c (r c) π π.is_partition has_dist.dist π) y a * ε)) :
vol y

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 {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : }  :
theorem box_integral.integrable_iff_cauchy_basis {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : }  :
vol (ε : ), ε > 0 ( (r : nnreal ) (set.Ioi 0)), ( (c : nnreal), l.r_cond (r c)) (c₁ c₂ : nnreal) (π₁ π₂ : , l.mem_base_set I c₁ (r c₁) π₁ π₁.is_partition l.mem_base_set I c₂ (r c₂) π₂ π₂.is_partition has_dist.dist π₁) π₂) ε)

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} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} {l₁ l₂ : box_integral.integration_params} (h : vol y) (hl : l₂ l₁) :
vol y
@[protected]
theorem box_integral.integrable.has_integral {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) :
vol f vol)
theorem box_integral.integrable.mono {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (hle : l' l) :
f vol
theorem box_integral.has_integral.unique {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y y' : F} (h : vol y) (h' : vol y') :
y = y'
theorem box_integral.has_integral.integrable {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (h : vol y) :
vol
theorem box_integral.has_integral.integral_eq {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (h : vol y) :
vol = y
theorem box_integral.has_integral.add {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } {y y' : F} (h : vol y) (h' : vol y') :
(f + g) vol (y + y')
theorem box_integral.integrable.add {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } (hf : vol) (hg : vol) :
(f + g) vol
theorem box_integral.integral_add {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } (hf : vol) (hg : vol) :
(f + g) vol = vol + vol
theorem box_integral.has_integral.neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (hf : vol y) :
(-f) vol (-y)
theorem box_integral.integrable.neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (hf : vol) :
(-f) vol
theorem box_integral.integrable.of_neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (hf : (-f) vol) :
vol
@[simp]
theorem box_integral.integrable_neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } :
(-f) vol vol
@[simp]
theorem box_integral.integral_neg {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } :
(-f) vol = - vol
theorem box_integral.has_integral.sub {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } {y y' : F} (h : vol y) (h' : vol y') :
(f - g) vol (y - y')
theorem box_integral.integrable.sub {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } (hf : vol) (hg : vol) :
(f - g) vol
theorem box_integral.integral_sub {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f g : ) E} {vol : } (hf : vol) (hg : vol) :
(f - g) vol = vol - vol
theorem box_integral.has_integral_const {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } (c : E) :
(λ (_x : ι ), c) vol ((vol I) c)
@[simp]
theorem box_integral.integral_const {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } (c : E) :
(λ (_x : ι ), c) vol = (vol I) c
theorem box_integral.integrable_const {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } (c : E) :
(λ (_x : ι ), c) vol
theorem box_integral.has_integral_zero {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } :
(λ (_x : ι ), 0) vol 0
theorem box_integral.integrable_zero {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } :
(λ (_x : ι ), 0) vol
theorem box_integral.integral_zero {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } :
(λ (_x : ι ), 0) vol = 0
theorem box_integral.has_integral_sum {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {vol : } {α : Type u_1} {s : finset α} {f : α ) E} {g : α F} (h : (i : α), i s (f i) vol (g i)) :
(λ (x : ι ), s.sum (λ (i : α), f i x)) vol (s.sum (λ (i : α), g i))
theorem box_integral.has_integral.smul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {y : F} (hf : vol y) (c : ) :
(c f) vol (c y)
theorem box_integral.integrable.smul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (hf : vol) (c : ) :
(c f) vol
theorem box_integral.integrable.of_smul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {c : } (hf : (c f) vol) (hc : c 0) :
vol
@[simp]
theorem box_integral.integral_smul {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (c : ) :
(λ (x : ι ), c f x) vol = c vol
theorem box_integral.integral_nonneg {ι : Type u} {I : box_integral.box ι} [fintype ι] {g : ) } (hg : (x : ι ), 0 g x) (μ : measure_theory.measure ))  :
0

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

theorem box_integral.norm_integral_le_of_norm_le {ι : Type u} {E : Type v} [ E] {I : box_integral.box ι} [fintype ι] {f : ) E} {g : ) } (hle : (x : ι ), f x g x) (μ : measure_theory.measure )) (hg : μ.to_box_additive.to_smul) :

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 box_integral.norm_integral_le_of_le_const {ι : Type u} {E : Type v} [ E] {I : box_integral.box ι} [fintype ι] {f : ) E} {c : } (hc : (x : ι ), f x c) (μ : measure_theory.measure ))  :
(μ I).to_real * 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 `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

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

noncomputable def box_integral.integrable.convergence_r {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (ε : ) :

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
• = dite (0 < ε) (λ (hε : 0 < ε), _.some) (λ (hε : ¬0 < ε) (_x : nnreal) (_x : ι ), 1, box_integral.integrable.convergence_r._proof_4⟩)
theorem box_integral.integrable.convergence_r_cond {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (ε : ) (c : nnreal) :
theorem box_integral.integrable.dist_integral_sum_integral_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {c : nnreal} {ε : } (h : vol) (h₀ : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) π) (hπp : π.is_partition) :
has_dist.dist π) f vol) ε
theorem box_integral.integrable.dist_integral_sum_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {c₁ c₂ : nnreal} {ε₁ ε₂ : } {π₁ π₂ : box_integral.tagged_prepartition I} (h : 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) :
has_dist.dist π₁) π₂) ε₁ + ε₂

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

• uses `box_integral.integrable.convergence_r` instead of a predicate assumption on `r`;
• uses `box_integral.integration_params.mem_base_set` instead of “subordinate to `r`” to account for additional requirements like being a Henstock partition or having a bounded distortion.

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

theorem box_integral.integrable.tendsto_integral_sum_to_filter_prod_self_inf_Union_eq_uniformity {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) :
filter.tendsto (λ (π : , π.fst, π.snd)) ((l.to_filter I).prod (l.to_filter I) (uniformity F)

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.

theorem box_integral.integrable.cauchy_map_integral_sum_to_filter_Union {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (π₀ : box_integral.prepartition I) :
cauchy (filter.map vol) (l.to_filter_Union 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 box_integral.integrable.to_subbox_aux {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I J : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (hJ : J I) :
(y : F), vol y (l.to_filter_Union I hJ)) (nhds y)
theorem box_integral.integrable.to_subbox {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I J : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (hJ : J I) :
vol

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

theorem box_integral.integrable.tendsto_integral_sum_to_filter_Union_single {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I J : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (hJ : J I) :
(l.to_filter_Union I hJ)) (nhds 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 box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {c : nnreal} {ε : } (h : vol) (h0 : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) π) {π₀ : box_integral.prepartition I} (hU : π.Union = π₀.Union) :
has_dist.dist π) (π₀.boxes.sum (λ (J : , 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 `box_integral.integrable.convergence_r` instead of a predicate assumption on `r`;
• uses `box_integral.integration_params.mem_base_set` 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 box_integral.integrable.dist_integral_sum_sum_integral_le_of_mem_base_set {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } {c : nnreal} {ε : } (h : vol) (h0 : 0 < ε) (hπ : l.mem_base_set I c (h.convergence_r ε c) π) :
has_dist.dist π) (π.to_prepartition.boxes.sum (λ (J : , 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 `box_integral.integrable.convergence_r` instead of a predicate assumption on `r`;
• uses `box_integral.integration_params.mem_base_set` instead of “subordinate to `r`” to account for additional requirements like being a Henstock partition or having a bounded distortion;
theorem box_integral.integrable.tendsto_integral_sum_sum_integral {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (π₀ : box_integral.prepartition I) :
(l.to_filter_Union I π₀) (nhds (π₀.boxes.sum (λ (J : , 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 box_integral.integrable.sum_integral_congr {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) {π₁ π₂ : box_integral.prepartition I} (hU : π₁.Union = π₂.Union) :
π₁.boxes.sum (λ (J : , vol) = π₂.boxes.sum (λ (J : , 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} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : vol) (J : box_integral.box ι) :
noncomputable def box_integral.integrable.to_box_additive {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (h : 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 #

theorem box_integral.integrable_of_continuous_on {ι : Type u} {E : Type v} [ E] [fintype ι] {I : box_integral.box ι} {f : ) E} (hc : ) (μ : measure_theory.measure ))  :

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} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (hl : l.bRiemann = bool.ff) (B : I) (hB0 : (J : , 0 B J) (g : I) (s : set )) (hs : s.countable) (hlH : s.nonempty ) (H₁ : (c : nnreal) (x : ι ), x (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (J : , J I ((l.bDistortion) J.distortion c) has_dist.dist ((vol J) (f x)) (g J) ε)) (H₂ : (c : nnreal) (x : ι ), x (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (J : , J I ((l.bHenstock) ((l.bDistortion) J.distortion c) has_dist.dist ((vol J) (f x)) (g J) ε * B J)) :
vol (g I)

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} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (B : I) (hB0 : (J : , 0 B J) (g : I) (s : set )) (hs : s.countable) (H₁ : (c : nnreal) (x : ι ), x (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (J : , J I ((l.bDistortion) J.distortion c) has_dist.dist ((vol J) (f x)) (g J) ε)) (H₂ : (c : nnreal) (x : ι ), x (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (J : , J I ((l.bDistortion) J.distortion c) has_dist.dist ((vol J) (f x)) (g J) ε * B J)) :
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 `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 along`l`with integral`g I`.

theorem box_integral.has_integral_McShane_of_forall_is_o {ι : Type u} {E : Type v} {F : Type w} [ E] [ F] {I : box_integral.box ι} [fintype ι] {f : ) E} {vol : } (B : I) (hB0 : (J : , 0 B J) (g : I) (H : nnreal (x : ι ), (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (J : , J I has_dist.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`.