Stokes' formula for one-forms on rectangles and annuli

The integral of the exterior derivative of a vector-valued real one-form over a rectangle or closed annulus is its positively oriented boundary integral. Zero inner radius gives the disc formula. Only C¹ regularity near the region of integration is required; in the annular case no regularity on the missing inner disc is needed. On a rectangle the formula is stated both for the set integral over Icc a b (TauCeti.integral_extDeriv_prod_Icc) and for the iterated integral over oriented intervals (TauCeti.integral2_extDeriv). For a scalar one-form f_s ds + f_t dt it is Green's theorem TauCeti.integral_fderiv_sub_fderiv_Icc, written in terms of the partial derivatives ∂_s f_t - ∂_t f_s.

One dimension up, the integral of a closed two-form over the boundary of a cube vanishes: its integrals over the top and bottom faces differ by the signed integrals over the four side faces (TauCeti.integral2_slice_sub_eq_sides). This follows from the rectangle formula applied to the cylinder homotopy operator TauCeti.cylinderHomotopy, a primitive of the difference of the top and bottom slices of a closed form. Pulled back along a homotopy of maps into a manifold, it gives the homotopy invariance of integrals of closed two-forms over cylinders.

Unlike the bilinear-pairing version of Green's formula, these results apply to arbitrary one-forms, including pullbacks of Liouville forms from exact symplectic manifolds. They provide the area calculation used to exclude holomorphic discs with exact Lagrangian boundary.

The proofs use Mathlib's rectangular divergence theorem, naturality of the exterior derivative, and the polar change of variables. Applying the rectangle formula to the polar pullback gives the annulus formula: the seam edges cancel, and the radial Jacobian is given by extDeriv_pullback_polarCoord_symm_apply. The bilinear Green formulas in TauCeti.MeasureTheory.Integral.DivergenceTheorem are special cases.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Chapter 16 (Stokes' theorem).
• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Section 4.1 (symplectic area and exactness).

theorem TauCeti.integral_extDeriv_prod_Icc {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : ℝ × ℝ → (ℝ × ℝ) [⋀^Fin 1]→L[ℝ] F} {a b : ℝ × ℝ} (hab : a ≤ b) (hω : ∀ z ∈ Set.Icc a b, ContDiffAt ℝ 1 ω z) : ∫ (z : ℝ × ℝ) in Set.Icc a b, (extDeriv ω z) ![(1, 0), (0, 1)] = ((∫ (t : ℝ) in a.2..b.2, (ω (b.1, t)) fun (x : Fin 1) => (0, 1)) - ∫ (t : ℝ) in a.2..b.2, (ω (a.1, t)) fun (x : Fin 1) => (0, 1)) - ((∫ (s : ℝ) in a.1..b.1, (ω (s, b.2)) fun (x : Fin 1) => (1, 0)) - ∫ (s : ℝ) in a.1..b.1, (ω (s, a.2)) fun (x : Fin 1) => (1, 0))

Stokes' formula on a rectangle for a one-form that is C¹ near the closed rectangle. The right and bottom edges have positive signs; the left and top edges have negative signs.

theorem TauCeti.integrableOn_fderiv_sub_fderiv_Icc {U : Set (ℝ × ℝ)} {fs ft : ℝ × ℝ → ℝ} {a b : ℝ × ℝ} (hU : IsOpen U) (hfs : ContDiffOn ℝ 1 fs U) (hft : ContDiffOn ℝ 1 ft U) (habU : Set.Icc a b ⊆ U) : MeasureTheory.IntegrableOn (fun (z : ℝ × ℝ) => (fderiv ℝ ft z) (1, 0) - (fderiv ℝ fs z) (0, 1)) (Set.Icc a b) MeasureTheory.volume

The exterior derivative ∂_s f_t - ∂_t f_s of a one-form f_s ds + f_t dt that is C¹ over an open neighbourhood of a rectangle is integrable over the rectangle.

theorem TauCeti.integral_fderiv_sub_fderiv_Icc {U : Set (ℝ × ℝ)} {fs ft : ℝ × ℝ → ℝ} {a b : ℝ × ℝ} (hU : IsOpen U) (hfs : ContDiffOn ℝ 1 fs U) (hft : ContDiffOn ℝ 1 ft U) (hab : a ≤ b) (habU : Set.Icc a b ⊆ U) : ∫ (z : ℝ × ℝ) in Set.Icc a b, (fderiv ℝ ft z) (1, 0) - (fderiv ℝ fs z) (0, 1) = (((∫ (s : ℝ) in a.1..b.1, fs (s, a.2)) + ∫ (t : ℝ) in a.2..b.2, ft (b.1, t)) - ∫ (s : ℝ) in a.1..b.1, fs (s, b.2)) - ∫ (t : ℝ) in a.2..b.2, ft (a.1, t)

Green's theorem on a rectangle. For a one-form f_s ds + f_t dt that is C¹ over an open neighbourhood of a rectangle [a₁, b₁] × [a₂, b₂], the integral of its exterior derivative ∂_s f_t - ∂_t f_s over the rectangle is its integral over the positively oriented boundary.

