The Hamiltonian action and the energy of cylindrical Floer solutions

Let (V, ω) be a symplectic vector space and H : ℝ → V → ℝ a time-dependent Hamiltonian. For a loop x : [0, 1] → V with x 1 = x 0, the symplectic area of the loop is a(x) = ½ ∫₀¹ ω(x(t), x'(t)) dt (TauCeti.SymplecticForm.loopArea, in TauCeti.Geometry.Symplectic.Area.Basic). It is the symplectic area ∫ D^* ω of the cone D(r, t) = r x(t) bounding the loop (SymplecticForm.integral_symplecticForm_fderiv_smul_eq_loopArea). The Hamiltonian action of the loop capped by this disc is

A_H(x) = a(x) + ∫₀¹ H(t, x(t)) dt

(TauCeti.SymplecticForm.hamiltonianAction), the convention A_H(x, D) = ∫ D^* ω + ∫ H dt of capped Floer theory with positive ends as inputs.

On a region of the domain where the Hamiltonian perturbation is cylindrical, K = H_t dt, such as a strip-like end or a neck of a punctured Floer domain, the curvature of K vanishes and the boundary terms of the Floer energy identity combine into actions. For a map u on [a, b] × [0, 1] whose bottom and top sides agree, so that each t ↦ u(s, t) is a loop:

• the symplectic area of u is a(u(b, ·)) - a(u(a, ·)) (SymplecticForm.integral_symplecticForm_fderiv_eq_loopArea_sub), by Green's formula for the primitive λₓ(v) = ½ ω(x, v) (SymplecticForm.integral_fderiv_apply_prod_Icc);
• the Floer energy of u is A_H(u(b, ·)) - A_H(u(a, ·)) (SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub), by the energy identity TauCeti.SymplecticForm.integral_floerEnergyDensity.

For a solution of the Floer equation ∂_s u + J (∂_t u - X_{H_t}(u)) = 0 with J tamed by ω, the energy density is nonnegative, so the action increases along the cylinder (SymplecticForm.hamiltonianAction_le_hamiltonianAction), and the energy of a Floer solution on the whole cylinder ℝ × [0, 1] is the difference of the limiting actions at its two ends (SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction), by exhausting the cylinder with rectangles (TauCeti.tendsto_setLIntegral_Icc_neg_prod). These are the end and neck terms of the energy identity E = A₁ + A₂ - A₀ + ω(A) - ∫ R_K for pairs of pants.

For an s-dependent family of Hamiltonians H_{(s, t)}, the perturbation K = H_{(s, t)} dt of a continuation cylinder has curvature ∂_s H, and the energy of u over [a, b] × [0, 1] is

E = A_{H(b, ·)}(u(b, ·)) - A_{H(a, ·)}(u(a, ·)) - ∫∫ (∂_s H)(s, t, u(s, t))

(SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral). Over the whole cylinder, for a solution with tame J whose loop actions converge at the two ends, the energy is the difference of the limiting actions minus the integral of ∂_s H along u (SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction_sub_integral). The cylindrical statements above are the special case of an s-independent family.

For a solution with tame J, the action therefore drops by at most the integral of -∂_s H along u (SymplecticForm.hamiltonianAction_le_hamiltonianAction_sub_integral), and it does not drop for a monotone homotopy (SymplecticForm.hamiltonianAction_le_hamiltonianAction_of_monotone).

A 1-periodic orbit x of X_{H_t} is a critical point of the action, so for a loop γ the difference A_H(γ) - A_H(x) has no term linear in ξ = γ - x: it is ∫₀¹ (½ ω(ξ, ξ') + H_t(γ) - H_t(x) - dH_t(x) ξ) dt (SymplecticForm.hamiltonianAction_sub_hamiltonianAction_eq_integral).

Main definitions

• TauCeti.SymplecticForm.hamiltonianAction: the Hamiltonian action of a loop.

Main results

• SymplecticForm.hamiltonianAction_add_const: adding a function c of time to the Hamiltonian adds ∫₀¹ c to the action of every loop.
• integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral_hamiltonianCurvature: the energy of a map over [a, b] × [0, 1], for a perturbation which is H_a dt and H_b dt on the two boundary circles, is the change of action minus the integrated curvature.
• SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub: the energy of a map over [a, b] × [0, 1] for a cylindrical perturbation is the change of action.
• SymplecticForm.hamiltonianAction_le_hamiltonianAction: the action increases along Floer solutions.
• SymplecticForm.monotoneOn_hamiltonianAction_of_floer: the action is monotone in s along a Floer solution on an open interval of s-values.
• SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction: the energy of a Floer solution on the whole cylinder is the difference of its limiting actions.
• SymplecticForm.tendsto_hamiltonianAction: the action is continuous for uniform C¹ convergence of loops.
• SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral: the energy identity of a continuation cylinder over a rectangle.
• SymplecticForm.hamiltonianAction_le_hamiltonianAction_sub_integral: the action estimate along a continuation cylinder over a rectangle.
• SymplecticForm.hamiltonianAction_le_hamiltonianAction_of_monotone: the action does not drop along a continuation cylinder of a monotone homotopy.
• SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction_sub_integral: the energy identity of a continuation cylinder over the whole cylinder.
• SymplecticForm.hamiltonianAction_sub_hamiltonianAction_eq_integral: the expansion of the action at an orbit, without linear term.

References

• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, Section 8.1 and the chapter on Floer homology, on the action functional and the energy identity.
• D. Salamon, Lectures on Floer homology, in Symplectic geometry and topology, IAS/Park City Math. Ser. 7 (1999), Lectures 1 and 3.

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

The Hamiltonian action A_H(x) = ½ ∫₀¹ ω(x, x') dt + ∫₀¹ H(t, x(t)) dt of a loop x, for a time-dependent Hamiltonian H. It is the action ∫ D^* ω + ∫ H dt of the loop capped by the cone D(r, t) = r x(t), with the sign convention in which the action increases along Floer solutions, so that positive ends are inputs.

theorem TauCeti.SymplecticForm.hamiltonianAction_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) (H : ℝ → V → ℝ) (x : ℝ → V) : ω.hamiltonianAction H x = ω.loopArea x + ∫ (t : ℝ) in 0..1, H t (x t)

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianAction_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) (H : ℝ → V → ℝ) (v : V) : (ω.hamiltonianAction H fun (x : ℝ) => v) = ∫ (t : ℝ) in 0..1, H t v

The action of a constant loop is the time average of the Hamiltonian at that point.

theorem TauCeti.SymplecticForm.hamiltonianAction_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (ω : SymplecticForm V) {H : ℝ → V → ℝ} {c : ℝ → ℝ} {x : ℝ → V} (hH : IntervalIntegrable (fun (t : ℝ) => H t (x t)) MeasureTheory.volume 0 1) (hc : IntervalIntegrable c MeasureTheory.volume 0 1) : ω.hamiltonianAction (fun (t : ℝ) (y : V) => H t y + c t) x = ω.hamiltonianAction H x + ∫ (t : ℝ) in 0..1, c t

Normalizing a Hamiltonian shifts the action. Adding a function c of time to the Hamiltonian adds its time average ∫₀¹ c to the action of every loop.

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

Reversing time negates the action. If the loop x and the Hamiltonian H are 1-periodic, the reversed loop t ↦ x(-t) has, for the reversed Hamiltonian (t, y) ↦ -H(-t, y), the opposite action.

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral_hamiltonianCurvature {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) {Ks Kt : ℝ × ℝ → V → ℝ} {Ha Hb : ℝ → V → ℝ} (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hKs : ContDiffOn ℝ 1 (Function.uncurry Ks) (U ×ˢ Set.univ)) (hKt : ContDiffOn ℝ 1 (Function.uncurry Kt) (U ×ˢ Set.univ)) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) (hKper : ∀ s ∈ Set.Icc a b, Ks (s, 1) = Ks (s, 0)) (hKa : ∀ t ∈ Set.Icc 0 1, Kt (a, t) = Ha t) (hKb : ∀ t ∈ Set.Icc 0 1, Kt (b, t) = Hb t) : ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, ω.floerEnergyDensity Ks Kt u z = ((ω.hamiltonianAction Hb fun (t : ℝ) => u (b, t)) - ω.hamiltonianAction Ha fun (t : ℝ) => u (a, t)) - ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, ω.hamiltonianCurvature Ks Kt z (u z)

The energy identity between two loops. Let u be C² and the perturbation components K_s and K_t be C¹ on an open neighbourhood U of [a, b] × [0, 1], with u(s, 1) = u(s, 0) and K_s(s, 1) = K_s(s, 0) for s ∈ [a, b], so that the bottom and top sides of the rectangle are glued into a cylinder. If on the two boundary circles the dt-component of K is a time-dependent Hamiltonian, K_t(a, t) = H_a(t) and K_t(b, t) = H_b(t), then the Floer energy of u over the rectangle is the change of action minus the integrated curvature:

∫ E = A_{H_b}(u(b, ·)) - A_{H_a}(u(a, ·)) - ∫ R_K(u).

No condition is imposed on K_s along the two boundary circles or on K in the interior.

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) : ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) H u z = ((ω.hamiltonianAction (fun (t : ℝ) => H (b, t)) fun (t : ℝ) => u (b, t)) - ω.hamiltonianAction (fun (t : ℝ) => H (a, t)) fun (t : ℝ) => u (a, t)) - ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, (fderiv ℝ (fun (w : ℝ × ℝ) => H w (u z)) z) stdComplexLineReal

