Classical derivatives up to the boundary

EllipticPdes.Embedding.exists_const_holderOnWith_of_gradClosed_domain produces a bounded Hölder representative of each member separately. u ∈ C^{k-1-⌊n/p⌋,γ}(closure Ω) says more: one function, differentiable to order k - 1 - ⌊n/p⌋ on Ω, whose derivatives are the members themselves and whose top derivatives are γ-Hölder on closure Ω. This file supplies that.

The representatives are chosen once, before any of them is read, so a single family v serves every index. Each v i is continuous on closure Ω, hence on Ω, and integrable there, and it has the weak gradient fun k => v (nxt i k) because a weak gradient sees only the almost-everywhere class. EllipticPdes.Embedding.hasFDerivAt_of_continuousOn_hasWeakGradOn then makes the weak gradient a classical one at every point of Ω, and an induction on the order remaining reads ContDiffOn off the chain.

The estimate is the one the clause states: the constant is quantified before the family, and it bounds the supremum and the Hölder seminorm of every member on closure Ω by a uniform L^{p₀} bound.

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_contDiffOn_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) → ∃ (v : ι → EuclideanSpace ℝ (Fin d) → ℝ), (∀ (i : ι), dep i + 1 + s ≤ m → v i =ᵐ[MeasureTheory.volume.restrict Ω] F i) ∧ (∀ (i : ι), dep i + 1 + s ≤ m → ∀ y ∈ closure Ω, ‖v i y‖ ≤ ↑(C * M)) ∧ (∀ (i : ι), dep i + 1 + s ≤ m → HolderOnWith (C * M) (morreyExponent d ↑P) (v i) (closure Ω)) ∧ (∀ (n : ℕ) (i : ι), dep i + n + 1 + s ≤ m → ContDiffOn ℝ (↑n) (v i) Ω) ∧ ∀ (i : ι), dep i + 2 + s ≤ m → ∀ y ∈ Ω, HasFDerivAt (v i) (gradCLM (fun (k : Fin d) => v (nxt i k)) y) y

Clause (ii) of the embedding with classical derivatives. One family of representatives serves every index: each is bounded and Hölder on closure Ω under the constant the clause names, each of low enough depth is differentiable on Ω with the next members as its partial derivatives, and each is n times continuously differentiable on Ω whenever the supply leaves n orders above it.