theorem TauCeti.integral2_extDeriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : ℝ × ℝ → (ℝ × ℝ) [⋀^Fin 1]→L[ℝ] F} {a₁ a₂ b₁ b₂ : ℝ} (hω : ∀ z ∈ Set.uIcc a₁ b₁ ×ˢ Set.uIcc a₂ b₂, ContDiffAt ℝ 1 ω z) : ∫ (s : ℝ) in a₁..b₁, ∫ (t : ℝ) in a₂..b₂, (extDeriv ω (s, t)) ![(1, 0), (0, 1)] = ((∫ (t : ℝ) in a₂..b₂, (ω (b₁, t)) fun (x : Fin 1) => (0, 1)) - ∫ (t : ℝ) in a₂..b₂, (ω (a₁, t)) fun (x : Fin 1) => (0, 1)) - ((∫ (s : ℝ) in a₁..b₁, (ω (s, b₂)) fun (x : Fin 1) => (1, 0)) - ∫ (s : ℝ) in a₁..b₁, (ω (s, a₂)) fun (x : Fin 1) => (1, 0))

Stokes' formula on a rectangle, as an iterated integral over oriented intervals, for a one-form that is C¹ near the closed rectangle. The corners may come in either order.

theorem TauCeti.integral2_slice_sub_eq_sides {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ψ : (ℝ × ℝ) × ℝ → ((ℝ × ℝ) × ℝ) [⋀^Fin 2]→L[ℝ] F} (hψ : ContDiff ℝ 1 ψ) (hdψ : extDeriv ψ = 0) (a b : ℝ × ℝ) : (∫ (s : ℝ) in a.1..b.1, ∫ (t : ℝ) in a.2..b.2, (ψ ((s, t), 1)) ![((1, 0), 0), ((0, 1), 0)]) - ∫ (s : ℝ) in a.1..b.1, ∫ (t : ℝ) in a.2..b.2, (ψ ((s, t), 0)) ![((1, 0), 0), ((0, 1), 0)] = ((∫ (t : ℝ) in a.2..b.2, ∫ (c : ℝ) in 0..1, (ψ ((a.1, t), c)) ![((0, 1), 0), (0, 1)]) - ∫ (t : ℝ) in a.2..b.2, ∫ (c : ℝ) in 0..1, (ψ ((b.1, t), c)) ![((0, 1), 0), (0, 1)]) - ((∫ (s : ℝ) in a.1..b.1, ∫ (c : ℝ) in 0..1, (ψ ((s, a.2), c)) ![((1, 0), 0), (0, 1)]) - ∫ (s : ℝ) in a.1..b.1, ∫ (c : ℝ) in 0..1, (ψ ((s, b.2), c)) ![((1, 0), 0), (0, 1)])

Stokes' formula on the boundary of a cube for a closed two-form ψ that is C¹ on (ℝ × ℝ) × ℝ: its integrals over the top and bottom faces [a, b] × {1} and [a, b] × {0} differ by the signed sum of its integrals over the four side faces, each parametrized by the direction of its edge followed by the last coordinate. All integrals are iterated integrals over oriented intervals, so the corners a and b may come in either order.

The proof applies Stokes' formula on the rectangle to the cylinder homotopy h ψ, whose exterior derivative is the difference of the top and bottom slices of the closed form ψ.

theorem TauCeti.extDeriv_pullback_polarCoord_symm_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : ℂ → ℂ [⋀^Fin 1]→L[ℝ] F} (z₀ : ℂ) (p : ℝ × ℝ) (hω : DifferentiableAt ℝ ω (z₀ + ↑Complex.polarCoord.symm p)) : (extDeriv (fun (q : ℝ × ℝ) => (ω (z₀ + ↑Complex.polarCoord.symm q)).compContinuousLinearMap (fderiv ℝ (fun (q : ℝ × ℝ) => z₀ + ↑Complex.polarCoord.symm q) q)) p) ![(1, 0), (0, 1)] = p.1 • (extDeriv ω (z₀ + ↑Complex.polarCoord.symm p)) ![1, Complex.I]

The exterior derivative of a one-form pulled back by the translated polar map, evaluated on the standard pair, includes exactly the radial Jacobian.

theorem TauCeti.integral_extDeriv_annulus {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : ℂ → ℂ [⋀^Fin 1]→L[ℝ] F} (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hω : ∀ z ∈ {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 1 ω z) : ∫ (z : ℂ) in {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, (extDeriv ω z) ![1, Complex.I] = (∫ (θ : ℝ) in -Real.pi..Real.pi, (ω (circleMap z₀ b θ)) fun (x : Fin 1) => circleMap 0 b θ * Complex.I) - ∫ (θ : ℝ) in -Real.pi..Real.pi, (ω (circleMap z₀ a θ)) fun (x : Fin 1) => circleMap 0 a θ * Complex.I

Stokes' formula for a real one-form near a closed annulus. Both circles are traversed counterclockwise; the inner circle is subtracted. The inner radius may be zero.

theorem TauCeti.integral_extDeriv_closedBall {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {ω : ℂ → ℂ [⋀^Fin 1]→L[ℝ] F} {z₀ : ℂ} {r : ℝ} (hr : 0 ≤ r) (hω : ∀ z ∈ Metric.closedBall z₀ r, ContDiffAt ℝ 1 ω z) : ∫ (z : ℂ) in Metric.closedBall z₀ r, (extDeriv ω z) ![1, Complex.I] = ∫ (θ : ℝ) in -Real.pi..Real.pi, (ω (circleMap z₀ r θ)) fun (x : Fin 1) => circleMap 0 r θ * Complex.I

Stokes' formula on a closed disc. The tangent vector in the boundary integral is the derivative of the counterclockwise circle parametrization.