Hölder continuity of the second derivatives for -Δu = f

Let u ∈ H¹(Ω) be a weak solution of Poisson's equation -Δu = f in an open set Ω ⊆ ℝ^{n+1}, with f ∈ L²(Ω), and let 0 < α < 1. This file proves that the second derivatives of u are as regular as f in the interior: if f is α-Hölder with constant K on the open R-thickening S_R of a set S, and S_R lies in an open V whose closure is compact and contained in Ω, then for every direction e the weak derivative ∂ₑu ∈ H¹(V) has a gradient whose precise representative is α-Hölder on S, with constant

C (‖e‖ K + R^{-(n+1)/2-α} ‖∇∂ₑu‖_{L²(V)}),

where C depends only on n and α, and ‖∇∂ₑu‖_{L²(V)} is finite by interior H² regularity. Applied along an orthonormal basis, this says that the second derivatives of u are α-Hölder on S: the interior C^{2,α} regularity of Poisson's equation with Hölder data.

Differentiating the equation

Interior H² regularity (TauCeti.PDE.UniformlyEllipticOn.exists_lowerOrder_eq_restrictL) puts u in H²(V), so w = ∂ₑu lies in H¹(V). The data f need not be weakly differentiable, so w is not a weak solution of -Δw = ∂ₑf; instead the derivative is kept on the test function. For a test function φ on V, moving ∂ₑ across the energy form (TauCeti.PDE.energyFormH1_ofTestFunctionₗ_eq_neg_of_hasWeakLineDerivOn) and using the equation for u against ∂ₑφ gives

∫_V ⟨∇w, ∇φ⟩ = -∫_V ⟨∇u, ∇∂ₑφ⟩ = -∫_V f ∂ₑφ = ∫_V ⟨-f e, ∇φ⟩,

so w solves -Δw = -div G in V with the field G = -f e, which is α-Hölder on S_R with constant ‖e‖ K. The interior Hölder estimate for the gradient (TauCeti.PDE.exists_holderOnWith_preciseRepresentative_gradient) then applies to w.

Main declarations

• TauCeti.PDE.exists_hasWeakLineDerivOn_and_holderOnWith_preciseRepresentative_gradient: the interior Hölder estimate for the second derivatives of a weak solution of -Δu = f.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 4.6.
• M. Giaquinta, L. Martinazzi, An Introduction to the Regularity Theory for Elliptic Systems, Harmonic Maps and Minimal Graphs, 2nd ed., Chapter 5.

theorem TauCeti.PDE.exists_hasWeakLineDerivOn_and_holderOnWith_preciseRepresentative_gradient {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {Omega V : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin (n + 1)))} {u : ↥(W1p MeasureTheory.volume Omega 2)} {f : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {K : NNReal} {S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {R : ℝ}, MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict ↑Omega) → (∀ (v : ↥(W1p0 MeasureTheory.volume Omega 2)), energyFormH1 (fun (x : EuclideanSpace ℝ (Fin (n + 1))) => 1) 0 0 u ↑v = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in ↑Omega, f x * ↑↑(W1p.value ↑v) x) → IsCompact (closure ↑V) → closure ↑V ⊆ ↑Omega → HolderOnWith K α f (Metric.thickening R S) → 0 < R → Metric.thickening R S ⊆ ↑V → ∀ (e : EuclideanSpace ℝ (Fin (n + 1))), ∃ (d : ↥(W1p MeasureTheory.volume V 2)), HasWeakLineDerivOn MeasureTheory.volume V (↑↑(W1p.value u)) (↑↑(W1p.value d)) e ∧ HolderOnWith (C * (‖e‖ * ↑K + R ^ (-((↑n + 1) / 2 + ↑α)) * ‖W1p.gradient d‖)).toNNReal α (MeasureTheory.preciseRepresentative MeasureTheory.volume ↑↑(W1p.gradient d)) S

Interior Hölder continuity of the second derivatives for -Δu = f. Let 0 < α < 1. There is a constant C, depending only on n and α, such that the following holds. Let Ω ⊆ ℝ^{n+1} be open, f ∈ L²(Ω), and let u ∈ H¹(Ω) be a weak solution of -Δu = f in Ω, that is ∫_Ω ⟨∇u, ∇v⟩ = ∫_Ω f v for every v ∈ H¹₀(Ω). Let V be open with compact closure contained in Ω, and suppose that the open R-thickening of S lies in V and that f is α-Hölder there with constant K. Then for every direction e, the weak derivative ∂ₑu lies in H¹(V), and the precise representative of its gradient is α-Hölder on S, with constant C (‖e‖ K + R^{-(n+1)/2-α} ‖∇∂ₑu‖_{L²(V)}).

No boundary condition is imposed on u and nothing is assumed about ∂Ω. The precise representative agrees with ∇∂ₑu almost everywhere on V (TauCeti.MeasureTheory.ae_eq_restrict_preciseRepresentative).