Interior Schauder estimates for classical solutions

Let 0 < α < 1, and let A be a constant (n + 1) × (n + 1) matrix with λ ‖ξ‖² ≤ ξᵀ A ξ ≤ Λ ‖ξ‖² and 0 < λ. This file proves the interior C^{2,α} estimate for classical solutions of ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = f: if u is C² on an open set containing the closed R-thickening of a bounded set S ⊆ ℝ^{n+1}, and f is α-Hölder with constant K on the open R-thickening S_R, then D²u is α-Hölder on S, with constant

C (Λ / λ)^(1 + (n + 1) / 4 + α / 2) (K / λ + R^{-(n+1)/2-α} ‖D²u‖_{L²(S_R)}),

where C depends only on n and α. The matrix enters only through λ and Λ, uniformly over all matrices with these ellipticity constants. This is the estimate for the frozen operator in the perturbation argument for equations with Hölder continuous coefficients, where the coefficients are frozen at a point of each small ball. The lower-order term is the L² norm of D²u on the thickening, as in Campanato's approach, rather than the supremum of u.

The argument

For the Laplacian, u lies in H¹(W) for an open W ⊇ closure S_R with compact closure in the domain, and Green's identity (TauCeti.PDE.energyFormH1_one_zero_zero_eq_setIntegral_neg_laplacian_mul) makes it a weak solution of -Δu = -Δu against H¹₀(W). The interior Hölder estimate for weak solutions (TauCeti.PDE.exists_hasWeakLineDerivOn_and_holderOnWith_preciseRepresentative_gradient) then bounds the precise representative of the weak gradient of each weak derivative ∂ᵢu. For a C² function the weak derivative is the classical one and the precise representative of a continuous function is the function itself, so ∇∂ᵢu is α-Hölder on S. Summing over the coordinate directions (TauCeti.norm_iteratedFDeriv_two_sub_le_sum) gives the estimate for D²u.

For a general A, there is a linear automorphism e with ‖e‖ ≤ √Λ, ‖e⁻¹‖ ≤ 1 / √λ and Δ (u ∘ e) = (∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu) ∘ e (TauCeti.PDE.exists_continuousLinearEquiv_laplacian_comp_eq). The estimate for the Laplacian applies to v = u ∘ e on the (R / √Λ)-thickening of e⁻¹ S, where Δv is α-Hölder with constant K Λ^(α/2). Changing variables, ‖D²v‖_{L²} ≤ Λ |det e|^(-1/2) ‖D²u‖_{L²(S_R)}, and |det e⁻¹| ≤ ‖e⁻¹‖^(n+1) (ContinuousLinearMap.abs_det_le_opNorm_pow). Finally D²u = D²v ∘ e⁻¹ precomposed with e⁻¹ in both slots, which costs the factor ‖e⁻¹‖^(2+α) ≤ λ^(-1-α/2) (ContinuousLinearEquiv.holderOnWith_iteratedFDeriv_of_comp_right).

Main declarations

• TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_laplacian: the interior Schauder estimate for C² solutions of Poisson's equation.
• TauCeti.PDE.exists_mem_nhds_holderOnWith_iteratedFDeriv_two_of_laplacian: a C² function with locally α-Hölder Laplacian has locally α-Hölder second derivatives.
• TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv: the interior Schauder estimate for C² solutions of ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu = f, with explicit dependence on λ and Λ.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 4.6 and Lemma 6.1 (reduction of a constant-coefficient operator to the Laplacian by a linear change of variables).
• 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_holderOnWith_iteratedFDeriv_two_of_laplacian {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {U S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {K : NNReal} {R : ℝ}, IsOpen U → ContDiffOn ℝ 2 u U → Bornology.IsBounded S → 0 < R → Metric.cthickening R S ⊆ U → HolderOnWith K α (Laplacian.laplacian u) (Metric.thickening R S) → HolderOnWith (C * (↑K + R ^ (-((↑n + 1) / 2 + ↑α)) * (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2 (MeasureTheory.volume.restrict (Metric.thickening R S))).toReal)).toNNReal α (iteratedFDeriv ℝ 2 u) S

Interior Schauder estimate for Poisson's equation, classical form. Let 0 < α < 1. There is a constant C, depending only on n and α, such that the following holds. Let u be of class C² on an open set U ⊆ ℝ^{n+1}, let S be bounded, R > 0, and suppose that the closed R-thickening of S lies in U and that Δu is α-Hölder with constant K on the open R-thickening S_R. Then the second derivative D²u is α-Hölder on S, with constant

C (K + R^{-(n+1)/2-α} ‖D²u‖_{L²(S_R)}).

theorem TauCeti.PDE.exists_mem_nhds_holderOnWith_iteratedFDeriv_two_of_laplacian {n : ℕ} {α : NNReal} (hα1 : α < 1) {U : Set (EuclideanSpace ℝ (Fin (n + 1)))} {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (hU : IsOpen U) (hu : ContDiffOn ℝ 2 u U) (hΔ : ∀ x ∈ U, ∃ T ∈ nhds x, ∃ (K : NNReal), HolderOnWith K α (Laplacian.laplacian u) T) {x : EuclideanSpace ℝ (Fin (n + 1))} (hx : x ∈ U) : ∃ T ∈ nhds x, ∃ (K : NNReal), HolderOnWith K α (iteratedFDeriv ℝ 2 u) T

Local C^{2,α} regularity for Poisson's equation. Let 0 ≤ α < 1, and let u be of class C² on an open set U ⊆ ℝ^{n+1} whose Laplacian is locally α-Hölder on U. Then D²u is locally α-Hölder on U: every point of U has a neighbourhood on which D²u is α-Hölder.

theorem TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {lam Lam : ℝ}, 0 < lam → (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ A.toQuadraticForm' ξ.ofLp) → (∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), A.toQuadraticForm' ξ.ofLp ≤ Lam * ‖ξ‖ ^ 2) → ∀ {U S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {K : NNReal} {R : ℝ}, IsOpen U → ContDiffOn ℝ 2 u U → Bornology.IsBounded S → 0 < R → Metric.cthickening R S ⊆ U → HolderOnWith K α (fun (x : EuclideanSpace ℝ (Fin (n + 1))) => ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), A i j • ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)) (Metric.thickening R S) → HolderOnWith (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2) * (↑K / lam + R ^ (-((↑n + 1) / 2 + ↑α)) * (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2 (MeasureTheory.volume.restrict (Metric.thickening R S))).toReal)).toNNReal α (iteratedFDeriv ℝ 2 u) S

Interior Schauder estimate for constant-coefficient operators, classical form. Let 0 < α < 1. There is a constant C, depending only on n and α, such that the following holds. Let A be a matrix with λ ‖ξ‖² ≤ ξᵀ A ξ ≤ Λ ‖ξ‖² and 0 < λ, let u be of class C² on an open set U ⊆ ℝ^{n+1}, let S be bounded, R > 0, and suppose that the closed R-thickening of S lies in U and that ∑ᵢⱼ Aᵢⱼ ∂ᵢ∂ⱼu is α-Hölder with constant K on the open R-thickening S_R. Then D²u is α-Hölder on S, with constant

C (Λ / λ)^(1 + (n + 1) / 4 + α / 2) (K / λ + R^{-(n+1)/2-α} ‖D²u‖_{L²(S_R)}).