Zulip Chat Archive

Stream: maths

Topic: Stokes theorem


view this post on Zulip Yury G. Kudryashov (Jan 05 2021 at 13:09):

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)

view this post on Zulip 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!

view this post on Zulip Yury G. Kudryashov (Jan 05 2021 at 21:08):

BTW, thanks for defining pi-measures!

view this post on Zulip 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