Hölder continuity up to the boundary

The second case of the Sobolev embedding at order k reads the Hölder exponent off Morrey's inequality at the exponent the ladder reaches, and states it on the closure of the domain. This file proves that statement.

The chain has three links. The ladder of EllipticPdes.Embedding.DomainLadder puts the member and its first derivatives in L^P(Ω) for a P above the dimension; EllipticPdes.Extension.exists_extension_subset_bound puts them on the whole space with the same bound; and morrey_ball on a ball containing the closure of the domain produces the continuous representative, whose Hölder seminorm is bounded by the L^P norms of the extended gradient. Restricting the representative to the closure of the domain is the last step, and it is where the conclusion reaches the boundary, which the interior statements of EllipticPdes.Embedding.HolderGeneral do not.

Supremum as well as seminorm

The C^{0,γ} norm of the cited statement is the supremum plus the Hölder seminorm, and Morrey supplies the seminorm alone. The supremum comes from the support clause of the extension: the extension vanishes outside a ball the closure of the domain sits inside, the representative is therefore zero somewhere in the larger ball Morrey runs on, and the estimate against that point bounds the representative everywhere by the seminorm times a power of the diameter. That power depends on the two radii and the exponent alone, so one constant states both halves.

Main declarations

• EllipticPdes.Embedding.exists_const_holderOnWith_of_gradClosed_domain: clause (ii) of the embedding on the closure of the domain, with a constant taken before the family.

References

James Guo, Partial Differential Equations (Course Lecture Notes), Theorem IV.2.3 case (ii); L. C. Evans, Partial Differential Equations (2nd ed.), §5.6.3 Theorem 6 clause (ii).

theorem EllipticPdes.Embedding.exists_const_holderOnWith_of_gradClosed_domain {d : ℕ} (hd : 1 < d) {Ω : Set (EuclideanSpace ℝ (Fin d))} (hΩopen : IsOpen Ω) (hΩb : Bornology.IsBounded Ω) (hC1 : Extension.HasC1Boundary Ω) (ι : Type u_1) {p₀ P : NNReal} (hp₀ : 1 ≤ p₀) {s : ℕ} (hsd : ↑p₀ * ↑s ≤ ↑d) (hp₀P : p₀ ≤ P) (hPd : ↑d < ↑P) (hPs : (↑p₀)⁻¹ - ↑s * (↑d)⁻¹ ≤ (↑P)⁻¹) : ∃ (C : NNReal), ∀ {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} {dep : ι → ℕ} {m : ℕ}, (∀ (i : ι) (k : Fin d), dep (nxt i k) ≤ dep i + 1) → (∀ (i : ι), dep i < m → HasWeakGradOn Ω (F i) fun (k : Fin d) => F (nxt i k)) → (∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) (↑p₀) (MeasureTheory.volume.restrict Ω)) → ∀ (M : NNReal), (∀ (j : ι), dep j ≤ m → MeasureTheory.eLpNorm (F j) (↑p₀) (MeasureTheory.volume.restrict Ω) ≤ ↑M) → ∀ (i : ι), dep i + 1 + s ≤ m → ∃ (w : EuclideanSpace ℝ (Fin d) → ℝ), w =ᵐ[MeasureTheory.volume.restrict Ω] F i ∧ (∀ y ∈ closure Ω, ‖w y‖ ≤ ↑(C * M)) ∧ HolderOnWith (C * M) (morreyExponent d ↑P) w (closure Ω)

Clause (ii) of the embedding on a bounded domain with C¹ boundary. One constant, depending on the domain, the dimension, the base exponent, the rung count and the landing exponent, bounds both the supremum and the Hölder seminorm on the closure of the domain of a representative of every member by a uniform L^{p₀} bound on the family. The Hölder exponent is Morrey's 1 - d/P, which EllipticPdes.Embedding.morreyExponent_eq_ladder identifies with the ⌊n/p⌋ + 1 - n/p of the cited statement at the landing exponent.