Interior C^{k,1/2} estimate for the weak solution, in every dimension

EllipticPdes.Regularity.exists_contDiffOn_holder_ball is case (ii) of Guo's embedding (Theorem IV.2.3) at p = 2: m orders of weak derivative on V give a C^{k,1/2} representative on a ball whenever k + 1 + ⌊d/2⌋ ≤ m. It is stated over an abstract supply of weak derivatives, which is what the iterated Sobolev ladder EllipticPdes.Embedding.memLp_of_gradClosed_fullStep consumes: ⌊d/2⌋ rungs of the full step 1/d, one weak derivative each.

This file discharges that supply from the equation. EllipticPdes.Regularity.higher_interior_regularity at order j gives j + 2 orders of weak derivative of the solution on any compact V ⊆ Ω, so running it at j = k + 1 + ⌊d/2⌋ covers the Guo condition with room to spare, and the composition is the interior C^{k,1/2} estimate for the weak solution itself, in every dimension and at every finite order k.

EllipticPdes.Regularity.interior_smooth is the same composition run at every order at once, and concludes C^∞ on the interior of V. The finite-order statement here asks finitely much of the coefficients and of the datum, and adds the Hölder seminorm bound, which the C^∞ statement drops.

Main declarations

• EllipticPdes.Regularity.interior_holder_of_weakSolution: the interior C^{k,1/2} estimate for the weak solution, in every dimension.

References

James Guo, Partial Differential Equations, Theorem IV.2.3(ii); L. C. Evans, Partial Differential Equations (2nd ed.), §6.3.1.

theorem EllipticPdes.Regularity.interior_holder_of_weakSolution {n : ℕ} (Op : Sobolev.FullEllipticOp (n + 1)) {Ω : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hΩm : MeasurableSet Ω) (hΩo : IsOpen Ω) (hA1 : IsLipCoeff Op.toEllipticCoeff) (k : ℕ) (hA : IsWkInftyCoeff Op.toEllipticCoeff (k + 1 + (n + 1) / 2 + 3)) (hbc : IsWkInftyLower Op (k + 1 + (n + 1) / 2 + 2)) (u : ↥(Sobolev.H01 Ω)) (f : Sobolev.L2D Ω) (M : ℝ) (hfk : HasIteratedWeakDerivOn Ω (k + 1 + (n + 1) / 2) f) (hM : IteratedL2Bound hfk M) (hweak : ∀ (w : ↥(Sobolev.H01 Ω)), ((Op.fullBilin Ω) u) w = ∫ (x : EuclideanSpace ℝ (Fin (n + 1))) in Ω, ↑↑f x * ↑↑((↑w).ofLp 0) x) {V : Set (EuclideanSpace ℝ (Fin (n + 1)))} (hVc : IsCompact V) (hVΩ : V ⊆ Ω) {c : EuclideanSpace ℝ (Fin (n + 1))} {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hBV : Metric.ball c R ⊆ V) : ∃ (w : EuclideanSpace ℝ (Fin (n + 1)) → ℝ), w =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] ↑↑((extendL2 hΩm) ((↑u).ofLp 0)) ∧ ContDiffOn ℝ (↑k) w (Metric.ball c r) ∧ ∃ (Mh : NNReal), HolderOnWith Mh (1 / 2) w (Metric.ball c r)

Interior C^{k,1/2} regularity of the weak solution in every dimension. With coefficients of enough W^{k,∞} regularity and a datum with enough weak derivatives, the weak solution of L u = f has a representative on every interior ball that is C^k there and whose k-th derivatives are Hölder of exponent 1/2.

The order asked of the datum and the coefficients is the Guo threshold k + 1 + ⌊d/2⌋ plus the two orders higher_interior_regularity supplies from the equation, so the dimension enters the hypotheses and not the conclusion.