English
The real distance between I.lower and I.upper is bounded by distortion(I) times the i-th edge length.
Русский
Реальное расстояние между I.lower и I.upper ограничено искажением I на величину ребра вдоль i.
LaTeX
$$$$ dist(I.lower,I.upper) \le I.distortion \cdot (I.upper(i) - I.lower(i)). $$$$
Lean4
/-- 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. -/
theorem hasIntegral_GP_divergence_of_forall_hasDerivWithinAt (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) → ℝ)) (hs : s.Countable)
(Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x)
(Hd : ∀ x ∈ (Box.Icc I) \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x) :
HasIntegral.{0, u, u} I GP (fun x => ∑ i, f' x (Pi.single i 1) i) BoxAdditiveMap.volume
(∑ i,
(integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.upper i) x) i) BoxAdditiveMap.volume -
integral.{0, u, u} (I.face i) GP (fun x => f (i.insertNth (I.lower i) x) i) BoxAdditiveMap.volume)) :=
by
refine HasIntegral.sum fun i _ => ?_
simp only [hasFDerivWithinAt_pi', continuousWithinAt_pi] at Hd Hs
exact hasIntegral_GP_pderiv I _ _ s hs (fun x hx => Hs x hx i) (fun x hx => Hd x hx i) i