The energy identity of a continuation cylinder. Let H_{(s, t)} be a C¹ family of Hamiltonians and let u be C² on an open neighbourhood U of [a, b] × [0, 1], with u(s, 1) = u(s, 0) for s ∈ [a, b]. For the perturbation K = H_{(s, t)} dt, the Floer energy of u over the rectangle is the action of the loop at s = b for H(b, ·), minus the action of the loop at s = a for H(a, ·), minus the integral of ∂_s H along u.

theorem TauCeti.SymplecticForm.hamiltonianAction_le_hamiltonianAction_sub_integral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} (hJ : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) (hfloer : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, (fderiv ℝ u z) stdComplexLineReal + (J z).toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (H z) (u z)) = 0) : (ω.hamiltonianAction (fun (t : ℝ) => H (a, t)) fun (t : ℝ) => u (a, t)) ≤ (ω.hamiltonianAction (fun (t : ℝ) => H (b, t)) fun (t : ℝ) => u (b, t)) - ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, (fderiv ℝ (fun (w : ℝ × ℝ) => H w (u z)) z) stdComplexLineReal

The action estimate along a continuation cylinder. Under the hypotheses of TauCeti.SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub_sub_integral, if u solves the Floer equation ∂_s u + J_z (∂_t u - X_{H_z}(u)) = 0 on the rectangle for almost complex structures J_z tamed by ω, then the action of the loop at s = a is at most the action of the loop at s = b minus the integral of ∂_s H along u.

