The curvature of perturbation data on the cylindrical ends of the pair of pants

Integrals of Floer data over the thrice-punctured sphere S = ℂ ∖ {0, 1} are computed end by end, in the cylinder coordinates (s, t) of each end, through the end charts TauCeti.Floer.endChart. This file reduces curvature bounds for perturbation data supported on the ends to one-variable integrals along the ends. The target is a manifold M with a smooth two-form ω, as in TauCeti.Geometry.Symplectic.Floer.Manifold; a symplectic vector space is the case of the constant form TauCeti.SymplecticForm.constSmooth, whose curvature is the vector-space curvature (TauCeti.SymplecticForm.hamiltonianCurvature_constSmooth).

• If a perturbation one-form K on ℂ is P(±s) h(t) dt on an end, so is its pullback along the end chart (TauCeti.Floer.perturbationPullback_endChart_of_eq), and its curvature there is ±P'(±s) h(t) (TauCeti.SmoothTwoForm.hamiltonianCurvature_perturbationPullback_endChart_of_eq).
• If K vanishes wherever the signed longitudinal coordinate of every end is at most 1, its curvature vanishes where all of them are less than 1 (TauCeti.SmoothTwoForm.hamiltonianCurvature_eq_zero_of_forall_endCoord_lt), and its integrated curvature along any map is at most the sum of its integrals over the images of the end strips (TauCeti.SmoothTwoForm.lintegral_enorm_hamiltonianCurvature_le_sum_endStrip).
• If, along a map u, the curvature of the pullback of K along each end chart is integrable over the strip of its end, the curvature of K along u is integrable over S (TauCeti.SmoothTwoForm.integrableOn_hamiltonianCurvature_of_forall_integrableOn_endStrip).
• If the curvature of the pullback of K along the end chart is at most f(s) on the strip of an end, the integrated curvature over the image of the strip is at most ∫ f(s) ds (TauCeti.SmoothTwoForm.setLIntegral_image_endChart_enorm_hamiltonianCurvature_le_lintegral). In particular, where K is P(±s) h(t) dt with |h| ≤ B, it is at most B ∫ |P'(±s)| ds (TauCeti.SmoothTwoForm.setLIntegral_image_endChart_enorm_hamiltonianCurvature_le).
• An integral over the strip of an end of a function of s alone is an integral over the half-line ±s > 1/2 (TauCeti.Floer.setLIntegral_endStrip_fst).

References

• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, Chapter 4, on cylindrical end coordinates of punctured Riemann surfaces, and Section 8.1, on the curvature of Hamiltonian perturbations.

theorem TauCeti.Floer.setLIntegral_endStrip_fst (q : ThricePuncturedSphere.Puncture) {f : ℝ → ENNReal} (hf : Measurable f) : ∫⁻ (z : ℝ × ℝ) in endStrip q, f z.1 = ∫⁻ (s : ℝ) in {s : ℝ | 1 / 2 < q.endSign * s}, f s

An integral over the strip of the end q of a function of the longitudinal coordinate alone is its integral over the half-line ±s > 1/2, since the angular coordinate ranges over an interval of length one.

theorem TauCeti.Floer.perturbationPullback_endChart_of_eq {X : Type u_1} {K : ℂ → X → ℂ →L[ℝ] ℝ} {q : ThricePuncturedSphere.Puncture} {P : ℝ → ℝ} {h : ℝ → X → ℝ} (hK : ∀ (z : ℂ), 0 < q.endSign * z.re → ∀ (x : X) (v : ℂ), (K (q.cylindricalEndLift z) x) (deriv q.cylindricalEndLift z * v) = v.im * (P (q.endSign * z.re) * h z.im x)) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) (v : ℝ × ℝ) (x : X) : perturbationPullback (endChart q) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) v z x = v.2 * (P (q.endSign * z.1) * h z.2 x)

Data of the form P(±s) h(t) dt on an end. If the datum K, pulled back along the end lift of q, is P(±s) h(t) dt on the part ±s > 0 of the end, then so is its pullback along the end chart: it sends a tangent vector v = (v₁, v₂) of the cylinder to v₂ · P(±s) h(t).

