Symplectic Stokes on a finite-energy punctured disc

The symplectic area of a finite-energy map on a punctured disc equals the action of its outer boundary loop for the primitive λₓ(v) = ½ ω(x, v). No extension, bounded image, or boundary decay at the puncture is assumed. In particular this identity applies before removal of a singularity has been proved. Both results hold in any finite-dimensional real normed space.

The vanishing-action result requires C¹ regularity near the punctured closed disc and a square-integrable differential. The Stokes identity requires C² regularity there, including the outer boundary. For a J-holomorphic map, this area identity is the input to the radial energy-decay argument in removal of singularities. For a map which is C² on the whole closed disc the energy is automatically finite, which gives Stokes' formula on the closed disc (TauCeti.SymplecticForm.integral_fderiv_apply_closedBall, and in the real coordinates ℝ × ℝ ≃ ℂ, TauCeti.SymplecticForm.integral_fderiv_apply_preimage_closedBall).

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Sections 4.4 and 4.5.

theorem TauCeti.SymplecticForm.exists_tendsto_integral_apply_circleMap_nhds_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℂ → V} (z₀ : ℂ) {b : ℝ} (hb : 0 < b) (hu : ∀ z ∈ {z : ℂ | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 1 u z) (henergy : MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖fderiv ℝ u z‖ ^ 2) {z : ℂ | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b} MeasureTheory.volume) : ∃ (r : ℕ → ℝ), (∀ (n : ℕ), 0 < r n ∧ r n ≤ b) ∧ Filter.Tendsto r Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (u (circleMap z₀ (r n) θ)) (deriv (fun (θ : ℝ) => u (circleMap z₀ (r n) θ)) θ)) Filter.atTop (nhds 0)

Finite energy gives a sequence of shrinking circles whose symplectic boundary actions tend to zero. No boundedness or extension of the map at the puncture is required.

theorem TauCeti.SymplecticForm.integral_fderiv_apply_punctured_disc {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℂ → V} (z₀ : ℂ) {b : ℝ} (hb : 0 < b) (hu : ∀ z ∈ {z : ℂ | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, ContDiffAt ℝ 2 u z) (henergy : MeasureTheory.IntegrableOn (fun (z : ℂ) => ‖fderiv ℝ u z‖ ^ 2) {z : ℂ | 0 < ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b} MeasureTheory.volume) : ∫ (z : ℂ) in {z : ℂ | 0 < ‖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 θ)) θ)

Stokes' formula on a finite-energy punctured disc. The integral of the pullback of a constant symplectic form equals the outer boundary action. The value of the map at the puncture is unrestricted, and the map need not be holomorphic.

theorem TauCeti.SymplecticForm.integral_fderiv_apply_closedBall {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℂ → V} (z₀ : ℂ) {b : ℝ} (hb : 0 < b) (hu : ∀ z ∈ Metric.closedBall z₀ b, ContDiffAt ℝ 2 u z) : ∫ (z : ℂ) in Metric.closedBall 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 θ)) θ)

Stokes' formula on a closed disc. For a map which is C² at every point of the closed disc ‖z - z₀‖ ≤ b, the integral over the disc of the pullback of a constant symplectic form is half the integral of ω(u, ∂_θ u) along the boundary circle.

theorem TauCeti.SymplecticForm.integral_fderiv_apply_preimage_closedBall {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {u : ℝ × ℝ → V} (z₀ : ℂ) {b : ℝ} (hb : 0 < b) (hu : ∀ z ∈ ⇑Complex.equivRealProdCLM.symm ⁻¹' Metric.closedBall z₀ b, ContDiffAt ℝ 2 u z) : ∫ (z : ℝ × ℝ) in ⇑Complex.equivRealProdCLM.symm ⁻¹' Metric.closedBall z₀ b, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag) = 1 / 2 * ∫ (θ : ℝ) in -Real.pi..Real.pi, (fun (v w : V) => (ω.toBilinForm v) w) (u (Complex.equivRealProdCLM (circleMap z₀ b θ))) (deriv (fun (θ : ℝ) => u (Complex.equivRealProdCLM (circleMap z₀ b θ))) θ)

Stokes' formula on a closed disc, in real coordinates. For a map u : ℝ × ℝ → V which is C² at every point of the preimage of the closed disc ‖z - z₀‖ ≤ b under ℝ × ℝ ≃ ℂ, the symplectic area of u over this preimage is half the integral of ω(u, ∂_θ u) along the boundary circle.