Curvature of Hamiltonian perturbations and the Floer energy identity

Inhomogeneous Floer equations on a Riemann surface with coordinates z = (s, t) are perturbed by a Hamiltonian-valued one-form K = K_s ds + K_t dt, given here by two families of Hamiltonians Ks Kt : ℝ × ℝ → V → ℝ on a symplectic vector space (V, ω). Writing X_F for the Hamiltonian vector field (ω(X_F, ·) = dF) and {F, G} = ω(X_F, X_G) for the Poisson bracket, we define:

• the curvature R_K = ∂_s K_t - ∂_t K_s - {K_s, K_t}, a function of (z, x);
• the perturbed derivative du - X_K = du - ds ⊗ X_{K_s}(u) - dt ⊗ X_{K_t}(u) of a map u : ℝ × ℝ → V;
• the Floer energy density ω(∂_s u - X_{K_s}(u), ∂_t u - X_{K_t}(u)).

The Floer equation (du - X_K)^{0,1} = 0 says that the perturbed derivative is complex linear for the standard complex structure on ℝ × ℝ, or in coordinates ∂_s u - X_{K_s}(u) + J (∂_t u - X_{K_t}(u)) = 0. Since the energy density is by definition the symplectic area density of the perturbed derivative, for solutions it is nonnegative under tameness (SymplecticForm.floerEnergyDensity_nonneg) and is half the metric energy density |du - X_K|², by IsComplexLinearMap.stdComplexLineEnergyDensity_eq_two_mul_symplecticForm. For a merely tame J the form ω(·, J ·) is not a metric, so the energy is compared with the norm instead: if c ‖v‖² ≤ ω(v, J v) and ‖J v‖ ≤ M ‖v‖, the energy density of a solution bounds c (‖∂_s u - X_{K_s}‖² + ‖∂_t u - X_{K_t}‖²) up to the factor 1 + M², pointwise and after integration. Such constants exist uniformly over a compact set of tamed structures (IsCompact.exists_pos_forall_mul_norm_sq_le), so on a compact window of tamed structures the energy bounds the L² norm of the perturbed derivative.

The main result is the energy identity: pointwise, ω(∂_s u - X_{K_s}, ∂_t u - X_{K_t}) = ω(∂_s u, ∂_t u) + d(K(u)) - R_K(u), where d(K(u)) = ∂_s (K_t(u)) - ∂_t (K_s(u)) is the exterior derivative of the pulled-back one-form K(u) = K_s(u) ds + K_t(u) dt. Integrated over a rectangle using Stokes' formula, the energy is the symplectic area plus the boundary integral of K(u) minus the integral of the curvature. Curvature bounds therefore turn into energy bounds. For a cylindrical perturbation K = H_t dt, the curvature vanishes; for the perturbation K = H_{(s, t)} dt of a homotopy of Hamiltonians, it is ∂_s H_{(s, t)}, and in particular for a continuation perturbation K = β(s) H_t dt it is β'(s) H_t.

Main definitions

• TauCeti.SymplecticForm.hamiltonianCurvature: the curvature R_K.
• TauCeti.SymplecticForm.hamiltonianOneForm: the vector-valued one-form X_K = ds ⊗ X_{K_s} + dt ⊗ X_{K_t}.
• TauCeti.SymplecticForm.perturbedFDeriv: the perturbed derivative du - X_K.
• TauCeti.SymplecticForm.floerEnergyDensity: the Floer energy density.
• TauCeti.SymplecticForm.stripEnergyMeasure: the measure on ℝ giving each set A of s-values the energy over A × [0, 1].

Main results

• SymplecticForm.floerEnergyDensity_eq: the pointwise energy identity.
• SymplecticForm.floerEnergyDensity_nonneg: the energy density of a solution is nonnegative.
• SymplecticForm.floerEnergyDensity_eq_zero_iff: under tameness, the energy density of a solution vanishes exactly where the perturbed derivative does.
• SymplecticForm.mul_norm_sq_add_norm_sq_perturbedFDeriv_le_mul_floerEnergyDensity and SymplecticForm.setLIntegral_norm_sq_add_norm_sq_perturbedFDeriv_le: the energy controls the perturbed derivative, pointwise and in L².
• SymplecticForm.norm_fderiv_stdComplexLineReal_sq_le: the energy density and the Hamiltonian vector field control ‖∂_s u‖².
• SymplecticForm.integral_floerEnergyDensity: the energy identity on a rectangle.
• SymplecticForm.integral_floerEnergyDensity_sub_add_eq_of_eventuallyEq_zero: the energy minus the symplectic area plus the integrated curvature does not change when a compact domain is shrunk to a part outside which the perturbation vanishes locally.
• SymplecticForm.floerEnergyDensity_add_hamiltonianCurvature_eq: for a C² map, the energy density plus the curvature is the exterior derivative of the one-form K(u) + λ(u), where λₓ(v) = ½ ω(x, v) is the primitive of ω; this globalizes the energy identity to domains that are not rectangles.
• SymplecticForm.isComplexLinearMap_perturbedFDeriv_iff: the coordinate form of the Floer equation.
• SymplecticForm.hamiltonianCurvature_zero_left, SymplecticForm.hamiltonianCurvature_cylindrical, SymplecticForm.hamiltonianCurvature_homotopy, SymplecticForm.hamiltonianCurvature_continuation: the curvature of perturbations without ds component. Its local form along a line near which the perturbation is cylindrical is SymplecticForm.hamiltonianCurvature_eq_zero_of_cylindrical, the constant-form case of the manifold statement in TauCeti.Geometry.Symplectic.Floer.Manifold.
• SymplecticForm.perturbedFDeriv_add_const, SymplecticForm.floerEnergyDensity_add_const, SymplecticForm.hamiltonianCurvature_add_const: adding a target-independent one-form k = k_s ds + k_t dt to K changes neither the perturbed derivative nor the energy density, and adds ∂_s k_t - ∂_t k_s to the curvature (SymplecticForm.hamiltonianCurvature_const).
• SymplecticForm.hamiltonianCurvature_congr_of_eventuallyEq, SymplecticForm.hamiltonianCurvature_comp_add_right: the curvature is local in the domain and commutes with domain translations (so data that agree on an open set have the same integrated curvature over it, SymplecticForm.setLIntegral_enorm_hamiltonianCurvature_congr_of_isOpen), and likewise for the perturbed derivative (SymplecticForm.perturbedFDeriv_congr_of_eventuallyEq, SymplecticForm.perturbedFDeriv_comp_add_right) and the energy density (SymplecticForm.floerEnergyDensity_congr_of_eventuallyEq, SymplecticForm.floerEnergyDensity_comp_add_right); hence translations preserve the energy (SymplecticForm.lintegral_floerEnergyDensity_comp_add_right) and translate the strip energy measure (SymplecticForm.stripEnergyMeasure_comp_add_right).

