The pair of pants and its end charts in real coordinates

Integrals over the pair of pants S = ℂ ∖ {0, 1} are computed in the real coordinates ℝ × ℝ ≃ ℂ, where the coordinate formulas of TauCeti.Geometry.Symplectic.Floer.Energy and TauCeti.Geometry.Symplectic.Floer.Pullback live. This file transports S (TauCeti.Floer.thricePuncturedSphereReal), the pair-of-pants perturbation and the cylindrical end lifts of S to these coordinates. The end chart φ_q (TauCeti.Floer.endChart q) is the end lift of the end q in real coordinates, a holomorphic change of coordinates from the cylinder of the end to S. On the strip ±s > 1/2, t ∈ [-1/2, 1/2) (TauCeti.Floer.endStrip q) it is injective, and it preserves orientation, so the change of variables formula applies on the images of the three strips; these images are disjoint and measurable. Along the end chart, the pair-of-pants perturbation pulls back to its components in the end coordinates.

On the input ends 0, 1 the end coordinate s tends to +∞, on the output end ∞ to -∞. The positive end chart φ'_q(s, t) = φ_q(±s, ±t) (TauCeti.Floer.positiveEndChart q), with the sign of the end, reads every end as a positive end; it is again holomorphic, orientation preserving and 1-periodic in t. Where a perturbation is H_q(t) dt on the end q, it pulls back along φ'_q to H'_q(t) dt for the Hamiltonian H'_q(t, x) = ±H_q(±t, x) (TauCeti.Floer.positiveEndHamiltonian), so that results about positive Floer half-cylinders apply to all three ends.

Main definitions

• TauCeti.Floer.thricePuncturedSphereReal: the pair of pants S in the real coordinates ℝ × ℝ ≃ ℂ.
• TauCeti.Floer.endChart q: the end lift of q in the real coordinates ℝ × ℝ ≃ ℂ.
• TauCeti.Floer.endStrip q: the part ±s > 1/2, t ∈ [-1/2, 1/2) of the cylinder of the end q.
• TauCeti.Floer.positiveEndChart q: the end chart of q read as a positive end.
• TauCeti.Floer.positiveEndHamiltonian H q: the end Hamiltonian in the positive end chart.

Main results

• TauCeti.Floer.isCompact_preimage_truncation, TauCeti.Floer.preimage_truncation_subset_thricePuncturedSphereReal, TauCeti.Floer.exists_lt_endSign_mul_re_endCoord_of_notMem_truncation: in real coordinates the truncation S_R is compact and lies in S, and every other point of S lies beyond R on some end.
• TauCeti.Floer.setIntegral_thricePuncturedSphereReal_eq_setIntegral_truncation: the integral over S of a function vanishing beyond R on every end is its integral over S_R.
• TauCeti.Floer.contDiffAt_uncurry_pairOfPantsPerturbation: in real coordinates, the components of the perturbation are Cⁿ on S × V for Cⁿ Hamiltonians.
• TauCeti.Floer.contMDiffOn_thricePuncturedSphereReal_prod_univ_of_forall_contMDiffAt: a datum which is C¹ on S × M has C¹ components in the real coordinates of S.
• TauCeti.Floer.endChart_mem_thricePuncturedSphereReal, TauCeti.Floer.re_endCoord_endChart: the end chart sends the part ±s > 0 of the end into S and preserves the longitudinal coordinate.
• TauCeti.Floer.injOn_endChart, TauCeti.Floer.det_fderiv_endChart_nonneg, TauCeti.Floer.det_fderiv_endChart_pos: the end chart is injective on the strip, preserves orientation and is a local diffeomorphism.
• TauCeti.Floer.pairwise_disjoint_image_endChart: the images of the three strips are disjoint.
• TauCeti.Floer.mem_image_endChart: they contain every point of S with signed longitudinal coordinate greater than 1/2 on some end.
• TauCeti.Floer.injOn_endChart_univ_prod_Ico: the end chart is injective on every band of angular width one.
• TauCeti.Floer.image_endChart_prod_Ico: the image of P × [0, 1) under the end chart is the set of points of S whose longitudinal coordinate lies in P, for any set P of positive signed longitudinal coordinates.
• TauCeti.Floer.preimage_truncation_inter_eq_image_endChart: the part ±s > c of the end q in the truncation S_R is the image under the end chart of c < ±s ≤ R, t ∈ [0, 1).
• TauCeti.Floer.perturbationPullback_endChart_eq_cylindricalEndLift: the pullback of a perturbation along the end chart is the perturbation evaluated on the image of a tangent vector under the end lift.
• TauCeti.Floer.perturbationPullback_endChart: the pullback of the pair-of-pants perturbation along the end chart is its component in the end coordinates.
• TauCeti.Floer.isComplexLinearMap_fderiv_endChart: the end chart is holomorphic.
• TauCeti.Floer.perturbationPullback_endChart_stdComplexLineImag_of_le, TauCeti.Floer.perturbationPullback_endChart_stdComplexLineReal_of_le: where a perturbation is H_q(t) dt on the end q, its pullback along the end chart sends ∂_t to H_q(t) and ∂_s to 0.
• TauCeti.Floer.isComplexLinearMap_fderiv_positiveEndChart, TauCeti.Floer.det_fderiv_positiveEndChart_pos, TauCeti.Floer.injOn_positiveEndChart, TauCeti.Floer.positiveEndChart_add_one: the positive end chart is holomorphic, orientation preserving, injective on the band ℝ × (0, 1) and 1-periodic in t.
• TauCeti.Floer.perturbationPullback_positiveEndChart_stdComplexLineReal_of_le, TauCeti.Floer.perturbationPullback_positiveEndChart_stdComplexLineImag_of_le: where a perturbation is H_q(t) dt on the end q, its pullback along the positive end chart is H'_q(t) dt.

