Documentation

TauCeti.Analysis.PDE.Regularity.DivergenceFormSchauder

Schauder estimates for divergence-form equations with Hölder coefficients #

Let u ∈ H¹(Ω) be a weak solution of the divergence-form equation

-∂ᵢ(aⁱʲ ∂ⱼu) = -div G in an open set Ω ⊆ ℝ^{n+1},

that is ∫_Ω ⟨a ∇u, ∇φ⟩ = ∫_Ω ⟨G, ∇φ⟩ for every test function φ, with a variable coefficient matrix a and a vector field G, and let 0 < α < 1. This file proves the interior Schauder estimate: if the open R-thickening of a set S lies in Ω, a is uniformly elliptic with constants λ, Λ at the points of S, and a and G are α-Hölder on the thickening with constants K_a and K_G, then the precise representative of ∇u is α-Hölder on S with constant

C (K_G + R^{-(n+1)/2-α} ‖∇u‖_{L²(Ω)}),

where C depends only on n, α, λ, Λ and a bound M ≥ R^α K_a. Hölder continuity of the coefficients is measured in the operator norm of the attached bilinear forms TauCeti.PDE.matrixBilinearForm. The constant is invariant under dilations, since R^α K_a is. For the Laplacian, a = 1, the estimate is TauCeti.PDE.exists_holderOnWith_preciseRepresentative_gradient.

The argument #

The proof is Campanato's, by comparison with the problem frozen at the centre of each ball. Fix a centre z ∈ S and write Φ(t) = ∫_{B_t} ‖∇u‖² and ψ(t) = ∫_{B_t} ‖∇u - (∇u)_{B_t}‖² for the balls B_t = ball z t. On B_r let w solve -∂ᵢ(a(z)ⁱʲ ∂ⱼw) = 0 with the boundary values of u. Its energy distance from u is O(r^{2α} (K_a² Φ(r) + K_G² r^{n+1})) (TauCeti.PDE.UniformlyEllipticOn.exists_frozen_setIntegral_norm_gradient_sub_sq_le), while Φ and ψ decay for w with exponents n + 1 and n + 3 (TauCeti.PDE.setIntegral_ball_norm_gradient_sq_le_of_forall_energyFormH1_eq_zero and TauCeti.PDE.setIntegral_ball_norm_gradient_sub_setAverage_sq_le_of_forall_energyFormH1_eq_zero). Transferring this decay to u (TauCeti.PDE.setIntegral_norm_gradient_sq_le_add_of_frozen and TauCeti.PDE.setIntegral_norm_gradient_sub_setAverage_sq_le_add_of_frozen) gives, for 0 < ρ ≤ r,

Φ(ρ) ≤ A ((ρ / r)^{n+1} + r^{2α} K_a² / λ²) Φ(r) + A K_G² r^{n+1+2α} / λ², ψ(ρ) ≤ A (ρ / r)^{n+3} ψ(r) + A r^{2α} (K_a² Φ(r) + K_G² r^{n+1}) / λ².

The coefficient oscillation r^{2α} K_a² is not small on B_R itself, only on B_{θR} for a small θ, depending on M. There the iteration lemma TauCeti.exists_le_mul_div_rpow_mul_add_mul_rpow_of_le_mul_add turns the two inequalities into decay estimates in four steps:

  1. Morrey decay Φ(t) ≲ (t / R)^{n+1-α}, from the first inequality, where the coefficient term is a small perturbation.
  2. Campanato decay ψ(t) ≲ (t / R)^{n+1+α}, from the second inequality and step 1.
  3. Morrey decay Φ(t) ≲ (t / R)^{n+1}: by step 2 and Campanato's theorem the averages of ∇u over the balls B_t stay bounded.
  4. Campanato decay ψ(t) ≲ (t / R)^{n+1+2α}, from the second inequality and step 3. This needs α < 1.

By Jensen's inequality, step 4 bounds the mean oscillation of ∇u on balls of radius t by a multiple of t^α, and the local form of Campanato's theorem (TauCeti.MeasureTheory.holderOnWith_preciseRepresentative_of_setAverage_norm_sub_le) gives the Hölder estimate.

Main declarations #

References #

theorem TauCeti.PDE.exists_holderOnWith_preciseRepresentative_gradient_of_holderOnWith_matrixBilinearForm {n : ℕ} {α : NNReal} (hα : 0 < α) (hα1 : α < 1) {lam Lam M : ℝ} :
∃ (C : ℝ), 0 ≤ C ∧ ∀ {Omega : TopologicalSpace.Opens (EuclideanSpace ℝ (Fin (n + 1)))} {u : ↥(W1p MeasureTheory.volume Omega 2)} {a : EuclideanSpace ℝ (Fin (n + 1)) → Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ} {G : EuclideanSpace ℝ (Fin (n + 1)) → EuclideanSpace ℝ (Fin (n + 1))} {Ka KG : NNReal} {S : Set (EuclideanSpace ℝ (Fin (n + 1)))} {R : ℝ}, UniformlyEllipticOn S a lam Lam → HolderOnWith Ka α (fun (x : EuclideanSpace ℝ (Fin (n + 1))) => matrixBilinearForm (a x)) (Metric.thickening R S) → HolderOnWith KG α G (Metric.thickening R S) → ↑Ka * R ^ ↑α ≤ M → (∀ (φ : TestFunction Omega ℝ ⊤), energyFormH1 a 0 0 u ((W1p.ofTestFunctionₗ MeasureTheory.volume Omega 2) φ) = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in ↑Omega, inner ℝ (G x) (gradient (⇑φ) x)) → 0 < R → Metric.thickening R S ⊆ ↑Omega → HolderOnWith (C * (↑KG + R ^ (-((↑n + 1) / 2 + ↑α)) * ‖W1p.gradient u‖)).toNNReal α (MeasureTheory.preciseRepresentative MeasureTheory.volume ↑↑(W1p.gradient u)) S

Interior Schauder estimate for divergence-form equations with Hölder coefficients. Let 0 < α < 1. There is a constant C, depending only on n, α, λ, Λ and M, such that the following holds. Let Ω ⊆ ℝ^{n+1} be open and let u ∈ H¹(Ω) be a weak solution of -∂ᵢ(aⁱʲ ∂ⱼu) = -div G in Ω, that is ∫_Ω ⟨a ∇u, ∇φ⟩ = ∫_Ω ⟨G, ∇φ⟩ for every test function φ. Let S be a set whose open R-thickening lies in Ω, let a be uniformly elliptic with constants λ, Λ at the points of S, and let a and G be α-Hölder on the R-thickening of S with constants K_a and K_G, the oscillation of a measured in the operator norm of the attached bilinear forms, where K_a R^α ≤ M. Then the precise representative of ∇u is α-Hölder on S, with constant C (K_G + R^{-(n+1)/2-α} ‖∇u‖_{L²(Ω)}).

The constant depends on the coefficients only through λ, Λ and the dimensionless bound M on R^α [a]_α, so the estimate is invariant under dilations. The precise representative agrees with ∇u almost everywhere on Ω (TauCeti.MeasureTheory.ae_eq_restrict_preciseRepresentative). For a = 1 this is TauCeti.PDE.exists_holderOnWith_preciseRepresentative_gradient.