References

• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, Section 8.1, on Hamiltonian perturbations, their curvature and the energy identity.
• P. Seidel, Fukaya categories and Picard–Lefschetz theory, Section 8, on inhomogeneous pseudoholomorphic maps and their energy.

theorem TauCeti.fderiv_mul_apply_stdComplexLineReal {β h : ℝ → ℝ} {z : ℝ × ℝ} (hβ : DifferentiableAt ℝ β z.1) (hh : DifferentiableAt ℝ h z.2) : (fderiv ℝ (fun (w : ℝ × ℝ) => β w.1 * h w.2) z) stdComplexLineReal = deriv β z.1 * h z.2

The ∂_s derivative of a product β(s) h(t) is β'(s) h(t). This is the domain part of the curvature of a continuation perturbation K = β(s) H_t dt, for any target.

theorem TauCeti.fderiv_cylindrical_apply_stdComplexLineReal {X : Type u_1} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (H : ℝ → X → G) (z : ℝ × ℝ) (x : X) : (fderiv ℝ (fun (w : ℝ × ℝ) => H w.2 x) z) stdComplexLineReal = 0

The ∂_s derivative of a family H_t(x) independent of s vanishes. This is the domain part of the curvature of a cylindrical perturbation K = H_t dt, for any target.

noncomputable def TauCeti.SymplecticForm.hamiltonianCurvature {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) : ℝ

The curvature R_K = ∂_s K_t - ∂_t K_s - {K_s, K_t} of the Hamiltonian perturbation one-form K = K_s ds + K_t dt, at the domain point z = (s, t) and the target point x.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature Ks Kt z x = (fderiv ℝ (fun (w : ℝ × ℝ) => Kt w x) z) stdComplexLineReal - (fderiv ℝ (fun (w : ℝ × ℝ) => Ks w x) z) stdComplexLineImag - ω.poissonBracket (Ks z) (Kt z) x

theorem TauCeti.SymplecticForm.hamiltonianCurvature_zero_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Kt : ℝ × ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature (fun (x : ℝ × ℝ) (x_1 : V) => 0) Kt z x = (fderiv ℝ (fun (w : ℝ × ℝ) => Kt w x) z) stdComplexLineReal

Without a ds component, the curvature of K = K_t dt is ∂_s K_t.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_cylindrical {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) z x = 0

A cylindrical perturbation K = H_t dt, independent of s, has zero curvature.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_homotopy {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : ℝ × ℝ → V → ℝ} {z : ℝ × ℝ} {x : V} (hH : DifferentiableAt ℝ (fun (w : ℝ × ℝ) => H w x) z) : ω.hamiltonianCurvature (fun (x : ℝ × ℝ) (x_1 : V) => 0) H z x = deriv (fun (s : ℝ) => H (s, z.2) x) z.1

The curvature of a homotopy of Hamiltonians. A perturbation K = H_{(s, t)} dt without ds component, given by a family H_{(s, t)} of Hamiltonians, has curvature ∂_s H_{(s, t)}.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_continuation {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {β : ℝ → ℝ} {H : ℝ → V → ℝ} {z : ℝ × ℝ} {x : V} (hβ : DifferentiableAt ℝ β z.1) (hH : DifferentiableAt ℝ (fun (t : ℝ) => H t x) z.2) : ω.hamiltonianCurvature (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) (y : V) => β w.1 * H w.2 y) z x = deriv β z.1 * H z.2 x

A continuation perturbation K = β(s) H_t dt has curvature β'(s) H_t.

