Schauder estimates with lower-order terms

Let 0 < α < 1. This file extends the interior and the whole-space Schauder estimates for ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu to the general second-order operator in non-divergence form

L u = ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu + b · ∇u + c u,

with a drift b : ℝ^{n+1} → ℝ^{n+1} and a potential c, both α-Hölder. The drift term is written fderiv ℝ u x (b x), as in the maximum principles for operators with lower-order terms. No sign condition on c is needed for the estimates.

• The interior estimate, exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul, on a compact set K inside an open set Ω. If a, b and c are α-Hölder on a ball around each point of K and a is elliptic at each point of K, there is a constant C such that every u that is C² on Ω satisfies [D²u]_{α; K} ≤ C ([L u]_{α; Ω} + N), where N bounds |u|, ‖Du‖ and ‖D²u‖ on Ω.
• The global estimate, exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul, on the whole space. For uniformly elliptic a and globally Hölder and bounded a, b and c, the Hölder constant of D²u and the bounds of Du and D²u are at most C ([L u]_α + ‖u‖_∞), with C depending only on n, α, the ellipticity constants and the bounds on the coefficients.

The argument

The lower-order part b · ∇u + c u is moved to the right side: u solves ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu = L u - b · ∇u - c u, and the Hölder constant of b · ∇u + c u is bounded by products of the sup norms and the Hölder constants of the factors (ContinuousLinearMap.holderOnWith_comp₂). The functions u and Du are bounded, with derivatives bounded by the bounds on Du and D²u, so they are α-Hölder (TauCeti.holderOnWith_thickening_of_norm_fderiv_le, TauCeti.holderWith_of_norm_le_of_norm_fderiv_le).

In the interior estimate the principal-part estimate (TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_of_holderOnWith) is applied on a thickening U of K. It is chosen so thin that the ball of the same radius about each point of U stays in Ω, which makes u and Du Lipschitz between nearby points of U, and so that the local Hölder bounds on b and c become uniform on U (IsCompact.exists_holderOnWith_thickening_and_norm_le). All lower-order quantities are then bounded by multiples of N.

On the whole space only ‖u‖_∞ is allowed on the right, so the bounds of Du and D²u entering through the lower-order terms are removed by the interpolation inequalities ‖Du‖_∞, ‖D²u‖_∞ ≤ C_ε ‖u‖_∞ + 2 ε^α [D²u]_α (HolderWith.norm_iteratedFDeriv_succ_le_and_norm_iteratedFDeriv_add_two_le), and the resulting multiple of [D²u]_α is absorbed into the global principal-part estimate (TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv) for small ε.

References

• D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Chapter 6, Theorem 6.2 and the proof of Theorem 6.6 (lower-order terms by interpolation).
• N. V. Krylov, Lectures on Elliptic and Parabolic Equations in Hölder Spaces, Graduate Studies in Mathematics 12, AMS, 1996, Chapter 4 (a priori estimates in the whole space).