The curvature of data supported on the ends

theorem TauCeti.SmoothTwoForm.hamiltonianCurvature_eq_zero_of_forall_endCoord_lt {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) (hK : ∀ (w : ℂ), (∀ (q : ThricePuncturedSphere.Puncture), q.endSign * (q.endCoord w).re ≤ 1) → ∀ (x : M), K w x = 0) {z : ℝ × ℝ} (hz : z ∈ Floer.thricePuncturedSphereReal) (h : ∀ (q : ThricePuncturedSphere.Puncture), q.endSign * (q.endCoord (Complex.equivRealProdCLM.symm z)).re < 1) (x : M) : ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z x = 0

The curvature of a datum supported on the ends. Let K be a perturbation one-form on ℂ that vanishes wherever the signed longitudinal coordinate of every end is at most 1. At a point of S where the signed longitudinal coordinate of every end is less than 1, K vanishes nearby, and so does its curvature.

theorem TauCeti.SmoothTwoForm.lintegral_enorm_hamiltonianCurvature_le_sum_endStrip {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) (hK : ∀ (w : ℂ), (∀ (q : ThricePuncturedSphere.Puncture), q.endSign * (q.endCoord w).re ≤ 1) → ∀ (x : M), K w x = 0) (u : ℝ × ℝ → M) : ∫⁻ (z : ℝ × ℝ), ‖ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z (u z)‖ₑ ≤ ∑ q : ThricePuncturedSphere.Puncture, ∫⁻ (z : ℝ × ℝ) in Floer.endChart q '' Floer.endStrip q, ‖ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z (u z)‖ₑ

The integrated curvature of a datum supported on the ends. Let K be a perturbation one-form on ℂ that vanishes wherever the signed longitudinal coordinate of every end is at most 1. Then for every map u into the target, the integral of |R_K(z, u(z))| over the plane is at most the sum over the three ends of its integrals over the images of their strips.

theorem TauCeti.SmoothTwoForm.integrableOn_hamiltonianCurvature_of_forall_integrableOn_endStrip {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) (hK : ∀ (w : ℂ), (∀ (q : ThricePuncturedSphere.Puncture), q.endSign * (q.endCoord w).re ≤ 1) → ∀ (x : M), K w x = 0) (hKs : ∀ (w : ThricePuncturedSphere) (x : M), (MDiffAt fun (p : ℂ × M) => K p.1 p.2) (↑w, x)) {u : ℝ × ℝ → M} (hR : ∀ (q : ThricePuncturedSphere.Puncture), MeasureTheory.IntegrableOn (fun (z : ℝ × ℝ) => ω.hamiltonianCurvature (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineReal) (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineImag) z (u (Floer.endChart q z))) (Floer.endStrip q) MeasureTheory.volume) : MeasureTheory.IntegrableOn (fun (z : ℝ × ℝ) => ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z (u z)) Floer.thricePuncturedSphereReal MeasureTheory.volume

Integrability of the curvature of a datum supported on the ends. Let K be a perturbation one-form on ℂ that vanishes wherever the signed longitudinal coordinate of every end is at most 1, and which is differentiable on S × M. If, along a map u, the curvature of the pullback of K along the end chart of each end is integrable over the strip of that end, then the curvature of K along u is integrable over S.

theorem TauCeti.SmoothTwoForm.hamiltonianCurvature_perturbationPullback_endChart_of_eq {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) {q : ThricePuncturedSphere.Puncture} {P : ℝ → ℝ} {h : ℝ → M → ℝ} (hK : ∀ (z : ℂ), 0 < q.endSign * z.re → ∀ (x : M) (v : ℂ), (K (q.cylindricalEndLift z) x) (deriv q.cylindricalEndLift z * v) = v.im * (P (q.endSign * z.re) * h z.im x)) {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) {x : M} (hP : DifferentiableAt ℝ P (q.endSign * z.1)) (hhx : DifferentiableAt ℝ (fun (t : ℝ) => h t x) z.2) : ω.hamiltonianCurvature (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineReal) (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineImag) z x = q.endSign * deriv P (q.endSign * z.1) * h z.2 x

