Stokes theorem

Stream: maths

[Yury G. Kudryashov]

From branch#measure-subadditive, this file:

def box_boundary_integral (f : (fin (n + 1) → ℝ) → fin (n + 1) → E) (x y : fin (n + 1) → ℝ) : E :=
∑ i : fin (n + 1),
  ((∫ z in Icc (x ∘ i.succ_above) (y ∘ i.succ_above), f (fin.insert_nth i (y i) z) i) -
    ∫ z in Icc (x ∘ i.succ_above) (y ∘ i.succ_above), f (fin.insert_nth i (x i) z) i)

theorem box_boundary_integral_eq_fderiv (h : x ≤ y)
  (hd : ∀ z ∈ Icc x y, differentiable_at ℝ f z)
  (hf'c : continuous_on (λ z, ∑ i, fderiv ℝ f z (update 0 i 1) i) (Icc x y)) :
  box_boundary_integral f x y = ∫ z in Icc x y, ∑ i, fderiv ℝ f z (update 0 i 1) i :=

@Patrick Massot @Sebastien Gouezel @Heather Macbeth @Floris van Doorn @Alex Kontorovich

The code is not PR-ready yet (but is sorry-free)

[Floris van Doorn]

It takes some work to parse these statements, but if I understand correctly, this is Stokes' theorem for boxes in R^n.

∫ z in Icc x y is a very nice way to write an integral over a box!

[Yury G. Kudryashov]

BTW, thanks for defining pi-measures!

[Yury G. Kudryashov]

#5625, #5626, #5627, #5571, and #4913 are dependencies of a future PR with the Stokes theorem.