Integrability and Stokes formulas for symplectic area

For a constant symplectic form ω, the primitive λₓ(v) = ½ ω(x, v) identifies the symplectic area of a C² map on a closed rectangle with the integral of λ over its positively oriented boundary (TauCeti.SymplecticForm.integral_fderiv_apply_prod_Icc), and the symplectic area of a C² map on a closed annulus with the difference of its boundary actions. The outer and inner circles are both parametrized counterclockwise on [-π, π], and the inner action is subtracted. No extension across the inner disc is needed. Together with the isoperimetric inequality for the boundary loops, this is the Stokes step used in energy decay and removal of singularities for holomorphic curves.

For a loop x : [0, 1] → V, the integral of λ along it is the loop area a(x) = ½ ∫₀¹ ω(x(t), x'(t)) dt (TauCeti.SymplecticForm.loopArea). If the bottom and top sides of a map u on [a, b] × [0, 1] agree, so that each t ↦ u(s, t) is a loop, the rectangle formula says that the symplectic area of u is a(u(b, ·)) - a(u(a, ·)) (TauCeti.SymplecticForm.integral_symplecticForm_fderiv_eq_loopArea_sub). In particular the loop area of a closed loop is the symplectic area of the cone r x(t) bounding it (TauCeti.SymplecticForm.integral_symplecticForm_fderiv_smul_eq_loopArea). Reparametrizing one period of a 2π-periodic curve backwards as a loop on [0, 1] negates its area over [-π, π] (TauCeti.SymplecticForm.loopArea_comp_sub_mul).

A square-integrable differential also gives an integrable symplectic area density, on any domain. Pairing bounded loops with functions whose norms have vanishing mean over [0, 1] gives integrals of the symplectic form that tend to zero (TauCeti.SymplecticForm.tendsto_integral_apply_of_tendsto_integral_norm).

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Section 4.5.

theorem TauCeti.SymplecticForm.integrableOn_fderiv_apply_of_integrableOn_norm_fderiv_sq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℂ → V} {D : Set ℂ} (henergy : MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖fderiv ℝ u z‖ ^ 2) D MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (z : ℂ) => (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) 1) ((fderiv ℝ u z) Complex.I)) D MeasureTheory.volume

A square-integrable differential has integrable symplectic area density.

theorem TauCeti.SymplecticForm.tendsto_integral_apply_of_tendsto_integral_norm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : SymplecticForm V} {ι : Type u_2} {l : Filter ι} {y d : ι → ℝ → V} {R : ℝ} (hy : ∀ (i : ι) (t : ℝ), ‖y i t‖ ≤ R) (hd : ∀ (i : ι), Continuous (d i)) (hdl : Filter.Tendsto (fun (i : ι) => ∫ (t : ℝ) in 0..1, ‖d i t‖) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (t : ℝ) in 0..1, (fun (v w : V) => (ω.toBilinForm v) w) (y i t) (d i t)) l (nhds 0)

Pairing with functions of vanishing mean norm. If the loops y_i are bounded by R and the integrals over [0, 1] of the norms of the continuous d_i tend to 0, then so do the integrals ∫₀¹ ω(y_i(t), d_i(t)) dt.

theorem TauCeti.SymplecticForm.integral_fderiv_apply_prod_Icc {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℝ × ℝ → V} {a b : ℝ × ℝ} (hle : a ≤ b) (hu : ∀ z ∈ Set.Icc a b, ContDiffAt ℝ 2 u z) : ∫ (z : ℝ × ℝ) in Set.Icc a b, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) (1, 0)) ((fderiv ℝ u z) (0, 1)) = 1 / 2 * (((∫ (t : ℝ) in a.2..b.2, (fun (v w : V) => (ω.toBilinForm v) w) (u (b.1, t)) ((fderiv ℝ u (b.1, t)) (0, 1))) - ∫ (t : ℝ) in a.2..b.2, (fun (v w : V) => (ω.toBilinForm v) w) (u (a.1, t)) ((fderiv ℝ u (a.1, t)) (0, 1))) - ((∫ (s : ℝ) in a.1..b.1, (fun (v w : V) => (ω.toBilinForm v) w) (u (s, b.2)) ((fderiv ℝ u (s, b.2)) (1, 0))) - ∫ (s : ℝ) in a.1..b.1, (fun (v w : V) => (ω.toBilinForm v) w) (u (s, a.2)) ((fderiv ℝ u (s, a.2)) (1, 0))))

Stokes' formula for symplectic area on a rectangle. If u is C² at every point of the rectangle Icc a b ⊆ ℝ × ℝ, its symplectic area over the rectangle is the integral of the primitive λₓ(v) = ½ ω(x, v) along the positively oriented boundary: the right side minus the left side of t ↦ ½ ω(u, ∂t u), minus the top side minus the bottom side of s ↦ ½ ω(u, ∂s u).