theorem TauCeti.SymplecticForm.hamiltonianAction_le_hamiltonianAction_of_monotone {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} (hJ : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hmono : ∀ (t : ℝ) (x : V), Monotone fun (s : ℝ) => H (s, t) x) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) (hfloer : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, (fderiv ℝ u z) stdComplexLineReal + (J z).toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (H z) (u z)) = 0) : (ω.hamiltonianAction (fun (t : ℝ) => H (a, t)) fun (t : ℝ) => u (a, t)) ≤ ω.hamiltonianAction (fun (t : ℝ) => H (b, t)) fun (t : ℝ) => u (b, t)

The action increases along continuation cylinders of monotone homotopies. Under the hypotheses of TauCeti.SymplecticForm.hamiltonianAction_le_hamiltonianAction_sub_integral, if every s ↦ H_{(s, t)}(x) is monotone, then the action of the loop at s = a for H(a, ·) is at most that of the loop at s = b for H(b, ·).

theorem TauCeti.SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction_sub_integral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ × ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} (hJ : ∀ z ∈ Set.univ ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hRU : Set.univ ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ (s : ℝ), u (s, 1) = u (s, 0)) (hfloer : ∀ z ∈ Set.univ ×ˢ Set.Icc 0 1, (fderiv ℝ u z) stdComplexLineReal + (J z).toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (H z) (u z)) = 0) (hint : MeasureTheory.IntegrableOn (fun (z : ℝ × ℝ) => (fderiv ℝ (fun (w : ℝ × ℝ) => H w (u z)) z) stdComplexLineReal) (Set.univ ×ˢ Set.Icc 0 1) MeasureTheory.volume) {A₁ A₂ : ℝ} (hbot : Filter.Tendsto (fun (s : ℝ) => ω.hamiltonianAction (fun (t : ℝ) => H (s, t)) fun (t : ℝ) => u (s, t)) Filter.atBot (nhds A₁)) (htop : Filter.Tendsto (fun (s : ℝ) => ω.hamiltonianAction (fun (t : ℝ) => H (s, t)) fun (t : ℝ) => u (s, t)) Filter.atTop (nhds A₂)) : ∫⁻ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) H u z) = ENNReal.ofReal (A₂ - A₁ - ∫ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, (fderiv ℝ (fun (w : ℝ × ℝ) => H w (u z)) z) stdComplexLineReal)

