Schauder estimates for coefficients of small oscillation

This file proves a global a priori Schauder estimate for a non-divergence-form operator with Hölder coefficients close to a constant elliptic matrix. The solution is assumed C², with a globally Hölder Hessian in L². The resulting Hölder constant depends only on the forcing, the L² Hessian, the coefficient bounds and the chosen scale; its initial Hölder constant is absorbed. Compactly supported C^{2,α} functions are an important application.

The scale condition combines the uniform oscillation ε with L r^α, where L bounds the coefficient Hölder constants. Thus an arbitrary finite L is allowed by taking r sufficiently small, provided the uniform oscillation is strictly below the perturbation threshold. This is the global estimate used after applying an interior cutoff; localization and covering are separate from the estimate here.

The proof freezes the coefficients, uses TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv, and absorbs the Hölder norm of the Hessian. The pointwise interpolation estimate is the arbitrary-scale form of HolderWith.enorm_le_add_eLpNorm.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 6, proof of the interior Schauder estimate by freezing coefficients.

theorem TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_abs_sub_le {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) → ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {ε L K : NNReal} {r : ℝ}, 0 < r → 2 * (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2)) * (↑n + 1) ^ 2 * (↑ε + ↑L * r ^ ↑α) ≤ lam → (∀ (x : EuclideanSpace ℝ (Fin (n + 1))) (i j : Fin (n + 1)), |a x i j - A i j| ≤ ↑ε) → (∀ (i j : Fin (n + 1)), HolderWith L α fun (x : EuclideanSpace ℝ (Fin (n + 1))) => a x i j) → ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}, ContDiff ℝ 2 u → MemHolder α (iteratedFDeriv ℝ 2 u) → MeasureTheory.MemLp (iteratedFDeriv ℝ 2 u) 2 MeasureTheory.volume → (HolderWith K α fun (x : EuclideanSpace ℝ (Fin (n + 1))) => ∑ i : Fin (n + 1), ∑ j : Fin (n + 1), a x i j • ((fderiv ℝ (fderiv ℝ u) x) (EuclideanSpace.single i 1)) (EuclideanSpace.single j 1)) → HolderWith (2 * (C * (Lam / lam) ^ (1 + (↑n + 1) / 4 + ↑α / 2)) * (↑K / lam + ((↑n + 1) ^ 2 * ↑L / lam * (MeasureTheory.volume (Metric.ball 0 r) ^ (-2⁻¹)).toReal + r ^ (-((↑n + 1) / 2 + ↑α))) * (MeasureTheory.eLpNorm (iteratedFDeriv ℝ 2 u) 2 MeasureTheory.volume).toReal)).toNNReal α (iteratedFDeriv ℝ 2 u)

Global a priori Schauder estimate for coefficients of small oscillation. For 0 < α < 1 there is C > 0, depending only on dimension and α, with the following property. Put κ = C (Λ / λ)^(1 + (n+1)/4 + α/2). Let A have ellipticity bounds λ, Λ, with λ > 0, and assume every coefficient entry is globally α-Hölder with constant L and within ε of the corresponding entry of A. If

2 κ (n+1)² (ε + L r^α) ≤ λ,

then a global C² function with globally α-Hölder Hessian H ∈ L² satisfies

[H]_α ≤ 2 κ ([Lu]_α / λ + ((n+1)² L / λ |B_r|^(-1/2) + r^(-(n+1)/2-α)) ‖H‖₂).

The Hölder hypothesis on the Hessian is an a priori regularity assumption; its constant does not occur in the conclusion. No compact-support or boundary hypothesis is imposed.