References

• D. McDuff and D. Salamon, J-holomorphic curves and symplectic topology, Chapter 4, on the cylindrical end coordinates of a punctured Riemann surface.

def TauCeti.Floer.thricePuncturedSphereReal : Set (ℝ × ℝ)

The pair of pants S = ℂ ∖ {0, 1}, in the real coordinates ℝ × ℝ ≃ ℂ.

@[simp]

theorem TauCeti.Floer.mem_thricePuncturedSphereReal_iff {z : ℝ × ℝ} : z ∈ thricePuncturedSphereReal ↔ Complex.equivRealProdCLM.symm z ≠ 0 ∧ Complex.equivRealProdCLM.symm z ≠ 1

A point lies in S when, as a complex number, it is neither 0 nor 1.

theorem TauCeti.Floer.isOpen_thricePuncturedSphereReal : IsOpen thricePuncturedSphereReal

The pair of pants is open in real coordinates.

theorem TauCeti.Floer.isCompact_preimage_truncation (R : ℝ) : IsCompact (⇑Complex.equivRealProdCLM.symm ⁻¹' ThricePuncturedSphere.truncation R)

The truncation S_R is compact in real coordinates.

theorem TauCeti.Floer.preimage_truncation_subset_thricePuncturedSphereReal (R : ℝ) : ⇑Complex.equivRealProdCLM.symm ⁻¹' ThricePuncturedSphere.truncation R ⊆ thricePuncturedSphereReal

The truncation S_R, in real coordinates, lies in S.

theorem TauCeti.Floer.exists_lt_endSign_mul_re_endCoord_of_notMem_truncation {R : ℝ} {z : ℝ × ℝ} (hz : z ∈ thricePuncturedSphereReal) (hzR : Complex.equivRealProdCLM.symm z ∉ ThricePuncturedSphere.truncation R) : ∃ (q : ThricePuncturedSphere.Puncture), R < q.endSign * (q.endCoord (Complex.equivRealProdCLM.symm z)).re

A point of S outside the truncation S_R lies beyond R on some end.

theorem TauCeti.Floer.setIntegral_thricePuncturedSphereReal_eq_setIntegral_truncation {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ × ℝ → E} {R : ℝ} (hf : ∀ z ∈ thricePuncturedSphereReal, ∀ (q : ThricePuncturedSphere.Puncture), R < q.endSign * (q.endCoord (Complex.equivRealProdCLM.symm z)).re → f z = 0) : ∫ (z : ℝ × ℝ) in thricePuncturedSphereReal, f z = ∫ (z : ℝ × ℝ) in ⇑Complex.equivRealProdCLM.symm ⁻¹' ThricePuncturedSphere.truncation R, f z

The integral over S of a function vanishing at every point of S beyond R on some end is its integral over the truncation S_R.

theorem TauCeti.Floer.ae_mem_thricePuncturedSphereReal : ∀ᵐ (z : ℝ × ℝ), z ∈ thricePuncturedSphereReal

Almost every point of the plane lies in the pair of pants: the two punctures form a null set.

theorem TauCeti.Floer.contDiffAt_uncurry_pairOfPantsPerturbation {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {H : ThricePuncturedSphere.Puncture → ℝ → V → ℝ} {n : ℕ∞} (hH : ∀ (q : ThricePuncturedSphere.Puncture), Function.Periodic (H q) 1) (hHs : ∀ (q : ThricePuncturedSphere.Puncture), ContDiff ℝ (↑n) (Function.uncurry (H q))) {z : ℝ × ℝ} (hz : z ∈ thricePuncturedSphereReal) (x : V) (v : ℂ) : ContDiffAt ℝ (↑n) (Function.uncurry fun (z : ℝ × ℝ) (x : V) => (pairOfPantsPerturbation H (Complex.equivRealProdCLM.symm z) x) v) (z, x)

In the real coordinates of S, the components of the pair-of-pants perturbation are Cⁿ jointly in the domain and target points, for Cⁿ Hamiltonians.

theorem TauCeti.Floer.contMDiffOn_thricePuncturedSphereReal_prod_univ_of_forall_contMDiffAt {E : Type u_2} {G : Type u_3} {M : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace G] {I : ModelWithCorners ℝ E G} [TopologicalSpace M] [ChartedSpace G M] {K : ℂ → M → ℂ →L[ℝ] ℝ} (hK : ∀ (w : ThricePuncturedSphere) (x : M), ContMDiffAt ((modelWithCornersSelf ℝ ℂ).prod I) (modelWithCornersSelf ℝ (ℂ →L[ℝ] ℝ)) 1 (fun (p : ℂ × M) => K p.1 p.2) (↑w, x)) (v : ℂ) : ContMDiffOn ((modelWithCornersSelf ℝ (ℝ × ℝ)).prod I) (modelWithCornersSelf ℝ ℝ) 1 (Function.uncurry fun (z : ℝ × ℝ) (x : M) => (K (Complex.equivRealProdCLM.symm z) x) v) (thricePuncturedSphereReal ×ˢ Set.univ)

A perturbation one-form K on ℂ which is C¹ at every point of S × M has components (z, x) ↦ K(z, x)(v), in the real coordinates of S, that are C¹ jointly on S × M.

noncomputable def TauCeti.Floer.endChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : ℝ × ℝ

The end lift of q, in the real coordinates ℝ × ℝ ≃ ℂ.

theorem TauCeti.Floer.endChart_apply (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : endChart q z = Complex.equivRealProdCLM (q.cylindricalEndLift (Complex.equivRealProdCLM.symm z))

theorem TauCeti.Floer.endChart_eq_realChart (q : ThricePuncturedSphere.Puncture) : endChart q = Complex.realChart q.cylindricalEndLift

The end chart is the end lift read in the real coordinates.

theorem TauCeti.Floer.endChart_mk (q : ThricePuncturedSphere.Puncture) (s t : ℝ) : endChart q (s, t) = Complex.equivRealProdCLM (q.cylindricalEndLift (↑s + ↑t * Complex.I))

The end chart at a point (s, t) of the cylinder is the end lift at s + i t.

@[simp]

theorem TauCeti.Floer.equivRealProdCLM_symm_endChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : Complex.equivRealProdCLM.symm (endChart q z) = q.cylindricalEndLift (Complex.equivRealProdCLM.symm z)

In complex coordinates the end chart is the end lift.

theorem TauCeti.Floer.re_endCoord_endChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : (q.endCoord (Complex.equivRealProdCLM.symm (endChart q z))).re = z.1

The longitudinal coordinate of the end q at the image of (s, t) is s.

theorem TauCeti.Floer.endChart_mem_thricePuncturedSphereReal {q : ThricePuncturedSphere.Puncture} {z : ℝ × ℝ} (hz : 0 < q.endSign * z.1) : endChart q z ∈ thricePuncturedSphereReal

The end chart sends the part ±s > 0 of the end into S.

noncomputable def TauCeti.Floer.endStrip (q : ThricePuncturedSphere.Puncture) : Set (ℝ × ℝ)

The part ±s > 1/2, t ∈ [-1/2, 1/2) of the end q in its cylinder coordinates. It contains the support of the curvature of the end, and the end lift is injective on it.

theorem TauCeti.Floer.endStrip_def (q : ThricePuncturedSphere.Puncture) : endStrip q = {s : ℝ | 1 / 2 < q.endSign * s} ×ˢ Set.Ico (-1 / 2) (1 / 2)

@[simp]

theorem TauCeti.Floer.mem_endStrip_iff {q : ThricePuncturedSphere.Puncture} {z : ℝ × ℝ} : z ∈ endStrip q ↔ 1 / 2 < q.endSign * z.1 ∧ z.2 ∈ Set.Ico (-1 / 2) (1 / 2)

A point lies in the strip of the end q when its signed longitudinal coordinate exceeds 1/2 and its angular coordinate lies in [-1/2, 1/2).

theorem TauCeti.Floer.endSign_mul_pos_of_mem_endStrip {q : ThricePuncturedSphere.Puncture} {z : ℝ × ℝ} (hz : z ∈ endStrip q) : 0 < q.endSign * z.1

Points of the strip of an end have positive signed longitudinal coordinate.

theorem TauCeti.Floer.hasFDerivAt_endChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : HasFDerivAt (endChart q) (↑Complex.equivRealProdCLM ∘SL ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ (deriv q.cylindricalEndLift (Complex.equivRealProdCLM.symm z))) ∘SL ↑Complex.equivRealProdCLM.symm) z

The derivative of the end chart is multiplication by the derivative of the end lift.

theorem TauCeti.Floer.fderiv_endChart_apply (q : ThricePuncturedSphere.Puncture) (z v : ℝ × ℝ) : (fderiv ℝ (endChart q) z) v = Complex.equivRealProdCLM (deriv q.cylindricalEndLift (Complex.equivRealProdCLM.symm z) * Complex.equivRealProdCLM.symm v)

The derivative of the end chart is multiplication by the derivative of the end lift, in real coordinates.

theorem TauCeti.Floer.isComplexLinearMap_fderiv_endChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) (AlmostComplexStructure.product ℝ) ↑(fderiv ℝ (endChart q) z)

The end charts are holomorphic: their derivatives are complex linear.

theorem TauCeti.Floer.contDiff_endChart (q : ThricePuncturedSphere.Puncture) (n : WithTop ℕ∞) : ContDiff ℝ n (endChart q)

theorem TauCeti.Floer.perturbationPullback_endChart_eq_cylindricalEndLift {X : Type u_2} (K : ℂ → X → ℂ →L[ℝ] ℝ) (q : ThricePuncturedSphere.Puncture) (v : ℝ × ℝ) : 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 = fun (z : ℝ × ℝ) (x : X) => (K (q.cylindricalEndLift (Complex.equivRealProdCLM.symm z)) x) (deriv q.cylindricalEndLift (Complex.equivRealProdCLM.symm z) * Complex.equivRealProdCLM.symm v)

Perturbation data in end coordinates. Let K be a perturbation one-form on ℂ, with ds and dt components K(z)(1) and K(z)(i) in the global coordinate z = s + i t. Its pullback along the end chart of q, evaluated on a tangent vector v of the cylinder, is K at the image point evaluated on the image φ'(z) v of v under the end lift φ.

theorem TauCeti.Floer.perturbationPullback_endChart {V : Type u_1} {H : ThricePuncturedSphere.Puncture → ℝ → V → ℝ} (q : ThricePuncturedSphere.Puncture) (v : ℝ × ℝ) : perturbationPullback (endChart q) (fun (z : ℝ × ℝ) (x : V) => (pairOfPantsPerturbation H (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : V) => (pairOfPantsPerturbation H (Complex.equivRealProdCLM.symm z) x) Complex.I) v = pairOfPantsEndComponent H q (Complex.equivRealProdCLM.symm v)

The pullback of the perturbation along the end chart of q, evaluated on a tangent vector v, is its component TauCeti.Floer.pairOfPantsEndComponent along v in the end coordinates.

theorem TauCeti.Floer.perturbationPullback_endChart_stdComplexLineImag_of_le {X : Type u_2} {K : ℂ → X → ℂ →L[ℝ] ℝ} {H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ} {T₀ : ℝ} (hKH : ∀ (q : ThricePuncturedSphere.Puncture) (w : ℂ) (x : X), T₀ ≤ q.endSign * (q.endCoord w).re → K w x = H q (q.endCoord w).im x • q.endAngularForm w) (hH : ∀ (q : ThricePuncturedSphere.Puncture), Function.Periodic (H q) 1) {q : ThricePuncturedSphere.Puncture} {ζ : ℝ × ℝ} (hζ : T₀ ≤ q.endSign * ζ.1) (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) stdComplexLineImag ζ x = H q ζ.2 x

Where K = H_q(t) dt on the end q, its pullback along the end chart sends ∂_t to H_q(t).

theorem TauCeti.Floer.perturbationPullback_endChart_stdComplexLineReal_of_le {X : Type u_2} {K : ℂ → X → ℂ →L[ℝ] ℝ} {H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ} {T₀ : ℝ} (hKH : ∀ (q : ThricePuncturedSphere.Puncture) (w : ℂ) (x : X), T₀ ≤ q.endSign * (q.endCoord w).re → K w x = H q (q.endCoord w).im x • q.endAngularForm w) {q : ThricePuncturedSphere.Puncture} {ζ : ℝ × ℝ} (hζ : T₀ ≤ q.endSign * ζ.1) (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) stdComplexLineReal ζ x = 0

Where K = H_q(t) dt on the end q, its pullback along the end chart sends ∂_s to 0.

theorem TauCeti.Floer.injOn_endChart_univ_prod_Ico (q : ThricePuncturedSphere.Puncture) (t₀ : ℝ) : Set.InjOn (endChart q) (Set.univ ×ˢ Set.Ico t₀ (t₀ + 1))

The end chart is injective on every band ℝ × [t₀, t₀ + 1) of angular width one: two points with the same image differ by an integer multiple of i.

theorem TauCeti.Floer.injOn_endChart (q : ThricePuncturedSphere.Puncture) : Set.InjOn (endChart q) (endStrip q)

The end lift is injective on the strip endStrip q, whose angular coordinate ranges over one period.

theorem TauCeti.Floer.mem_image_endChart {z : ℝ × ℝ} (hz : z ∈ thricePuncturedSphereReal) {q : ThricePuncturedSphere.Puncture} (hq : 1 / 2 < q.endSign * (q.endCoord (Complex.equivRealProdCLM.symm z)).re) : z ∈ endChart q '' endStrip q

Every point of S where some end has signed longitudinal coordinate greater than 1/2 is the image of a point of that end's strip.

theorem TauCeti.Floer.image_endChart_prod_Ico {q : ThricePuncturedSphere.Puncture} {P : Set ℝ} (hP : ∀ s ∈ P, 0 < q.endSign * s) : endChart q '' P ×ˢ Set.Ico 0 1 = {z : ℝ × ℝ | z ∈ thricePuncturedSphereReal ∧ (q.endCoord (Complex.equivRealProdCLM.symm z)).re ∈ P}

The points of S at which the longitudinal coordinate of the end q lies in a set P of positive signed values are exactly the images under the end chart of P × [0, 1).

theorem TauCeti.Floer.preimage_truncation_inter_eq_image_endChart (q : ThricePuncturedSphere.Puncture) {c : ℝ} (hc : 0 ≤ c) (R : ℝ) : ⇑Complex.equivRealProdCLM.symm ⁻¹' ThricePuncturedSphere.truncation R ∩ {z : ℝ × ℝ | c < q.endSign * (q.endCoord (Complex.equivRealProdCLM.symm z)).re} = endChart q '' {s : ℝ | c < q.endSign * s ∧ q.endSign * s ≤ R} ×ˢ Set.Ico 0 1

For 0 ≤ c, the part ±s > c of the end q in the truncation S_R is the image under the end chart of c < ±s ≤ R, t ∈ [0, 1).

theorem TauCeti.Floer.measurableSet_endStrip (q : ThricePuncturedSphere.Puncture) : MeasurableSet (endStrip q)

The strip of an end is measurable.

theorem TauCeti.Floer.det_fderiv_endChart_nonneg (q : ThricePuncturedSphere.Puncture) (ζ : ℝ × ℝ) : 0 ≤ (fderiv ℝ (endChart q) ζ).det

The end charts preserve orientation.

theorem TauCeti.Floer.det_fderiv_endChart_pos (q : ThricePuncturedSphere.Puncture) (ζ : ℝ × ℝ) : 0 < (fderiv ℝ (endChart q) ζ).det

The end charts are local diffeomorphisms: their Jacobian determinants are positive.

theorem TauCeti.Floer.pairwise_disjoint_image_endChart : Pairwise (Function.onFun Disjoint fun (q : ThricePuncturedSphere.Puncture) => endChart q '' endStrip q)

The three end strips have disjoint images.

Positive end charts

noncomputable def TauCeti.Floer.positiveEndChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : ℝ × ℝ

The end chart of q read as a positive end: (s, t) ↦ φ_q(±s, ±t), with the sign ± of the end, so that s → ∞ along every end. It is the end chart TauCeti.Floer.endChart q on the input ends, and (s, t) ↦ φ_∞(-s, -t) on the output end.

theorem TauCeti.Floer.positiveEndChart_apply (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : positiveEndChart q z = endChart q (q.endSign • z)

theorem TauCeti.Floer.positiveEndChart_mk (q : ThricePuncturedSphere.Puncture) (s t : ℝ) : positiveEndChart q (s, t) = endChart q (q.endSign * s, q.endSign * t)

theorem TauCeti.Floer.endChart_eq_positiveEndChart (q : ThricePuncturedSphere.Puncture) (s t : ℝ) : endChart q (q.endSign * s, t) = positiveEndChart q (s, q.endSign * t)

The end chart at (±s, t) is the positive end chart at (s, ±t).

theorem TauCeti.Floer.positiveEndChart_add_one (q : ThricePuncturedSphere.Puncture) (s t : ℝ) : positiveEndChart q (s, t + 1) = positiveEndChart q (s, t)

The positive end chart is 1-periodic in the angular coordinate.

theorem TauCeti.Floer.hasFDerivAt_positiveEndChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : HasFDerivAt (positiveEndChart q) (fderiv ℝ (endChart q) (q.endSign • z) ∘SL (q.endSign • ContinuousLinearMap.id ℝ (ℝ × ℝ))) z

The derivative of the positive end chart is the derivative of the end chart at the reflected point, composed with the reflection v ↦ ±v.

theorem TauCeti.Floer.fderiv_positiveEndChart_apply (q : ThricePuncturedSphere.Puncture) (z v : ℝ × ℝ) : (fderiv ℝ (positiveEndChart q) z) v = q.endSign • (fderiv ℝ (endChart q) (q.endSign • z)) v

theorem TauCeti.Floer.contDiff_positiveEndChart (q : ThricePuncturedSphere.Puncture) (n : WithTop ℕ∞) : ContDiff ℝ n (positiveEndChart q)

theorem TauCeti.Floer.isComplexLinearMap_fderiv_positiveEndChart (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : IsComplexLinearMap (AlmostComplexStructure.product ℝ) (AlmostComplexStructure.product ℝ) ↑(fderiv ℝ (positiveEndChart q) z)

The positive end charts are holomorphic.

theorem TauCeti.Floer.det_fderiv_positiveEndChart_pos (q : ThricePuncturedSphere.Puncture) (z : ℝ × ℝ) : 0 < (fderiv ℝ (positiveEndChart q) z).det

The positive end charts preserve orientation strictly.

theorem TauCeti.Floer.positiveEndChart_mem_thricePuncturedSphereReal {q : ThricePuncturedSphere.Puncture} {z : ℝ × ℝ} (hz : 0 < z.1) : positiveEndChart q z ∈ thricePuncturedSphereReal

The positive end chart sends the part s > 0 of the end into S.

theorem TauCeti.Floer.injOn_positiveEndChart (q : ThricePuncturedSphere.Puncture) : Set.InjOn (positiveEndChart q) (Set.univ ×ˢ Set.Ioo 0 1)

The positive end chart is injective on the open band ℝ × (0, 1).

noncomputable def TauCeti.Floer.positiveEndHamiltonian {X : Type u_2} (H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ) (q : ThricePuncturedSphere.Puncture) (t : ℝ) (x : X) : ℝ

The Hamiltonian of the end q in its positive end chart: H'_q(t, x) = ±H_q(±t, x) with the sign of the end. It is H_q on the input ends and (t, x) ↦ -H_∞(-t, x) on the output end.

theorem TauCeti.Floer.positiveEndHamiltonian_apply {X : Type u_2} (H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ) (q : ThricePuncturedSphere.Puncture) (t : ℝ) (x : X) : positiveEndHamiltonian H q t x = q.endSign * H q (q.endSign * t) x

theorem TauCeti.Floer.periodic_positiveEndHamiltonian {X : Type u_2} {H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ} {q : ThricePuncturedSphere.Puncture} (hH : Function.Periodic (H q) 1) : Function.Periodic (positiveEndHamiltonian H q) 1

theorem TauCeti.Floer.contDiff_uncurry_positiveEndHamiltonian {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : ThricePuncturedSphere.Puncture → ℝ → E → ℝ} {q : ThricePuncturedSphere.Puncture} {n : WithTop ℕ∞} (hH : ContDiff ℝ n (Function.uncurry (H q))) : ContDiff ℝ n (Function.uncurry (positiveEndHamiltonian H q))

theorem TauCeti.Floer.periodic_comp_endSign_mul {α : Type u_2} {q : ThricePuncturedSphere.Puncture} {x : ℝ → α} (hx : Function.Periodic x 1) : Function.Periodic (fun (t : ℝ) => x (q.endSign * t)) 1

A 1-periodic loop read with the time ±t of an end is 1-periodic.

theorem TauCeti.Floer.perturbationPullback_positiveEndChart {X : Type u_2} {K : ℂ → X → ℂ →L[ℝ] ℝ} (q : ThricePuncturedSphere.Puncture) (v ζ : ℝ × ℝ) (x : X) : perturbationPullback (positiveEndChart 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 ζ x = q.endSign * 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 (q.endSign • ζ) x

The pullback of a perturbation along the positive end chart is the pullback along the end chart at the reflected point, multiplied by the sign of the end.

theorem TauCeti.Floer.perturbationPullback_positiveEndChart_stdComplexLineReal_of_le {X : Type u_2} {K : ℂ → X → ℂ →L[ℝ] ℝ} {H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ} {T₀ : ℝ} (hKH : ∀ (q : ThricePuncturedSphere.Puncture) (w : ℂ) (x : X), T₀ ≤ q.endSign * (q.endCoord w).re → K w x = H q (q.endCoord w).im x • q.endAngularForm w) {q : ThricePuncturedSphere.Puncture} {ζ : ℝ × ℝ} (hζ : T₀ ≤ ζ.1) (x : X) : perturbationPullback (positiveEndChart q) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineReal ζ x = 0

Where K = H_q(t) dt on the end q, its pullback along the positive end chart sends ∂_s to 0.

theorem TauCeti.Floer.perturbationPullback_positiveEndChart_stdComplexLineImag_of_le {X : Type u_2} {K : ℂ → X → ℂ →L[ℝ] ℝ} {H : ThricePuncturedSphere.Puncture → ℝ → X → ℝ} {T₀ : ℝ} (hKH : ∀ (q : ThricePuncturedSphere.Puncture) (w : ℂ) (x : X), T₀ ≤ q.endSign * (q.endCoord w).re → K w x = H q (q.endCoord w).im x • q.endAngularForm w) (hH : ∀ (q : ThricePuncturedSphere.Puncture), Function.Periodic (H q) 1) {q : ThricePuncturedSphere.Puncture} {ζ : ℝ × ℝ} (hζ : T₀ ≤ ζ.1) (x : X) : perturbationPullback (positiveEndChart q) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) 1) (fun (z : ℝ × ℝ) (x : X) => (K (Complex.equivRealProdCLM.symm z) x) Complex.I) stdComplexLineImag ζ x = positiveEndHamiltonian H q ζ.2 x

Where K = H_q(t) dt on the end q, its pullback along the positive end chart sends ∂_t to the end Hamiltonian H'_q(t) of the positive end.