The energy of a continuation cylinder. Let H_{(s, t)} be a C¹ family of Hamiltonians and let u be C² on an open neighbourhood U of ℝ × [0, 1], with u(s, 1) = u(s, 0) for all s, solving the Floer equation ∂_s u + J_z (∂_t u - X_{H_z}(u)) = 0 there for almost complex structures J_z tamed by ω. Suppose that ∂_s H is integrable along u and that the actions A_{H(s, ·)}(u(s, ·)) tend to A₁ as s → -∞ and to A₂ as s → ∞. Then the energy of u is A₂ - A₁ minus the integral of ∂_s H along u.

theorem TauCeti.SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) : ∫ (z : ℝ × ℝ) in Set.Icc a b ×ˢ Set.Icc 0 1, ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) u z = (ω.hamiltonianAction H fun (t : ℝ) => u (b, t)) - ω.hamiltonianAction H fun (t : ℝ) => u (a, t)

The energy identity for a cylindrical perturbation. Let H be a C¹ time-dependent Hamiltonian and let u be C² on an open neighbourhood U of [a, b] × [0, 1], with u(s, 1) = u(s, 0) for s ∈ [a, b]. For the cylindrical perturbation K = H_t dt, the Floer energy of u over the rectangle is the action of the loop at s = b minus the action of the loop at s = a.

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

The Floer energy density of a solution of the Floer equation ∂_s u + J (∂_t u - X_{H_t}(u)) = 0 for the cylindrical perturbation K = H_t dt is nonnegative when J is tamed by ω.

theorem TauCeti.SymplecticForm.hamiltonianAction_le_hamiltonianAction {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} {a b : ℝ} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} (hJ : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hab : a ≤ b) (hRU : Set.Icc a b ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ s ∈ Set.Icc a b, u (s, 1) = u (s, 0)) (hfloer : ∀ z ∈ Set.Icc a b ×ˢ Set.Icc 0 1, (fderiv ℝ u z) stdComplexLineReal + (J z).toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (H z.2) (u z)) = 0) : (ω.hamiltonianAction H fun (t : ℝ) => u (a, t)) ≤ ω.hamiltonianAction H fun (t : ℝ) => u (b, t)

The action increases along Floer solutions. Under the hypotheses of TauCeti.SymplecticForm.integral_floerEnergyDensity_eq_hamiltonianAction_sub, if u solves the Floer equation ∂_s u + J (∂_t u - X_{H_t}(u)) = 0 on the rectangle for almost complex structures J z tamed by ω, which may depend on the domain point, then the action of the loop at s = a is at most that of the loop at s = b.

theorem TauCeti.SymplecticForm.monotoneOn_hamiltonianAction_of_floer {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ → V → ℝ} {u : ℝ × ℝ → V} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} {S : Set ℝ} (hS : IsOpen S) [S.OrdConnected] (hH : ContDiff ℝ 1 (Function.uncurry H)) (hu : ContDiffOn ℝ 2 u (S ×ˢ Set.univ)) (hper : ∀ s ∈ S, Function.Periodic (fun (t : ℝ) => u (s, t)) 1) (hJ : ∀ z ∈ S ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hfloer : ∀ z ∈ S ×ˢ Set.Icc 0 1, IsComplexLinearMap (AlmostComplexStructure.product ℝ) (J z) ↑(ω.perturbedFDeriv (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) u z)) : MonotoneOn (fun (s : ℝ) => ω.hamiltonianAction H fun (t : ℝ) => u (s, t)) S

The action increases along a Floer solution. Let S be an open interval of s-values, for instance a half-line s > a or s < a, and let u be a C² solution of the Floer equation on S × [0, 1] with 1-periodic loops and tame almost complex structures. Then the action A_H(u(s, ·)) of the loop at s is monotone in s ∈ S.

