The mean-value inequality for Δ w ≥ -A w²

Let E be a real inner product space of dimension two with an additive Haar measure μ, and let w ≥ 0 be a C² function on a ball ball x₀ r with

Δ w ≥ -A w².

The mean-value inequality says that if the integral of w over the ball is small, 8 A ∫ w < μ (ball 0 1), then w is controlled at the centre by its average:

μ (ball x₀ r) * w x₀ ≤ 8 * ∫ x in ball x₀ r, w x ∂μ.

For Lebesgue measure on ℂ, with r > 0 and A > 0, this is w x₀ ≤ 8 / (π r²) ∫ w under ∫ w < π / (8 A). Applied to the energy density w = |du|² of a J-holomorphic curve, which satisfies such a differential inequality, it bounds the derivative of a curve with small energy pointwise; this is the analytic input to bubbling and Gromov compactness. The nonlinearity w² is critical in dimension two: both sides of the hypothesis and the conclusion scale in the same way under dilations, which is why the smallness condition does not depend on r.

The proof has two steps.

• A quadratic correction. If Δ w ≥ -K on ball x₀ R, then w + K ‖x - x₀‖² / (2n) has nonnegative Laplacian, and the sub-mean-value inequality TauCeti.mul_le_setIntegral_ball_of_laplacian_nonneg together with ∫ x in ball x₀ R, ‖x - x₀‖² = n R² μ (ball x₀ R) / (n + 2) gives μ (ball x₀ R) * w x₀ ≤ ∫ w + K R² μ (ball x₀ R) / (2 (n + 2)), in any dimension n.
• Choosing the centre. The continuous function (r - ρ)² w z on the compact set {(ρ, z) | 0 ≤ ρ ≤ r, dist z x₀ ≤ ρ} attains its maximum at some (ρ, z). With c = w z and ε = (r - ρ) / 2, maximality gives r² w x₀ ≤ 4 ε² c and w ≤ 4 c on closedBall z ε, so Δ w ≥ -16 A c² there. The first step on a ball ball z δ with δ ≤ ε and 4 A c δ² ≤ 1 gives δ² c μ (ball 0 1) ≤ 2 ∫ w. If δ = ε is allowed, this together with r² w x₀ ≤ 4 ε² c is the claim; otherwise δ² = 1 / (4 A c) contradicts the smallness of ∫ w.

Main declarations

• TauCeti.mul_le_setIntegral_ball_add_of_neg_le_laplacian: the mean-value inequality for Δ w ≥ -K, in any dimension.
• TauCeti.mul_le_eight_mul_setIntegral_ball_of_neg_mul_sq_le_laplacian: the mean-value inequality for Δ w ≥ -A w² in dimension two.

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).

theorem TauCeti.mul_le_setIntegral_ball_add_of_neg_le_laplacian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {w : E → ℝ} {x₀ : E} {R K : ℝ} (hw : ContDiffOn ℝ 2 w (Metric.ball x₀ R)) (hwc : ContinuousOn w (Metric.closedBall x₀ R)) (hΔ : ∀ x ∈ Metric.ball x₀ R, -K ≤ Laplacian.laplacian w x) : μ.real (Metric.ball x₀ R) * w x₀ ≤ ∫ (x : E) in Metric.ball x₀ R, w x ∂μ + K * R ^ 2 / (2 * (↑(Module.finrank ℝ E) + 2)) * μ.real (Metric.ball x₀ R)

The mean-value inequality for Δ w ≥ -K. If w is C² on the ball ball x₀ R, continuous on its closure, and Δ w ≥ -K on the ball, then, in dimension n, μ (ball x₀ R) * w x₀ ≤ ∫ x in ball x₀ R, w x ∂μ + K R² / (2 (n + 2)) * μ (ball x₀ R).

theorem TauCeti.mul_le_eight_mul_setIntegral_ball_of_neg_mul_sq_le_laplacian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] (hE : Module.finrank ℝ E = 2) {w : E → ℝ} {x₀ : E} {r A : ℝ} (hw : ContDiffOn ℝ 2 w (Metric.ball x₀ r)) (hwc : ContinuousOn w (Metric.closedBall x₀ r)) (hw0 : ∀ x ∈ Metric.ball x₀ r, 0 ≤ w x) (hΔ : ∀ x ∈ Metric.ball x₀ r, -(A * w x ^ 2) ≤ Laplacian.laplacian w x) (hsmall : 8 * A * ∫ (x : E) in Metric.ball x₀ r, w x ∂μ < μ.real (Metric.ball 0 1)) : μ.real (Metric.ball x₀ r) * w x₀ ≤ 8 * ∫ (x : E) in Metric.ball x₀ r, w x ∂μ

The mean-value inequality. Let E be two-dimensional, and let w be C² on the ball ball x₀ r, continuous on its closure, nonnegative on the ball, with Δ w ≥ -A w² there. If 8 A ∫ w < μ (ball 0 1) over the ball, then μ (ball x₀ r) * w x₀ ≤ 8 ∫ w. For Lebesgue measure on ℂ, where μ (ball 0 1) = π, and for r > 0 and A > 0, this is w x₀ ≤ 8 / (π r²) ∫ w under ∫ w < π / (8 A).