Morrey's Dirichlet growth theorem

Let u ∈ W^{1,p}(Ω), 1 ≤ p, on an open subset Ω of a finite-dimensional real inner product space of dimension n, and let 0 < α. Morrey's Dirichlet growth theorem says that if the gradient of u grows on balls like

∫_{B(x, r)} ‖∇u‖ ≤ M r^(n - 1 + α),

then u is α-Hölder continuous, with Hölder constant a multiple of M depending only on n, α and μ(B(0, 1)). More precisely the Hölder continuous function is the precise representative TauCeti.MeasureTheory.preciseRepresentative of u, the limit of its averages over shrinking balls, which agrees with u almost everywhere on Ω by TauCeti.W1p.ae_eq_preciseRepresentative.

This is the form in which energy estimates deliver Hölder regularity. A Caccioppoli inequality together with a comparison argument typically bounds ∫_{B(x, r)} ‖∇u‖² by r^(n - 2 + 2α); by the Cauchy–Schwarz inequality on the ball this gives the growth condition above. In the Campanato approach to the Schauder estimates the same theorem, applied to the derivatives of a solution, gives Hölder continuity of the gradient.

The proof combines two results. The Poincaré–Wirtinger inequality on balls (TauCeti.W1p.setIntegral_abs_value_sub_setAverage_le_of_ball_subset) bounds the mean oscillation of u on a ball of radius r by 2^(n + 1) r times the average of ‖∇u‖ over the ball, so the growth condition makes the mean oscillation O(r^α). Campanato's theorem (TauCeti.MeasureTheory.dist_preciseRepresentative_le_of_setAverage_norm_sub_le) turns such a bound into a Hölder estimate for the precise representative.

The growth condition only needs to hold for balls centred at the points under consideration and for radii up to a multiple of their distance, so the theorem applies to interior estimates.

Main declarations

• TauCeti.W1p.setAverage_norm_value_sub_setAverage_closedBall_le: the mean oscillation of u on closedBall x r is at most 2^(n + 1) r times the average of ‖∇u‖ over ball x r.
• TauCeti.W1p.dist_preciseRepresentative_le_of_setIntegral_norm_gradient_le: the pointwise Hölder estimate between two points.
• TauCeti.W1p.holderOnWith_preciseRepresentative_of_setIntegral_norm_gradient_le: Morrey's Dirichlet growth theorem on a subset of Ω.
• TauCeti.W1p.holderWith_preciseRepresentative_of_setIntegral_norm_gradient_le: the same on the whole space.

References

• C. B. Morrey, Multiple Integrals in the Calculus of Variations, Theorem 3.5.2.
• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 7.19.
• M. Giaquinta, L. Martinazzi, An Introduction to the Regularity Theory for Elliptic Systems, Harmonic Maps and Minimal Graphs, Theorem 5.7.

theorem TauCeti.W1p.setAverage_norm_value_sub_setAverage_closedBall_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {x : E} {r : ℝ} (hr : 0 < r) (hball : Metric.ball x r ⊆ ↑Omega) (u : ↥(W1p mu Omega p)) : ⨍ (y : E) in Metric.closedBall x r, ‖↑↑(value u) y - ⨍ (z : E) in Metric.closedBall x r, ↑↑(value u) z ∂mu‖ ∂mu ≤ 2 ^ (Module.finrank ℝ E + 1) * r * ⨍ (y : E) in Metric.ball x r, ‖↑↑(gradient u) y‖ ∂mu

Poincaré's inequality for the mean oscillation on a closed ball. If u ∈ W^{1,p}(Ω) and B(x, r) ⊆ Ω, the mean oscillation ⨍_{closedBall x r} |u - u_{x,r}| of u is at most 2^(n + 1) r times the average of ‖∇u‖ over B(x, r).