theorem TauCeti.SymplecticForm.contDiff_uncurry_cylindrical {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {H : ℝ → V → ℝ} (hH : ContDiff ℝ n (Function.uncurry H)) : ContDiff ℝ n (Function.uncurry fun (w : ℝ × ℝ) => H w.2)

The cylindrical perturbation K = H_t dt of a Cⁿ time-dependent Hamiltonian is Cⁿ.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt Ks' Kt' : ℝ × ℝ → V → ℝ} {z : ℝ × ℝ} (hs : Ks =ᶠ[nhds z] Ks') (ht : Kt =ᶠ[nhds z] Kt') : ω.hamiltonianCurvature Ks Kt z = ω.hamiltonianCurvature Ks' Kt' z

The curvature only depends on the germs of the perturbation data at the domain point.

theorem TauCeti.SymplecticForm.setLIntegral_enorm_hamiltonianCurvature_congr_of_isOpen {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt Ks' Kt' : ℝ × ℝ → V → ℝ} {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hs : Set.EqOn Ks Ks' U) (ht : Set.EqOn Kt Kt' U) (u : ℝ × ℝ → V) : ∫⁻ (z : ℝ × ℝ) in U, ‖ω.hamiltonianCurvature Ks Kt z (u z)‖ₑ = ∫⁻ (z : ℝ × ℝ) in U, ‖ω.hamiltonianCurvature Ks' Kt' z (u z)‖ₑ

Perturbation data that agree on an open set have the same integrated curvature over it.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_eq_zero_of_eventuallyEq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt : ℝ × ℝ → V → ℝ} {z : ℝ × ℝ} (hs : Ks =ᶠ[nhds z] 0) (ht : Kt =ᶠ[nhds z] 0) (x : V) : ω.hamiltonianCurvature Ks Kt z x = 0

If both components of a Hamiltonian one-form vanish near a domain point, its curvature vanishes there. No differentiability assumption is needed.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_eq_zero_of_notMem {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt : ℝ × ℝ → V → ℝ} {D : Set (ℝ × ℝ)} (hD : IsClosed D) (hs : ∀ z ∉ D, Ks z = 0) (ht : ∀ z ∉ D, Kt z = 0) {z : ℝ × ℝ} (hz : z ∉ D) (x : V) : ω.hamiltonianCurvature Ks Kt z x = 0

If both components of a Hamiltonian one-form vanish off a closed domain set, its curvature also vanishes off that set. No differentiability assumption is needed.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_add_of_eq_zero_on {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt δs δt : ℝ × ℝ → V → ℝ} {D U : Set (ℝ × ℝ)} (hD : IsClosed D) (hU : IsOpen U) (hDU : D ⊆ U) (hKs : ∀ z ∈ U, Ks z = 0) (hKt : ∀ z ∈ U, Kt z = 0) (hδs : ∀ z ∉ D, δs z = 0) (hδt : ∀ z ∉ D, δt z = 0) (z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature (fun (w : ℝ × ℝ) (y : V) => Ks w y + δs w y) (fun (w : ℝ × ℝ) (y : V) => Kt w y + δt w y) z x = ω.hamiltonianCurvature Ks Kt z x + ω.hamiltonianCurvature δs δt z x

Adding a perturbation supported in a closed set inside an open region where the original one-form vanishes adds their curvatures exactly: there are no mixed Poisson-bracket terms.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (v z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature (fun (w : ℝ × ℝ) => Ks (w + v)) (fun (w : ℝ × ℝ) => Kt (w + v)) z x = ω.hamiltonianCurvature Ks Kt (z + v) x

Curvature commutes with translations of the domain.

noncomputable def TauCeti.SymplecticForm.perturbedFDeriv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : ℝ × ℝ →L[ℝ] V

The perturbed derivative du - X_K of a map u at z, for the perturbation one-form K = K_s ds + K_t dt: it sends a tangent vector (a, b) to du(a, b) - a X_{K_s} - b X_{K_t}, with the Hamiltonian vector fields evaluated at u z.

theorem TauCeti.SymplecticForm.perturbedFDeriv_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z v : ℝ × ℝ) : (ω.perturbedFDeriv Ks Kt u z) v = (fderiv ℝ u z) v - v.1 • ω.hamiltonianVectorField (Ks z) (u z) - v.2 • ω.hamiltonianVectorField (Kt z) (u z)

noncomputable def TauCeti.SymplecticForm.hamiltonianOneForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) : ℝ × ℝ →L[ℝ] V

The Hamiltonian vector field X_K = ds ⊗ X_{K_s} + dt ⊗ X_{K_t} of the perturbation one-form K = K_s ds + K_t dt, at the domain point z and the target point x: it sends a tangent vector (a, b) of the domain to a X_{K_s}(x) + b X_{K_t}(x).

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianOneForm_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (z : ℝ × ℝ) (x : V) (v : ℝ × ℝ) : (ω.hamiltonianOneForm Ks Kt z x) v = v.1 • ω.hamiltonianVectorField (Ks z) x + v.2 • ω.hamiltonianVectorField (Kt z) x

theorem TauCeti.SymplecticForm.contDiffOn_hamiltonianOneForm {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt : ℝ × ℝ → V → ℝ} {W : Set ((ℝ × ℝ) × V)} {n : WithTop ℕ∞} (hW : IsOpen W) (hKs : ContDiffOn ℝ (n + 1) (Function.uncurry Ks) W) (hKt : ContDiffOn ℝ (n + 1) (Function.uncurry Kt) W) : ContDiffOn ℝ n (fun (p : (ℝ × ℝ) × V) => ω.hamiltonianOneForm Ks Kt p.1 p.2) W

