The mean-value inequality on half-discs with a Neumann condition

Let x₀ be a point of the real axis and let w ≥ 0 be C² on the half-disc {0 ≤ im z} ∩ ball x₀ r, up to its straight edge, with

Δ w ≥ -A w² above the axis and ∂ₜ w = 0 on the axis.

The boundary mean-value inequality says that if the integral of w over the half-disc is small, 16 A ∫ w < π, then

π r² w x₀ ≤ 16 ∫_{{0 ≤ im z} ∩ ball x₀ r} w.

The proof reflects w evenly across the real axis (TauCeti.evenReflection). The Neumann condition makes the reflection C² on the whole disc (TauCeti.contDiffOn_evenReflection); its Laplacian satisfies the same inequality, off the axis because conjugation is an isometry and on the axis by continuity; and its integral over the disc is at most twice that of w over the half-disc. The interior mean-value inequality TauCeti.mul_le_eight_mul_setIntegral_ball_of_neg_mul_sq_le_laplacian then applies to the reflection, centred at the boundary point x₀.

In Gromov compactness for holomorphic strips and discs with totally real boundary conditions, w is the energy density |∂ₛu|² of a curve on a half-disc whose straight edge is mapped to the totally real submanifold. For a metric adapted to the boundary condition this density satisfies the hypotheses above, and the inequality gives the pointwise derivative bound at boundary points for curves of small energy, the boundary counterpart of the interior estimate TauCeti.pi_mul_sq_mul_norm_fderiv_one_sq_le_eight_mul_setIntegral_ball. The geometric input, the Neumann condition and differential inequality for the energy density, is not proved here.

Main results

• TauCeti.neg_mul_sq_le_laplacian_evenReflection: the even reflection of w satisfies Δ w ≥ -A w² on the whole disc.
• TauCeti.pi_mul_sq_mul_le_sixteen_mul_setIntegral_inter_ball_of_neg_mul_sq_le_laplacian: the boundary mean-value inequality.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Section 4.3 (the mean-value inequality, and its version for half-discs proved by reflecting the energy density in the boundary).

theorem TauCeti.neg_mul_sq_le_laplacian_evenReflection {w : ℂ → ℝ} {x₀ : ℂ} {r A : ℝ} (hx₀ : x₀.im = 0) (hw : ContDiffOn ℝ 2 w ({z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r)) (hN : ∀ x ∈ Metric.ball x₀ r, x.im = 0 → (fderivWithin ℝ w ({z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r) x) Complex.I = 0) (hΔ : ∀ z ∈ Metric.ball x₀ r, 0 < z.im → -(A * w z ^ 2) ≤ Laplacian.laplacian w z) {z : ℂ} (hz : z ∈ Metric.ball x₀ r) : -(A * evenReflection w z ^ 2) ≤ Laplacian.laplacian (evenReflection w) z

If w is C² up to the real axis on a disc centred on the axis, satisfies the Neumann condition on the axis and Δ w ≥ -A w² above it, then its even reflection satisfies Δ w ≥ -A w² on the whole disc.

theorem TauCeti.pi_mul_sq_mul_le_sixteen_mul_setIntegral_inter_ball_of_neg_mul_sq_le_laplacian {w : ℂ → ℝ} {x₀ : ℂ} {r A : ℝ} (hx₀ : x₀.im = 0) (hr : 0 ≤ r) (hw : ContDiffOn ℝ 2 w ({z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r)) (hwc : ContinuousOn w ({z : ℂ | 0 ≤ z.im} ∩ Metric.closedBall x₀ r)) (hw0 : ∀ z ∈ {z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r, 0 ≤ w z) (hN : ∀ x ∈ Metric.ball x₀ r, x.im = 0 → (fderivWithin ℝ w ({z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r) x) Complex.I = 0) (hΔ : ∀ z ∈ Metric.ball x₀ r, 0 < z.im → -(A * w z ^ 2) ≤ Laplacian.laplacian w z) (hsmall : 16 * A * ∫ (z : ℂ) in {z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r, w z < Real.pi) : Real.pi * r ^ 2 * w x₀ ≤ 16 * ∫ (z : ℂ) in {z : ℂ | 0 ≤ z.im} ∩ Metric.ball x₀ r, w z

The boundary mean-value inequality. Let x₀ lie on the real axis, and let w ≥ 0 be C² on the half-disc {0 ≤ im z} ∩ ball x₀ r up to its straight edge, continuous on its closure, with Δ w ≥ -A w² above the axis and vanishing normal derivative ∂ₜ w = 0 on the axis. If 16 A ∫ w < π over the half-disc, then

π r² w x₀ ≤ 16 ∫_{{0 ≤ im z} ∩ ball x₀ r} w.