theorem TauCeti.W1p.dist_preciseRepresentative_le_of_setIntegral_norm_gradient_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {α M : ℝ} (hα : 0 < α) (u : ↥(W1p mu Omega p)) {x y : E} (hxy : Metric.closedBall x (2 * dist x y) ⊆ ↑Omega) (hx : ∀ (r : ℝ), 0 < r → r ≤ 2 * dist x y → ∫ (z : E) in Metric.ball x r, ‖↑↑(gradient u) z‖ ∂mu ≤ M * r ^ (↑(Module.finrank ℝ E) - 1 + α)) (hy : ∀ (r : ℝ), 0 < r → r ≤ dist x y → ∫ (z : E) in Metric.ball y r, ‖↑↑(gradient u) z‖ ∂mu ≤ M * r ^ (↑(Module.finrank ℝ E) - 1 + α)) : dist (MeasureTheory.preciseRepresentative mu (↑↑(value u)) x) (MeasureTheory.preciseRepresentative mu (↑↑(value u)) y) ≤ 2 * 2 ^ α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-α))) * (2 ^ (Module.finrank ℝ E + 1) / mu.real (Metric.ball 0 1) * M * dist x y ^ α)

The pointwise Morrey estimate. Let u ∈ W^{1,p}(Ω), α > 0, d = dist x y, and suppose that closedBall x (2 d) ⊆ Ω and that the gradient of u satisfies the growth condition ∫_{B(z, r)} ‖∇u‖ ≤ M r^(n - 1 + α) for z = x, 0 < r ≤ 2 d and for z = y, 0 < r ≤ d. Then the precise representative u* of u satisfies

|u*(x) - u*(y)| ≤ 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · 2^(n + 1) / ω · M d^α,

where ω is the measure of the unit ball.

theorem TauCeti.W1p.holderOnWith_preciseRepresentative_of_setIntegral_norm_gradient_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {Omega : TopologicalSpace.Opens E} {p : ENNReal} [Fact (1 ≤ p)] {α : NNReal} (hα : 0 < α) {M R : ℝ} (u : ↥(W1p mu Omega p)) {K : Set E} (hKR : ∀ x ∈ K, ∀ y ∈ K, dist x y ≤ R) (hK : Metric.cthickening (2 * R) K ⊆ ↑Omega) (hgrowth : ∀ x ∈ K, ∀ (r : ℝ), 0 < r → r ≤ 2 * R → ∫ (z : E) in Metric.ball x r, ‖↑↑(gradient u) z‖ ∂mu ≤ M * r ^ (↑(Module.finrank ℝ E) - 1 + ↑α)) : HolderOnWith (2 * 2 ^ ↑α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-↑α))) * (2 ^ (Module.finrank ℝ E + 1) / mu.real (Metric.ball 0 1) * M)).toNNReal α (MeasureTheory.preciseRepresentative mu ↑↑(value u)) K

Morrey's Dirichlet growth theorem. Let u ∈ W^{1,p}(Ω) and α > 0, and let K be a set of diameter at most R whose closed 2R-thickening lies in Ω. If the gradient of u satisfies the growth condition

∫_{B(x, r)} ‖∇u‖ ≤ M r^(n - 1 + α) for every x ∈ K and 0 < r ≤ 2R,

then the precise representative of u is α-Hölder continuous on K, with Hölder constant 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · 2^(n + 1) / ω · M, where ω is the measure of the unit ball.

theorem TauCeti.W1p.holderWith_preciseRepresentative_of_setIntegral_norm_gradient_le {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : ENNReal} [Fact (1 ≤ p)] {α : NNReal} (hα : 0 < α) {M : ℝ} (u : ↥(W1p mu ⊤ p)) (hgrowth : ∀ (x : E) (r : ℝ), 0 < r → ∫ (z : E) in Metric.ball x r, ‖↑↑(gradient u) z‖ ∂mu ≤ M * r ^ (↑(Module.finrank ℝ E) - 1 + ↑α)) : HolderWith (2 * 2 ^ ↑α * (2 ^ Module.finrank ℝ E / (1 - 2 ^ (-↑α))) * (2 ^ (Module.finrank ℝ E + 1) / mu.real (Metric.ball 0 1) * M)).toNNReal α (MeasureTheory.preciseRepresentative mu ↑↑(value u))

Morrey's Dirichlet growth theorem on the whole space. Let u ∈ W^{1,p} of the whole space and α > 0. If ∫_{B(x, r)} ‖∇u‖ ≤ M r^(n - 1 + α) for every ball B(x, r), then the precise representative of u is α-Hölder continuous, with Hölder constant 2 · 2^α · 2ⁿ / (1 - 2^(-α)) · 2^(n + 1) / ω · M, where ω is the measure of the unit ball.