On an open set of (ℝ × ℝ) × V, the Hamiltonian one-form of a jointly C^(n+1) perturbation is jointly Cⁿ.

theorem TauCeti.SymplecticForm.perturbedFDeriv_eq_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : ω.perturbedFDeriv Ks Kt u z = fderiv ℝ u z - ω.hamiltonianOneForm Ks Kt z (u z)

The perturbed derivative is du - X_K(u).

@[simp]

theorem TauCeti.SymplecticForm.perturbedFDeriv_apply_stdComplexLineReal {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : (ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal = (fderiv ℝ u z) stdComplexLineReal - ω.hamiltonianVectorField (Ks z) (u z)

The ∂_s component of the perturbed derivative is ∂_s u - X_{K_s}(u).

@[simp]

theorem TauCeti.SymplecticForm.perturbedFDeriv_apply_stdComplexLineImag {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : (ω.perturbedFDeriv Ks Kt u z) stdComplexLineImag = (fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (Kt z) (u z)

The ∂_t component of the perturbed derivative is ∂_t u - X_{K_t}(u).

theorem TauCeti.SymplecticForm.isComplexLinearMap_perturbedFDeriv_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (J : AlmostComplexStructure V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z) ↔ (fderiv ℝ u z) stdComplexLineReal - ω.hamiltonianVectorField (Ks z) (u z) + J.toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (Kt z) (u z)) = 0

The Floer equation in coordinates. The perturbed derivative is complex linear, that is (du - X_K)^{0,1} = 0, exactly when ∂_s u - X_{K_s}(u) + J (∂_t u - X_{K_t}(u)) = 0.

theorem TauCeti.SymplecticForm.perturbedFDeriv_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (v z : ℝ × ℝ) : ω.perturbedFDeriv (fun (w : ℝ × ℝ) => Ks (w + v)) (fun (w : ℝ × ℝ) => Kt (w + v)) (fun (w : ℝ × ℝ) => u (w + v)) z = ω.perturbedFDeriv Ks Kt u (z + v)

The perturbed derivative commutes with translations of the domain: translating the map and the perturbation data by v translates the perturbed derivative by v.

theorem TauCeti.SymplecticForm.perturbedFDeriv_congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) {u u' : ℝ × ℝ → V} {z : ℝ × ℝ} (h : u =ᶠ[nhds z] u') : ω.perturbedFDeriv Ks Kt u z = ω.perturbedFDeriv Ks Kt u' z

The perturbed derivative at z only depends on the germ of the map at z.

theorem TauCeti.SymplecticForm.perturbedFDeriv_congr {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt Ks' Kt' : ℝ × ℝ → V → ℝ} (u : ℝ × ℝ → V) {z : ℝ × ℝ} (hs : Ks z = Ks' z) (ht : Kt z = Kt' z) : ω.perturbedFDeriv Ks Kt u z = ω.perturbedFDeriv Ks' Kt' u z

The perturbed derivative at z only depends on the components of the perturbation at z.

noncomputable def TauCeti.SymplecticForm.floerEnergyDensity {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : ℝ

The Floer energy density ω(∂_s u - X_{K_s}(u), ∂_t u - X_{K_t}(u)) of a map u at z: the symplectic area density of the perturbed derivative.

theorem TauCeti.SymplecticForm.floerEnergyDensity_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : ω.floerEnergyDensity Ks Kt u z = (fun (v w : V) => (ω.toBilinForm v) w) ((ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal) ((ω.perturbedFDeriv Ks Kt u z) stdComplexLineImag)

@[simp]

theorem TauCeti.SymplecticForm.floerEnergyDensity_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (u : ℝ × ℝ → V) (z : ℝ × ℝ) : ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (x : ℝ × ℝ) (x_1 : V) => 0) u z = (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag)

For the zero perturbation the Floer energy density is the symplectic area density ω(∂_s u, ∂_t u).

theorem TauCeti.SymplecticForm.floerEnergyDensity_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (v z : ℝ × ℝ) : ω.floerEnergyDensity (fun (w : ℝ × ℝ) => Ks (w + v)) (fun (w : ℝ × ℝ) => Kt (w + v)) (fun (w : ℝ × ℝ) => u (w + v)) z = ω.floerEnergyDensity Ks Kt u (z + v)

The Floer energy density commutes with translations of the domain.

theorem TauCeti.SymplecticForm.floerEnergyDensity_congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) {u u' : ℝ × ℝ → V} {z : ℝ × ℝ} (h : u =ᶠ[nhds z] u') : ω.floerEnergyDensity Ks Kt u z = ω.floerEnergyDensity Ks Kt u' z

The Floer energy density at z only depends on the germ of the map at z.

theorem TauCeti.SymplecticForm.floerEnergyDensity_congr_perturbation {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt Ks' Kt' : ℝ × ℝ → V → ℝ} (u : ℝ × ℝ → V) {z : ℝ × ℝ} (hs : Ks z = Ks' z) (ht : Kt z = Kt' z) : ω.floerEnergyDensity Ks Kt u z = ω.floerEnergyDensity Ks' Kt' u z

The Floer energy density at z only depends on the values K_s(z) and K_t(z) of the perturbation at z, not on its derivatives.

theorem TauCeti.SymplecticForm.floerEnergyDensity_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) (hu : DifferentiableAt ℝ u z) (hKs : DifferentiableAt ℝ (Function.uncurry Ks) (z, u z)) (hKt : DifferentiableAt ℝ (Function.uncurry Kt) (z, u z)) : ω.floerEnergyDensity Ks Kt u z = (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag) + ((fderiv ℝ (fun (w : ℝ × ℝ) => Kt w (u w)) z) stdComplexLineReal - (fderiv ℝ (fun (w : ℝ × ℝ) => Ks w (u w)) z) stdComplexLineImag) - ω.hamiltonianCurvature Ks Kt z (u z)

The pointwise energy identity. The Floer energy density is the symplectic area density ω(∂_s u, ∂_t u), plus the exterior derivative ∂_s (K_t(u)) - ∂_t (K_s(u)) of the pulled-back one-form K(u), minus the curvature R_K(u).

theorem TauCeti.SymplecticForm.floerEnergyDensity_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} (hJ : ω.Tames J) (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z)) : 0 ≤ ω.floerEnergyDensity Ks Kt u z