noncomputable def TauCeti.SymplecticForm.loopArea {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) (x : ℝ → V) : ℝ

The symplectic area ½ ∫₀¹ ω(x(t), x'(t)) dt of a loop x : [0, 1] → V: the integral of the primitive λₓ(v) = ½ ω(x, v) of ω along the loop. For a closed loop it is the symplectic area of the cone r x(t) bounding it (SymplecticForm.integral_symplecticForm_fderiv_smul_eq_loopArea).

theorem TauCeti.SymplecticForm.loopArea_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) (x : ℝ → V) : ω.loopArea x = 1 / 2 * ∫ (t : ℝ) in 0..1, (fun (v w : V) => (ω.toBilinForm v) w) (x t) (deriv x t)

@[simp]

theorem TauCeti.SymplecticForm.loopArea_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) (v : V) : (ω.loopArea fun (x : ℝ) => v) = 0

A constant loop has zero symplectic area.

theorem TauCeti.SymplecticForm.loopArea_comp_sub_mul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) {g : ℝ → V} (hg : Function.Periodic g (2 * Real.pi)) (θ₀ : ℝ) : (ω.loopArea fun (t : ℝ) => g (θ₀ - 2 * Real.pi * t)) = -(1 / 2 * ∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (g θ) (deriv g θ))

The loop area of a circle traversed backwards. If g is 2π-periodic, the loop t ↦ g(θ₀ - 2πt) runs once through a period of g in the reverse direction, so its loop area is minus the area ½ ∫_{-π}^{π} ω(g(θ), g'(θ)) dθ of g over one period.

theorem TauCeti.SymplecticForm.loopArea_comp_add_mul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) {g : ℝ → V} (hg : Function.Periodic g (2 * Real.pi)) (θ₀ : ℝ) : (ω.loopArea fun (t : ℝ) => g (θ₀ + 2 * Real.pi * t)) = 1 / 2 * ∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (g θ) (deriv g θ)

The loop area of a circle traversed forwards. If g is 2π-periodic, the loop t ↦ g(θ₀ + 2πt) runs once through a period of g, so its loop area is the area ½ ∫_{-π}^{π} ω(g(θ), g'(θ)) dθ of g over one period.

theorem TauCeti.SymplecticForm.loopArea_comp_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) {x : ℝ → V} (hx : Function.Periodic x 1) : (ω.loopArea fun (t : ℝ) => x (-t)) = -ω.loopArea x

The loop area of a loop traversed backwards. If x is 1-periodic, the loop t ↦ x(-t) has the opposite loop area.

theorem TauCeti.SymplecticForm.integral_symplecticForm_fderiv_eq_loopArea_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {u : ℝ × ℝ → V} {a b : ℝ} (ω : SymplecticForm V) (hab : a ≤ b) (hu : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, ContDiffAt ℝ 2 u z) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) : ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag) = (ω.loopArea fun (t : ℝ) => u (b, t)) - ω.loopArea fun (t : ℝ) => u (a, t)

The symplectic area of a cylinder. Let u be C² near [a, b] × [0, 1], with u(s, 1) = u(s, 0) for s ∈ [a, b], so that each t ↦ u(s, t) is a loop. Then the symplectic area of u over the rectangle is the area of the loop at s = b minus the area of the loop at s = a.

theorem TauCeti.SymplecticForm.integral_symplecticForm_fderiv_smul_eq_loopArea {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {x : ℝ → V} (hx : ∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ 2 x t) (hx₁ : x 1 = x 0) : ∫ (z : ℝ × ℝ) in Set.Icc 0 1 ×ˢ Set.Icc 0 1, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ (fun (w : ℝ × ℝ) => w.1 • x w.2) z) stdComplexLineReal) ((fderiv ℝ (fun (w : ℝ × ℝ) => w.1 • x w.2) z) stdComplexLineImag) = ω.loopArea x

The loop area is the area of a cap. For a loop x that is C² near [0, 1] with x 1 = x 0, the symplectic area of the cone D(r, t) = r x(t) over [0, 1] × [0, 1], a disc bounding x, is the loop area of x.

theorem TauCeti.SymplecticForm.integral_fderiv_apply_annulus {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℂ → V} (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hu : ∀ z ∈ {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z) : ∫ (z : ℂ) in {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) 1) ((fderiv ℝ u z) Complex.I) = 1 / 2 * ((∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (u (circleMap z₀ b θ)) (deriv (fun (θ : ℝ) => u (circleMap z₀ b θ)) θ)) - ∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (u (circleMap z₀ a θ)) (deriv (fun (θ : ℝ) => u (circleMap z₀ a θ)) θ))

Stokes' formula for symplectic area on an annulus. The pullback area of a C² map is the outer boundary action minus the inner boundary action for the primitive λₓ(v) = ½ ω(x, v). This identity does not require any regularity on the inner disc or a holomorphicity hypothesis.