theorem TauCeti.PDE.exists_holderOnWith_iteratedFDeriv_two_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) {Ω K : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩ : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω) {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {b : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))} {c : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} (ha : ∀ x ∈ K, ∃ r > 0, ∃ (L : NNReal), ∀ (i j : Fin (n + 1)), HolderOnWith L α (fun (y : EuclideanSpace ℝ (Fin (n + 1))) => a y i j) (Metric.ball x r)) (hb : ∀ x ∈ K, ∃ r > 0, ∃ (L : NNReal), HolderOnWith L α b (Metric.ball x r)) (hc : ∀ x ∈ K, ∃ r > 0, ∃ (L : NNReal), HolderOnWith L α c (Metric.ball x r)) (hell : ∀ x ∈ K, ∃ (lam : ℝ), 0 < lam ∧ ∀ (ξ : EuclideanSpace ℝ (Fin (n + 1))), lam * ‖ξ‖ ^ 2 ≤ (a x).toQuadraticForm' ξ.ofLp) : ∃ (C : NNReal), ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N M : NNReal}, ContDiffOn ℝ 2 u Ω → (∀ x ∈ Ω, |u x| ≤ ↑N) → (∀ x ∈ Ω, ‖fderiv ℝ u x‖ ≤ ↑N) → (∀ x ∈ Ω, ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑N) → (∀ S ⊆ Ω, IsCompact S → ∃ (V : NNReal), HolderOnWith V α (iteratedFDeriv ℝ 2 u) S) → HolderOnWith M α (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) + (fderiv ℝ u x) (b x) + c x * u x) Ω → HolderOnWith (C * (M + N)) α (iteratedFDeriv ℝ 2 u) K

The interior Schauder estimate with lower-order terms. Let 0 < α < 1, let Ω ⊆ ℝ^{n+1} be open and K ⊆ Ω compact. Let a be a matrix-valued coefficient, b a vector field and c a function, each α-Hölder on a ball around each x ∈ K, with a x elliptic at each x ∈ K, that is, λₓ ‖ξ‖² ≤ ξᵀ a(x) ξ for some λₓ > 0. Put L u = ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu + b · ∇u + c u. Then there is a constant C, depending on a, b, c, K and Ω but not on u, with the following property. Let u be C² on Ω, with |u|, ‖Du‖ and ‖D²u‖ bounded by N on Ω and with D²u α-Hölder on every compact subset of Ω (with any constants). If L u is α-Hölder on Ω with constant M, then D²u is α-Hölder on K with constant C (M + N).

theorem TauCeti.PDE.exists_holderWith_iteratedFDeriv_two_and_norm_le_of_sum_smul_fderiv_fderiv_add_fderiv_add_mul {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) (lam Lam : ℝ) (L B : NNReal) : ∃ (C : NNReal), ∀ {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {b : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))} {c : EuclideanSpace ℝ (Fin (n + 1)) → ℝ}, UniformlyEllipticOn Set.univ a lam Lam → (∀ (i j : Fin (n + 1)), HolderWith L α fun (x : EuclideanSpace ℝ (Fin (n + 1))) => a x i j) → HolderWith L α b → (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖b x‖ ≤ ↑B) → HolderWith L α c → (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |c x| ≤ ↑B) → ∀ {u : EuclideanSpace ℝ (Fin (n + 1)) → ℝ} {N K : NNReal}, ContDiff ℝ 2 u → (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), |u x| ≤ ↑N) → BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin (n + 1))) => ‖iteratedFDeriv ℝ 2 u x‖) → MemHolder α (iteratedFDeriv ℝ 2 u) → (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) + (fderiv ℝ u x) (b x) + c x * u x) → HolderWith (C * (K + N)) α (iteratedFDeriv ℝ 2 u) ∧ (∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖fderiv ℝ u x‖ ≤ ↑C * (↑K + ↑N)) ∧ ∀ (x : EuclideanSpace ℝ (Fin (n + 1))), ‖iteratedFDeriv ℝ 2 u x‖ ≤ ↑C * (↑K + ↑N)

The global Schauder estimate with lower-order terms on the whole space. Let 0 < α < 1, and let λ, Λ, L and B be given. Then there is a constant C, depending only on n, α, λ, Λ, L and B, with the following property. Let a be a matrix-valued coefficient on ℝ^{n+1} which is uniformly elliptic and bounded with constants 0 < λ ≤ Λ (UniformlyEllipticOn univ a λ Λ) and globally α-Hölder entrywise with constant L, and let b be a vector field and c a function, both globally α-Hölder with constant L and bounded by B. Put L u = ∑ᵢⱼ aᵢⱼ ∂ᵢ∂ⱼu + b · ∇u + c u. Let u be C² with |u| ≤ N, and with D²u bounded and globally α-Hölder (with any constant). If L u is globally α-Hölder with constant K, then D²u is globally α-Hölder with constant C (K + N), and ‖Du‖ and ‖D²u‖ are bounded by C (K + N).