Nonnegativity of the Floer energy density. If the perturbed derivative of u at z is complex linear for an almost complex structure J tamed by ω, that is if u solves the Floer equation at z, then the Floer energy density at z is nonnegative.

theorem TauCeti.SymplecticForm.floerEnergyDensity_zero_left_nonneg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} (hJ : ω.Tames J) (hfloer : (fderiv ℝ u z) stdComplexLineReal + J.toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (Kt z) (u z)) = 0) : 0 ≤ ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) Kt u z

The Floer energy density of a solution of the Floer equation ∂_s u + J (∂_t u - X_{K_t}(u)) = 0 at z, for the perturbation K = K_t dt with a domain-dependent Hamiltonian K_t, is nonnegative when J is tamed by ω.

theorem TauCeti.SymplecticForm.floerEnergyDensity_eq_of_isComplexLinearMap {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z)) : ω.floerEnergyDensity Ks Kt u z = (fun (v w : V) => (ω.toBilinForm v) w) ((ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal) (J.toLinearMap ((ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal))

For a solution of the Floer equation at z, the t-component of the perturbed derivative is J applied to its s-component a = ∂_s u - X_{K_s}, so the Floer energy density is ω(a, J a).

theorem TauCeti.SymplecticForm.floerEnergyDensity_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} (hJ : ω.Tames J) (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z)) : ω.floerEnergyDensity Ks Kt u z = 0 ↔ ω.perturbedFDeriv Ks Kt u z = 0

For a solution of the Floer equation with J tamed by ω, the Floer energy density at z vanishes exactly when the perturbed derivative du - X_K vanishes at z.

theorem TauCeti.SymplecticForm.mul_norm_sq_add_norm_sq_perturbedFDeriv_le_mul_floerEnergyDensity {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} {c M : ℝ} (hc : 0 ≤ c) (hJc : ∀ (v : V), c * ‖v‖ ^ 2 ≤ (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v)) (hJM : ∀ (v : V), ‖J.toLinearMap v‖ ≤ M * ‖v‖) (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z)) : c * (‖(ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal‖ ^ 2 + ‖(ω.perturbedFDeriv Ks Kt u z) stdComplexLineImag‖ ^ 2) ≤ (1 + M ^ 2) * ω.floerEnergyDensity Ks Kt u z

Coercivity of the Floer energy density. Let u solve the Floer equation at z for an almost complex structure J with c ‖v‖² ≤ ω(v, J v) and ‖J v‖ ≤ M ‖v‖ for all v, where 0 ≤ c. Then the energy density controls both components of the perturbed derivative: c (‖∂_s u - X_{K_s}‖² + ‖∂_t u - X_{K_t}‖²) ≤ (1 + M²) ω(∂_s u - X_{K_s}, ∂_t u - X_{K_t}). For J ranging over a compact set of tamed structures, uniform constants c > 0 and M exist by IsCompact.exists_pos_forall_mul_norm_sq_le and the boundedness of compact sets.

theorem TauCeti.SymplecticForm.norm_fderiv_stdComplexLineReal_sq_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) {J : AlmostComplexStructure V} {c : ℝ} (hc : 0 < c) (hJc : ∀ (v : V), c * ‖v‖ ^ 2 ≤ (fun (v w : V) => (ω.toBilinForm v) w) v (J.toLinearMap v)) (h : IsComplexLinearMap (AlmostComplexStructure.product ℝ) J ↑(ω.perturbedFDeriv Ks Kt u z)) : ‖(fderiv ℝ u z) stdComplexLineReal‖ ^ 2 ≤ 2 / c * ω.floerEnergyDensity Ks Kt u z + 2 * ‖ω.hamiltonianVectorField (Ks z) (u z)‖ ^ 2

The energy density bounds the derivative. Let u solve the Floer equation at z for an almost complex structure J with c ‖v‖² ≤ ω(v, J v) for all v, where 0 < c. Then ∂_s u is controlled by the energy density and the Hamiltonian vector field: ‖∂_s u‖² ≤ 2 / c · ω(∂_s u - X_{K_s}, ∂_t u - X_{K_t}) + 2 ‖X_{K_s}(u)‖².

