Divergence integral for Henstock-Kurzweil integral #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove the Divergence Theorem for a Henstock-Kurzweil style integral. The theorem
says the following. Let f : ℝⁿ → Eⁿ be a function differentiable on a closed rectangular box
I with derivative f' x : ℝⁿ →L[ℝ] Eⁿ at x ∈ I. Then the divergence λ x, ∑ k, f' x eₖ k,
where eₖ = pi.single k 1 is the k-th basis vector, is integrable on I, and its integral is
equal to the sum of integrals of f over the faces of I taken with appropriate signs.
To make the proof work, we had to ban tagged partitions with “long and thin” boxes. More precisely,
we use the following generalization of one-dimensional Henstock-Kurzweil integral to functions
defined on a box in ℝⁿ (it corresponds to the value box_integral.integration_params.GP = ⊥ of
box_integral.integration_params in the definition of box_integral.has_integral).
We say that f : ℝⁿ → E has integral y : E over a box I ⊆ ℝⁿ if for an arbitrarily small
positive ε and an arbitrarily large c, there exists a function r : ℝⁿ → (0, ∞) such that for
any tagged partition π of I such that
πis a Henstock partition, i.e., each tag belongs to its box;πis subordinate tor;- for every box of
π, the maximum of the ratios of its sides is less than or equal toc,
the integral sum of f over π is ε-close to y. In case of dimension one, the last condition
trivially holds for any c ≥ 1, so this definition is equivalent to the standard definition of
Henstock-Kurzweil integral.
Tags #
Henstock-Kurzweil integral, integral, Stokes theorem, divergence theorem
Auxiliary lemma for the divergence theorem.
If f : ℝⁿ⁺¹ → E is differentiable on a closed rectangular box I with derivative f', then
the partial derivative λ x, f' x (pi.single i 1) is Henstock-Kurzweil integrable with integral
equal to the difference of integrals of f over the faces x i = I.upper i and x i = I.lower i.
More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
we allow f to be non-differentiable (but still continuous) at a countable set of points.
TODO: If n > 0, then the condition at x ∈ s can be replaced by a much weaker estimate but this
requires either better integrability theorems, or usage of a filter depending on the countable set
s (we need to ensure that none of the faces of a partition contain a point from s).
Divergence theorem for a Henstock-Kurzweil style integral.
If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is differentiable on a closed rectangular box I with derivative f', then
the divergence ∑ i, f' x (pi.single i 1) i is Henstock-Kurzweil integrable with integral equal to
the sum of integrals of f over the faces of I taken with appropriate signs.
More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
we allow f to be non-differentiable (but still continuous) at a countable set of points.