Documentation

TauCeti.Geometry.Symplectic.JHolomorphic.Energy.MeanValue

The mean-value inequality for J-holomorphic curves #

Let V be a real inner product space and J : V → (V →L[ℝ] V) a C² family of linear maps with J(x)² = -1, an almost complex structure on V written as a matrix-valued function, as in local coordinates on an almost complex manifold. A map u : ℂ → V, with s + i t the coordinate on ℂ, is J-holomorphic when it solves the Cauchy--Riemann equation ∂ₛu + J(u) ∂ₜu = 0, that is ∂ₜu = J(u) ∂ₛu. Here ∂ₛu = du(1) and ∂ₜu = du(i) are written fderiv ℝ u y 1 and fderiv ℝ u y I. Since J(u)² = -1, this single equation says that du intertwines multiplication by i with J(u); a curve that is TauCeti.IsJHolomorphicAt for the standard complex structure of ℂ satisfies it (TauCeti.IsJHolomorphicAt.fderiv_I_eq).

The energy density ‖∂ₛu‖² of such a curve satisfies the differential inequality

Δ ‖∂ₛu‖² ≥ -A ‖∂ₛu‖⁴,

with A = 4ac + 2b² + 8a²b² whenever a, b, c bound J, its first derivative and its second derivative along u. Differentiating the Cauchy--Riemann equation twice and using J(u)² = -1 removes the third derivatives of u from Δ ∂ₛu. What remains is bounded by ‖∂ₛu‖³ and by ‖∂ₛu‖ times the second derivatives of u, and the positive term 2 ‖∇ ∂ₛu‖² in Δ ‖∂ₛu‖² absorbs the latter. For constant J the constant A vanishes and ‖∂ₛu‖² is subharmonic.

Fed into the two-dimensional mean-value inequality TauCeti.mul_le_eight_mul_setIntegral_ball_of_neg_mul_sq_le_laplacian, this gives the pointwise derivative bound for curves of small energy, the basic estimate behind bubbling and Gromov compactness: if 8 A ∫_{B_r(z₀)} ‖∂ₛu‖² < π, then

π r² ‖∂ₛu(z₀)‖² ≤ 8 ∫_{B_r(z₀)} ‖∂ₛu‖².

For J that is C² on an open set containing a compact set K, one smallness threshold δ > 0 works for all curves with image in K. As ∂ₜu = J(u) ∂ₛu, these bounds control the full derivative of u.

Main declarations #

References #