theorem TauCeti.SymplecticForm.floerEnergyDensity_add_hamiltonianCurvature_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {z : ℝ × ℝ} (ω : SymplecticForm V) (hu : ContDiffAt ℝ 2 u z) (hKs : DifferentiableAt ℝ (Function.uncurry Ks) (z, u z)) (hKt : DifferentiableAt ℝ (Function.uncurry Kt) (z, u z)) : ω.floerEnergyDensity Ks Kt u z + ω.hamiltonianCurvature Ks Kt z (u z) = (fderiv ℝ (fun (w : ℝ × ℝ) => Kt w (u w) + 1 / 2 * (fun (v w : V) => (ω.toBilinForm v) w) (u w) ((fderiv ℝ u w) stdComplexLineImag)) z) stdComplexLineReal - (fderiv ℝ (fun (w : ℝ × ℝ) => Ks w (u w) + 1 / 2 * (fun (v w : V) => (ω.toBilinForm v) w) (u w) ((fderiv ℝ u w) stdComplexLineReal)) z) stdComplexLineImag

The energy density plus the curvature is exact. For a C² map u into a symplectic vector space and a perturbation K = K_s ds + K_t dt, the Floer energy density plus the curvature R_K(u) is the exterior derivative ∂_s α_t - ∂_t α_s of the one-form α = K(u) + λ(u), where λₓ(v) = ½ ω(x, v) is the primitive of ω.

Target-independent perturbations

Adding to K a one-form k = k_s ds + k_t dt whose components are functions of the domain point alone changes no Hamiltonian vector field. The perturbed derivative, and with it the Floer equation and the energy density, are unchanged, while the curvature changes by the exterior derivative ∂_s k_t - ∂_t k_s of k. Normalizing the Hamiltonians on the ends by functions of time is the main example.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianCurvature_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (ks kt : ℝ × ℝ → ℝ) (z : ℝ × ℝ) (x : V) : ω.hamiltonianCurvature (fun (w : ℝ × ℝ) (x : V) => ks w) (fun (w : ℝ × ℝ) (x : V) => kt w) z x = (fderiv ℝ kt z) stdComplexLineReal - (fderiv ℝ ks z) stdComplexLineImag

The curvature of a target-independent perturbation k = k_s ds + k_t dt is the exterior derivative ∂_s k_t - ∂_t k_s; the Poisson bracket term vanishes.

@[simp]

theorem TauCeti.SymplecticForm.perturbedFDeriv_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (ks kt : ℝ × ℝ → ℝ) (u : ℝ × ℝ → V) : ω.perturbedFDeriv (fun (w : ℝ × ℝ) (x : V) => ks w) (fun (w : ℝ × ℝ) (x : V) => kt w) u = fderiv ℝ u

A target-independent perturbation has no Hamiltonian vector fields, so its perturbed derivative is the derivative of the map.

theorem TauCeti.SymplecticForm.hamiltonianCurvature_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {Ks Kt : ℝ × ℝ → V → ℝ} {ks kt : ℝ × ℝ → ℝ} {z : ℝ × ℝ} {x : V} (hKs : DifferentiableAt ℝ (fun (w : ℝ × ℝ) => Ks w x) z) (hKt : DifferentiableAt ℝ (fun (w : ℝ × ℝ) => Kt w x) z) (hks : DifferentiableAt ℝ ks z) (hkt : DifferentiableAt ℝ kt z) : ω.hamiltonianCurvature (fun (w : ℝ × ℝ) (y : V) => Ks w y + ks w) (fun (w : ℝ × ℝ) (y : V) => Kt w y + kt w) z x = ω.hamiltonianCurvature Ks Kt z x + ω.hamiltonianCurvature (fun (w : ℝ × ℝ) (x : V) => ks w) (fun (w : ℝ × ℝ) (x : V) => kt w) z x

Adding a target-independent one-form to the perturbation adds its exterior derivative to the curvature: R_{K + k} = R_K + ∂_s k_t - ∂_t k_s, at a point where the components are differentiable in the domain.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianOneForm_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (ks kt : ℝ × ℝ → ℝ) : (ω.hamiltonianOneForm (fun (w : ℝ × ℝ) (y : V) => Ks w y + ks w) fun (w : ℝ × ℝ) (y : V) => Kt w y + kt w) = ω.hamiltonianOneForm Ks Kt

Adding a target-independent one-form to the perturbation does not change the Hamiltonian one-form X_K.

@[simp]

theorem TauCeti.SymplecticForm.perturbedFDeriv_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (ks kt : ℝ × ℝ → ℝ) (u : ℝ × ℝ → V) : ω.perturbedFDeriv (fun (w : ℝ × ℝ) (y : V) => Ks w y + ks w) (fun (w : ℝ × ℝ) (y : V) => Kt w y + kt w) u = ω.perturbedFDeriv Ks Kt u

Adding a target-independent one-form to the perturbation does not change the perturbed derivative, so a map solves the Floer equation for K + k exactly when it solves it for K.

@[simp]

