## Stream: maths

### Topic: Stokes theorem

#### Yury G. Kudryashov (Jan 05 2021 at 13:09):

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 (Jan 05 2021 at 17:19):

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 (Jan 05 2021 at 21:08):

BTW, thanks for defining pi-measures!

#### Yury G. Kudryashov (Jan 06 2021 at 00:09):

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

Last updated: May 10 2021 at 08:14 UTC