BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le
theorem BoxIntegral.norm_volume_sub_integral_face_upper_sub_lower_smul_le :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [inst_2 : CompleteSpace E]
(I : BoxIntegral.Box (Fin (n + 1))) {i : Fin (n + 1)} {f : (Fin (n + 1) → ℝ) → E}
{f' : (Fin (n + 1) → ℝ) →L[ℝ] E},
ContinuousOn f (BoxIntegral.Box.Icc I) →
∀ {x : Fin (n + 1) → ℝ},
x ∈ BoxIntegral.Box.Icc I →
∀ {a : E} {ε : ℝ},
0 < ε →
(∀ y ∈ BoxIntegral.Box.Icc I, ‖f y - a - f' (y - x)‖ ≤ ε * ‖y - x‖) →
∀ {c : NNReal},
I.distortion ≤ c →
‖(Finset.univ.prod fun j => I.upper j - I.lower j) • f' (Pi.single i 1) -
(BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.upper i))
BoxIntegral.BoxAdditiveMap.volume -
BoxIntegral.integral (I.face i) ⊥ (f ∘ i.insertNth (I.lower i))
BoxIntegral.BoxAdditiveMap.volume)‖ ≤
2 * ε * ↑c * Finset.univ.prod fun j => I.upper j - I.lower j
This theorem is an auxiliary lemma for the divergence theorem. It states that for a given normed additive commutative group `E` over the reals, which also forms a normed space, a natural number `n` and assuming `E` is a complete space, a box `I` in `n+1` dimensions, a function `f` from `n+1` dimensions into `E`, a continuous linear map `f'` from `n+1` dimensions into `E`, if `f` is continuous on the closed box `I`, for all `x` in the box `I` and any `a` in `E` and a real number `ε` greater than zero such that the norm of the difference between `f(y)` and `f'(y - x)` subtracted from `a` is less than or equal to `ε` times the norm of `y - x` for all `y` in the box `I`, then for all nonnegative real number `c` such that the distortion of `I` is less than or equal to `c`, the norm of the difference between the product of the upper and lower bounds of `I` and `f'` evaluated at the coordinate unit vector `i` and the volume integral of `f` over the face `i` of `I` at the upper and lower bounds, is less than or equal to twice the product of `ε`, `c` and the product of the upper and lower bounds of `I`.
More concisely: Under the given assumptions, the norm of the difference between the integral of a continuous function `f` over a box's face and the linear map `f'` evaluated at the coordinate unit vector, is less than or equal to twice the product of `ε`, `c`, and the box's volume.
|
BoxIntegral.hasIntegral_GP_pderiv
theorem BoxIntegral.hasIntegral_GP_pderiv :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [inst_2 : CompleteSpace E]
(I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → E)
(f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ)),
s.Countable →
(∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
(∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
∀ (i : Fin (n + 1)),
BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => (f' x) (Pi.single i 1))
BoxIntegral.BoxAdditiveMap.volume
(BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
(fun x => f (i.insertNth (I.upper i) x)) BoxIntegral.BoxAdditiveMap.volume -
BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
(fun x => f (i.insertNth (I.lower i) x)) BoxIntegral.BoxAdditiveMap.volume)
The theorem `BoxIntegral.hasIntegral_GP_pderiv` states that for a function `f : ℝⁿ⁺¹ → E` that is differentiable on a closed rectangular box `I` with derivative `f'`, the partial derivative `f' x (Pi.single i 1)` is Henstock-Kurzweil integrable. Furthermore, the integral of this partial derivative equals the difference in integrals of `f` over the faces of the box defined by `x i = I.upper i` and `x i = I.lower i`.
This theorem is a non-standard generalization of the Henstock-Kurzweil integral which allows `f` to be non-differentiable (though still continuous) at a countable set of points. Note that if the dimension `n` is greater than 0, the condition at `x ∈ s` can potentially be replaced with a weaker estimate, but this would require improved integrability theorems or the use of a filter that depends on the countable set `s`. The goal is to ensure that none of the faces of a partition contain a point from `s`.
More concisely: For a differentiable real-valued function `f` on a closed rectangular box `I` ⊆ ℝⁿ with derivative `f'`, the partial derivative `f' x (Pi.single i 1)` is Henstock-Kurzweil integrable and equal to the difference in integrals of `f` over the i-th faces of `I`.
|
BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt
theorem BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt :
∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [inst_2 : CompleteSpace E]
(I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E)
(f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E) (s : Set (Fin (n + 1) → ℝ)),
s.Countable →
(∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
(∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP
(fun x => Finset.univ.sum fun i => (f' x) (Pi.single i 1) i) BoxIntegral.BoxAdditiveMap.volume
(Finset.univ.sum fun i =>
BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
(fun x => f (i.insertNth (I.upper i) x) i) BoxIntegral.BoxAdditiveMap.volume -
BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
(fun x => f (i.insertNth (I.lower i) x) i) BoxIntegral.BoxAdditiveMap.volume)
This theorem is a version of the Divergence theorem for a Henstock-Kurzweil style integral.
In the context of multivariate calculus, it states that if we have a function `f` mapping from ℝⁿ⁺¹ to Eⁿ⁺¹, which is differentiable on a closed rectangular box `I` with derivative `f'`, then the divergence of `f` (represented as `∑ i, f' x (Pi.single i 1) i`) is Henstock-Kurzweil integrable. Further, the integral of this divergence is equal to the sum of integrals of `f` over the faces of `I` (with appropriate signs considered).
The theorem allows for the derivative `f'` to be non-differentiable (although still continuous) at a countable set of points in `s`, and uses a generalized version of the Henstock-Kurzweil integral. The divergence is calculated as the sum of the derivative `f'` applied to the unit vectors in each dimension, and the integral is then found using the volume of the box `I`.
The integral over all the faces of `I` is calculated by considering each face in turn, and integrating `f` over that face. The result for each face is then subtracted from the integral of the divergence to give the final result.
More concisely: If a differentiable function `f` : ℝⁿ → Eⁿ with continuous derivative `f'` on a closed rectangular box `I` in ℝⁿ has Henstock-Kurzweil integrable divergence `∑ i, f' (Pi.single i 1) i`, then the integral of this divergence equals the sum of integrals of `f` over the faces of `I` with appropriate signs.
|