theorem TauCeti.SymplecticForm.floerEnergyDensity_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (ks kt : ℝ × ℝ → ℝ) (u : ℝ × ℝ → V) : ω.floerEnergyDensity (fun (w : ℝ × ℝ) (y : V) => Ks w y + ks w) (fun (w : ℝ × ℝ) (y : V) => Kt w y + kt w) u = ω.floerEnergyDensity Ks Kt u

Adding a target-independent one-form to the perturbation does not change the Floer energy density.

theorem TauCeti.SymplecticForm.lintegral_floerEnergyDensity_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (v : ℝ × ℝ) (S : Set (ℝ × ℝ)) : ∫⁻ (z : ℝ × ℝ) in (fun (x : ℝ × ℝ) => x + v) ⁻¹' S, ENNReal.ofReal (ω.floerEnergyDensity (fun (w : ℝ × ℝ) => Ks (w + v)) (fun (w : ℝ × ℝ) => Kt (w + v)) (fun (w : ℝ × ℝ) => u (w + v)) z) = ∫⁻ (z : ℝ × ℝ) in S, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z)

Translations preserve the energy. Translating the map and the perturbation data by v preserves the energy: the energy of the translate over (· + v) ⁻¹' S is the energy of the original over S.

theorem TauCeti.SymplecticForm.continuousOn_floerEnergyDensity {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hu : ContDiffOn ℝ 1 u U) (hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (U ×ˢ Set.univ)) (hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (U ×ˢ Set.univ)) : ContinuousOn (ω.floerEnergyDensity Ks Kt u) U

For a map and perturbation data that are C¹ over an open set U of the domain, the Floer energy density is continuous on U.

theorem TauCeti.SymplecticForm.continuousOn_hamiltonianCurvature_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hu : ContinuousOn u U) (hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (U ×ˢ Set.univ)) (hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (U ×ˢ Set.univ)) : ContinuousOn (fun (z : ℝ × ℝ) => ω.hamiltonianCurvature Ks Kt z (u z)) U

For perturbation data that is C¹ over an open set U of the domain, the curvature evaluated along a map continuous on U is continuous on U.

theorem TauCeti.SymplecticForm.continuous_hamiltonianCurvature_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) (hu : Continuous u) (hKs : ContDiff ℝ 1 (Function.uncurry Ks)) (hKt : ContDiff ℝ 1 (Function.uncurry Kt)) : Continuous fun (z : ℝ × ℝ) => ω.hamiltonianCurvature Ks Kt z (u z)

For C¹ perturbation data, the curvature evaluated along a continuous map is continuous.

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {U : Set (ℝ × ℝ)} (hU : IsOpen U) (hu : ContDiffOn ℝ 1 u U) (hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (U ×ˢ Set.univ)) (hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (U ×ˢ Set.univ)) {a b : ℝ × ℝ} (hab : a ≤ b) (habU : Set.Icc a b ⊆ U) : ∫ (z : ℝ × ℝ) in Set.Icc a b, ω.floerEnergyDensity Ks Kt u z = (∫ (z : ℝ × ℝ) in Set.Icc a b, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag)) + ((((∫ (s : ℝ) in a.1..b.1, Ks (s, a.2) (u (s, a.2))) + ∫ (t : ℝ) in a.2..b.2, Kt (b.1, t) (u (b.1, t))) - ∫ (s : ℝ) in a.1..b.1, Ks (s, b.2) (u (s, b.2))) - ∫ (t : ℝ) in a.2..b.2, Kt (a.1, t) (u (a.1, t))) - ∫ (z : ℝ × ℝ) in Set.Icc a b, ω.hamiltonianCurvature Ks Kt z (u z)

The energy identity on a rectangle. For a map u and perturbation data that are C¹ over an open neighbourhood of a rectangle [a₁, b₁] × [a₂, b₂], the integral of the Floer energy density over the rectangle is the symplectic area, plus the integral of the pulled-back one-form K(u) = K_s(u) ds + K_t(u) dt over the positively oriented boundary, minus the integral of the curvature R_K(u).

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity_sub_add_eq_of_eventuallyEq_zero {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {P D T : Set (ℝ × ℝ)} (hP : IsOpen P) (hu : ContDiffOn ℝ 1 u P) (hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (P ×ˢ Set.univ)) (hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (P ×ˢ Set.univ)) (hD : IsCompact D) (hDP : D ⊆ P) (hTD : T ⊆ D) (hKsD : ∀ z ∈ D \ T, Ks =ᶠ[nhds z] 0) (hKtD : ∀ z ∈ D \ T, Kt =ᶠ[nhds z] 0) : ((∫ (z : ℝ × ℝ) in D, ω.floerEnergyDensity Ks Kt u z) - ∫ (z : ℝ × ℝ) in D, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag)) + ∫ (z : ℝ × ℝ) in D, ω.hamiltonianCurvature Ks Kt z (u z) = ((∫ (z : ℝ × ℝ) in T, ω.floerEnergyDensity Ks Kt u z) - ∫ (z : ℝ × ℝ) in T, (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ u z) stdComplexLineReal) ((fderiv ℝ u z) stdComplexLineImag)) + ∫ (z : ℝ × ℝ) in T, ω.hamiltonianCurvature Ks Kt z (u z)