The curvature of data of the form P(±s) h(t) dt on an end. If the datum K, pulled back along the end lift of q, is P(±s) h(t) dt on the part ±s > 0 of the end, then the curvature of its pullback along the end chart is ±P'(±s) h(t) there.

theorem TauCeti.SmoothTwoForm.setLIntegral_image_endChart_enorm_hamiltonianCurvature_le_lintegral {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) {q : ThricePuncturedSphere.Puncture} (hKd : ∀ (w : ℂ), w ≠ 0 ∧ w ≠ 1 → ∀ (x : M) (v : ℂ), DifferentiableAt ℝ (fun (w' : ℂ) => (K w' x) v) w) (hKx : ∀ (w : ℂ), w ≠ 0 ∧ w ≠ 1 → ∀ (x : M) (v : ℂ), (MDiffAt fun (y : M) => (K w y) v) x) {f : ℝ → ENNReal} (hf : Measurable f) (hR : ∀ z ∈ Floer.endStrip q, ∀ (x : M), ‖ω.hamiltonianCurvature (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineReal) (Floer.perturbationPullback (Floer.endChart q) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineImag) z x‖ₑ ≤ f z.1) (u : ℝ × ℝ → M) : ∫⁻ (z : ℝ × ℝ) in Floer.endChart q '' Floer.endStrip q, ‖ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z (u z)‖ₑ ≤ ∫⁻ (s : ℝ), f s

The integrated curvature over an end strip, from a pointwise bound. Let K be a perturbation one-form on ℂ which is differentiable on S separately in the domain point and in the target point. If the curvature of its pullback along the end chart of q is at most f(s) at every point (s, t) of the strip of q, for a measurable f, then for every map u into the target, the integral of |R_K(z, u(z))| over the image of the strip of q is at most ∫ f(s) ds.

theorem TauCeti.SmoothTwoForm.setLIntegral_image_endChart_enorm_hamiltonianCurvature_le {E : Type u_1} {G : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] [IsManifold I (↑⊤) M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (ω : SmoothTwoForm I M) {q : ThricePuncturedSphere.Puncture} {P : ℝ → ℝ} {h : ℝ → M → ℝ} (hKd : ∀ (w : ℂ), w ≠ 0 ∧ w ≠ 1 → ∀ (x : M) (v : ℂ), DifferentiableAt ℝ (fun (w' : ℂ) => (K w' x) v) w) (hKx : ∀ (w : ℂ), w ≠ 0 ∧ w ≠ 1 → ∀ (x : M) (v : ℂ), (MDiffAt fun (y : M) => (K w y) v) x) (hK : ∀ (z : ℂ), 0 < q.endSign * z.re → ∀ (x : M) (v : ℂ), (K (q.cylindricalEndLift z) x) (deriv q.cylindricalEndLift z * v) = v.im * (P (q.endSign * z.re) * h z.im x)) (hP : Differentiable ℝ P) (hh : ∀ (x : M), Differentiable ℝ fun (t : ℝ) => h t x) {B : ℝ} (hB : ∀ (t : ℝ) (x : M), |h t x| ≤ B) (u : ℝ × ℝ → M) : ∫⁻ (z : ℝ × ℝ) in Floer.endChart q '' Floer.endStrip q, ‖ω.hamiltonianCurvature (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) z (u z)‖ₑ ≤ (∫⁻ (s : ℝ), ‖deriv P (q.endSign * s)‖ₑ) * ENNReal.ofReal B

The integrated curvature over an end strip. Let K be a perturbation one-form on ℂ which is differentiable on S separately in the domain point and in the target point, and which, pulled back along the end lift of q, is P(±s) h(t) dt on the part ±s > 0 of the end, with |h| ≤ B. Then for every map u into the target, the integral of |R_K(z, u(z))| over the image of the strip of q is at most B times the total variation ∫ |P'(±s)| ds of the profile P.