theorem TauCeti.SymplecticForm.lintegral_floerEnergyDensity_eq_of_tendsto_hamiltonianAction {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ → V → ℝ} {u : ℝ × ℝ → V} {U : Set (ℝ × ℝ)} (ω : SymplecticForm V) {J : ℝ × ℝ → AlmostComplexStructure V} (hJ : ∀ z ∈ Set.univ ×ˢ Set.Icc 0 1, ω.Tames (J z)) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hRU : Set.univ ×ˢ Set.Icc 0 1 ⊆ U) (hper : ∀ (s : ℝ), u (s, 1) = u (s, 0)) (hfloer : ∀ z ∈ Set.univ ×ˢ Set.Icc 0 1, (fderiv ℝ u z) stdComplexLineReal + (J z).toLinearMap ((fderiv ℝ u z) stdComplexLineImag - ω.hamiltonianVectorField (H z.2) (u z)) = 0) {A₁ A₂ : ℝ} (hbot : Filter.Tendsto (fun (s : ℝ) => ω.hamiltonianAction H fun (t : ℝ) => u (s, t)) Filter.atBot (nhds A₁)) (htop : Filter.Tendsto (fun (s : ℝ) => ω.hamiltonianAction H fun (t : ℝ) => u (s, t)) Filter.atTop (nhds A₂)) : ∫⁻ (z : ℝ × ℝ) in Set.univ ×ˢ Set.Icc 0 1, ENNReal.ofReal (ω.floerEnergyDensity (fun (x : ℝ × ℝ) (x_1 : V) => 0) (fun (w : ℝ × ℝ) => H w.2) u z) = ENNReal.ofReal (A₂ - A₁)

The energy of a Floer cylinder. Let H be a C¹ time-dependent Hamiltonian and let u be C² on an open neighbourhood U of ℝ × [0, 1], with u(s, 1) = u(s, 0) for all s, solving the Floer equation ∂_s u + J_z (∂_t u - X_{H_t}(u)) = 0 there for almost complex structures J_z tamed by ω, which may depend on the domain point. If the actions of the loops t ↦ u(s, t) tend to A₁ as s → -∞ and to A₂ as s → ∞, then the energy of u is A₂ - A₁.

theorem TauCeti.SymplecticForm.hamiltonianAction_sub_hamiltonianAction_eq_integral {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {H : ℝ → V → ℝ} {x : ℝ → V} (ω : SymplecticForm V) (hH : ContDiff ℝ 1 (Function.uncurry H)) (hx : ∀ (t : ℝ), HasDerivAt x (ω.hamiltonianVectorField (H t) (x t)) t) (hx1 : x 1 = x 0) {γ γ' : ℝ → V} (hγ' : Continuous γ') (hγ : ∀ (t : ℝ), HasDerivAt γ (γ' t) t) (hγ1 : γ 1 = γ 0) : ω.hamiltonianAction H γ - ω.hamiltonianAction H x = ∫ (t : ℝ) in 0..1, 1 / 2 * (fun (v w : V) => (ω.toBilinForm v) w) (γ t - x t) (γ' t - ω.hamiltonianVectorField (H t) (x t)) + (H t (γ t) - H t (x t) - (fderiv ℝ (H t) (x t)) (γ t - x t))

The action near a critical loop. Let x be an orbit of the Hamiltonian vector field of a C¹ Hamiltonian H with x 1 = x 0, and let γ be a loop with continuous derivative γ' and γ 1 = γ 0. Since x is a critical point of the action, the action difference has no term linear in ξ = γ - x: A_H(γ) - A_H(x) = ∫₀¹ (½ ω(ξ, ξ') + H_t(γ) - H_t(x) - dH_t(x) ξ) dt.

theorem TauCeti.SymplecticForm.tendsto_hamiltonianAction {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ι : Type u_2} {l : Filter ι} [l.IsCountablyGenerated] {H : ℝ → V → ℝ} {x : ι → ℝ → V} {x₀ : ℝ → V} (ω : SymplecticForm V) (hH : Continuous (Function.uncurry H)) (hx : ∀ᶠ (i : ι) in l, ContinuousOn (x i) (Set.Icc 0 1)) (hdx : ∀ᶠ (i : ι) in l, ContinuousOn (deriv (x i)) (Set.Icc 0 1)) (hlim : TendstoUniformlyOn x x₀ l (Set.Icc 0 1)) (hdlim : TendstoUniformlyOn (fun (i : ι) => deriv (x i)) (deriv x₀) l (Set.Icc 0 1)) : Filter.Tendsto (fun (i : ι) => ω.hamiltonianAction H (x i)) l (nhds (ω.hamiltonianAction H x₀))

The action is continuous for uniform C¹ convergence of loops. Let H be a continuous time-dependent Hamiltonian. If the loops x i and their derivatives are eventually continuous on [0, 1] and converge uniformly there to x₀ and to the derivative of x₀, then the actions of the x i converge to the action of x₀.