source
theorem TauCeti.IsJHolomorphicAt.fderiv_I_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {u : ℂ → V} {z : ℂ} {J' : V → AlmostComplexStructure V} (h : IsJHolomorphicAt (fun (x : ℂ) => AlmostComplexStructure.ofComplexModule ℂ) J' u z) :
(fderiv ℝ u z) Complex.I = (J' (u z)).toLinearMap ((fderiv ℝ u z) 1)

A curve that is J'-holomorphic at z for the standard complex structure of ℂ satisfies the Cauchy--Riemann equation in the form ∂ₜu = J'(u) ∂ₛu used in this file.

source
theorem TauCeti.neg_mul_norm_fderiv_one_pow_four_le_laplacian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {u : ℂ → V} {J : V → V →L[ℝ] V} {z : ℂ} {a b c : ℝ} (hu : ContDiffAt ℝ 3 u z) (hJ : ContDiffAt ℝ 2 J (u z)) (hCR : ∀ᶠ (y : ℂ) in nhds z, (fderiv ℝ u y) Complex.I = (J (u y)) ((fderiv ℝ u y) 1)) (hJsq : ∀ (v : V), (J (u z)) ((J (u z)) v) = -v) (ha : ‖J (u z)‖ ≤ a) (hb : ‖fderiv ℝ J (u z)‖ ≤ b) (hc : ‖iteratedFDeriv ℝ 2 J (u z)‖ ≤ c) :
-((4 * a * c + 2 * b ^ 2 + 8 * a ^ 2 * b ^ 2) * ‖(fderiv ℝ u z) 1‖ ^ 4) ≤ Laplacian.laplacian (fun (y : ℂ) => ‖(fderiv ℝ u y) 1‖ ^ 2) z

The energy density of a J-holomorphic curve is almost subharmonic. Let u : ℂ → V be C³ at z and solve the Cauchy--Riemann equation ∂ₜu = J(u) ∂ₛu near z, where J is C² at u z with J(u z)² = -1. If a, b and c bound the norms of J, of its derivative and of its second derivative at u z, then

Δ ‖∂ₛu‖² ≥ -(4ac + 2b² + 8a²b²) ‖∂ₛu‖⁴ at z.

source
theorem TauCeti.pi_mul_sq_mul_norm_fderiv_one_sq_le_eight_mul_setIntegral_ball {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {u : ℂ → V} {J : V → V →L[ℝ] V} {z₀ : ℂ} {r a b c : ℝ} (hr : 0 ≤ r) (hu : ContDiffOn ℝ 3 u (Metric.ball z₀ r)) (hu' : ContinuousOn (fun (y : ℂ) => (fderiv ℝ u y) 1) (Metric.closedBall z₀ r)) (hCR : ∀ y ∈ Metric.ball z₀ r, (fderiv ℝ u y) Complex.I = (J (u y)) ((fderiv ℝ u y) 1)) (hJ : ∀ y ∈ Metric.ball z₀ r, ContDiffAt ℝ 2 J (u y)) (hJsq : ∀ y ∈ Metric.ball z₀ r, ∀ (v : V), (J (u y)) ((J (u y)) v) = -v) (ha : ∀ y ∈ Metric.ball z₀ r, ‖J (u y)‖ ≤ a) (hb : ∀ y ∈ Metric.ball z₀ r, ‖fderiv ℝ J (u y)‖ ≤ b) (hc : ∀ y ∈ Metric.ball z₀ r, ‖iteratedFDeriv ℝ 2 J (u y)‖ ≤ c) (hsmall : 8 * (4 * a * c + 2 * b ^ 2 + 8 * a ^ 2 * b ^ 2) * ∫ (y : ℂ) in Metric.ball z₀ r, ‖(fderiv ℝ u y) 1‖ ^ 2 < Real.pi) :
Real.pi * r ^ 2 * ‖(fderiv ℝ u z₀) 1‖ ^ 2 ≤ 8 * ∫ (y : ℂ) in Metric.ball z₀ r, ‖(fderiv ℝ u y) 1‖ ^ 2

The mean-value inequality for J-holomorphic curves. Let u : ℂ → V be C³ on the open disk ball z₀ r, with ∂ₛu continuous on its closure, and solve the Cauchy--Riemann equation ∂ₜu = J(u) ∂ₛu on the disk. Suppose that on the disk J is C² along u, squares to -1, and a, b, c bound the norms of J, of its derivative and of its second derivative along u. If the energy ∫ ‖∂ₛu‖² over the disk is small, 8 (4ac + 2b² + 8a²b²) ∫ ‖∂ₛu‖² < π, then ‖∂ₛu(z₀)‖² is at most eight times its average over the disk:

π r² ‖∂ₛu(z₀)‖² ≤ 8 ∫_{B_r(z₀)} ‖∂ₛu‖².

source
theorem TauCeti.exists_pos_forall_pi_mul_sq_mul_norm_fderiv_one_sq_le_eight_mul_setIntegral_ball {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {J : V → V →L[ℝ] V} {W K : Set V} (hW : IsOpen W) (hJ : ContDiffOn ℝ 2 J W) (hK : IsCompact K) (hKW : K ⊆ W) (hJsq : ∀ x ∈ K, ∀ (v : V), (J x) ((J x) v) = -v) :
∃ δ > 0, ∀ ⦃u : ℂ → V⦄ ⦃z₀ : ℂ⦄ ⦃r : ℝ⦄, 0 ≤ r → ContDiffOn ℝ 3 u (Metric.ball z₀ r) → ContinuousOn (fun (y : ℂ) => (fderiv ℝ u y) 1) (Metric.closedBall z₀ r) → (∀ y ∈ Metric.ball z₀ r, (fderiv ℝ u y) Complex.I = (J (u y)) ((fderiv ℝ u y) 1)) → (∀ y ∈ Metric.ball z₀ r, u y ∈ K) → ∫ (y : ℂ) in Metric.ball z₀ r, ‖(fderiv ℝ u y) 1‖ ^ 2 < δ → Real.pi * r ^ 2 * ‖(fderiv ℝ u z₀) 1‖ ^ 2 ≤ 8 * ∫ (y : ℂ) in Metric.ball z₀ r, ‖(fderiv ℝ u y) 1‖ ^ 2

The mean-value inequality for J-holomorphic curves in a compact set. Let J be C² on an open set W containing a compact set K, with J(x)² = -1 on K. There is an energy threshold δ > 0 such that every solution u of ∂ₜu = J(u) ∂ₛu that is C³ on the open disk ball z₀ r, has ∂ₛu continuous on its closure, maps the disk into K and has energy ∫ ‖∂ₛu‖² < δ over it, satisfies π r² ‖∂ₛu(z₀)‖² ≤ 8 ∫_{B_r(z₀)} ‖∂ₛu‖².