Shrinking to where the datum lives. Let the perturbation data be C¹ over an open set P of the domain, let u be C¹ on P, and let T ⊆ D ⊆ P with D compact. If K_s and K_t vanish near every point of D \ T, then the Floer energy minus the symplectic area plus the integrated curvature is the same over D as over T.

theorem TauCeti.SymplecticForm.setLIntegral_norm_sq_add_norm_sq_perturbedFDeriv_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {U : Set (ℝ × ℝ)} (hU : MeasurableSet U) {J : ℝ × ℝ → AlmostComplexStructure V} {c M : ℝ} (hc : 0 < c) (hJc : ∀ z ∈ U, ∀ (v : V), c * ‖v‖ ^ 2 ≤ (fun (v w : V) => (ω.toBilinForm v) w) v ((J z).toLinearMap v)) (hJM : ∀ z ∈ U, ∀ (v : V), ‖(J z).toLinearMap v‖ ≤ M * ‖v‖) (h : ∀ z ∈ U, IsComplexLinearMap (AlmostComplexStructure.product ℝ) (J z) ↑(ω.perturbedFDeriv Ks Kt u z)) : ∫⁻ (z : ℝ × ℝ) in U, ENNReal.ofReal (‖(ω.perturbedFDeriv Ks Kt u z) stdComplexLineReal‖ ^ 2 + ‖(ω.perturbedFDeriv Ks Kt u z) stdComplexLineImag‖ ^ 2) ≤ ENNReal.ofReal ((1 + M ^ 2) / c) * ∫⁻ (z : ℝ × ℝ) in U, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z)

The energy controls the perturbed derivative in L². Let u solve the Floer equation on a measurable set U for domain-dependent almost complex structures J z satisfying c ‖v‖² ≤ ω(v, J z v) and ‖J z v‖ ≤ M ‖v‖ on U, with 0 < c. Then the integral over U of ‖∂_s u - X_{K_s}‖² + ‖∂_t u - X_{K_t}‖² is at most (1 + M²) / c times the energy over U. No measurability of the integrands is assumed.

noncomputable def TauCeti.SymplecticForm.stripEnergyMeasure {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) : MeasureTheory.Measure ℝ

The strip energy measure of a map u of the strip ℝ × [0, 1]: the measure on ℝ giving each set A of s-values the Floer energy of u over A × [0, 1] for the perturbation data Ks, Kt (TauCeti.SymplecticForm.stripEnergyMeasure_apply). It is the pushforward to the s-axis of the energy density on the strip.

theorem TauCeti.SymplecticForm.stripEnergyMeasure_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) : ω.stripEnergyMeasure Ks Kt u = MeasureTheory.Measure.map Prod.fst ((MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Icc 0 1)).withDensity fun (z : ℝ × ℝ) => ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z))

The strip energy measure is the pushforward to the s-axis of the measure with density the positive part of the energy density on the strip.

theorem TauCeti.SymplecticForm.stripEnergyMeasure_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) {A : Set ℝ} (hA : MeasurableSet A) : (ω.stripEnergyMeasure Ks Kt u) A = ∫⁻ (z : ℝ × ℝ) in A ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z)

The strip energy measure of a measurable set A is the energy over A × [0, 1].

theorem TauCeti.SymplecticForm.stripEnergyMeasure_univ {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) : (ω.stripEnergyMeasure Ks Kt u) Set.univ = ∫⁻ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z)

The total mass of the strip energy measure is the energy over the strip.

theorem TauCeti.SymplecticForm.isFiniteMeasure_stripEnergyMeasure {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : SymplecticForm V} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} (hfin : ∫⁻ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z) ≠ ⊤) : MeasureTheory.IsFiniteMeasure (ω.stripEnergyMeasure Ks Kt u)

The strip energy measure of a map of finite energy is finite.

theorem TauCeti.SymplecticForm.stripEnergyMeasure_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : SymplecticForm V} {Ks Kt : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} : ω.stripEnergyMeasure Ks Kt u = 0 ↔ ∫⁻ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity Ks Kt u z) = 0

The strip energy measure vanishes exactly when the energy over the strip does.

theorem TauCeti.SymplecticForm.stripEnergyMeasure_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (Ks Kt : ℝ × ℝ → V → ℝ) (u : ℝ × ℝ → V) (c : ℝ) : (ω.stripEnergyMeasure (fun (w : ℝ × ℝ) => Ks (w + (c, 0))) (fun (w : ℝ × ℝ) => Kt (w + (c, 0))) fun (w : ℝ × ℝ) => u (w + (c, 0))) = MeasureTheory.Measure.map (fun (x : ℝ) => x - c) (ω.stripEnergyMeasure Ks Kt u)

Translations translate the strip energy measure. Translating a map and its perturbation data by (c, 0) translates its strip energy measure by -c.

theorem TauCeti.SymplecticForm.stripEnergyMeasure_cylindrical_comp_add_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (u : ℝ × ℝ → V) (H : ℝ → V → ℝ) (c : ℝ) : (ω.stripEnergyMeasure (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) fun (w : ℝ × ℝ) => u (w + (c, 0))) = MeasureTheory.Measure.map (fun (x : ℝ) => x - c) (ω.stripEnergyMeasure (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) u)

For the cylindrical perturbation K = H_t dt, translating the map by (c, 0) translates its strip energy measure by -c.