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

The ε-δ definition of box_integral.has_integral.

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.

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

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

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

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

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;

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.

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.