Hölder continuity at a general base exponent

EllipticPdes.Embedding.exists_holderOnWith_of_gradClosed runs the ladder from L² and reads the Hölder exponent off Morrey's inequality at the exponent the ladder reaches. Morrey is already stated for every exponent above the dimension, and the rung count and the landing exponent are already free there, so the base exponent is the only thing left at 2. This file frees it, which is the second case of Evans, Partial Differential Equations, §5.6.3 Theorem 6, and of Guo, Partial Differential Equations, Theorem IV.2.3, at the exponent each quantifies over.

Landing exponent

Running s rungs from p₀ lands at the reciprocal 1/p₀ - s/d, and Morrey at that exponent gives the Hölder exponent 1 - d/P = s + 1 - d/p₀. At s = ⌊d/p₀⌋ that is the ⌊n/p⌋ + 1 - n/p of the cited statements. When d/p₀ is an integer the reciprocal reaches 0, the ladder reaches every finite exponent, and the Hölder exponent is free in (0,1), which is the other case those statements separate out.

Main declarations

• EllipticPdes.Embedding.exists_holderOnWith_of_gradClosed_general: the Hölder clause at a general base exponent.
• EllipticPdes.Embedding.morreyExponent_eq_ladder: the exponent it lands on is the one the cited statements name.

References

Evans, Partial Differential Equations (2nd ed.), §5.6.3 Theorem 6 clause (ii). Guo, Partial Differential Equations, Theorem IV.2.3 case (ii).

theorem EllipticPdes.Embedding.exists_holderOnWith_of_gradClosed_general {d : ℕ} (hd : 1 < d) (c : EuclideanSpace ℝ (Fin d)) {r R : ℝ} (hr : 0 < r) (hrR : r < R) {ι : Type u_1} {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} {dep : ι → ℕ} {m : ℕ} {p₀ : NNReal} (hp₀ : 1 ≤ p₀) (hdep : ∀ (i : ι) (k : Fin d), dep (nxt i k) ≤ dep i + 1) (hgrad : ∀ (i : ι), dep i < m → HasWeakGradOn (Metric.ball c R) (F i) fun (k : Fin d) => F (nxt i k)) (hmem : ∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) (↑p₀) (MeasureTheory.volume.restrict (Metric.ball c R))) {s : ℕ} {P : NNReal} (hsd : ↑p₀ * ↑s ≤ ↑d) (hp₀P : p₀ ≤ P) (hPd : ↑d < ↑P) (hPs : (↑p₀)⁻¹ - ↑s * (↑d)⁻¹ ≤ (↑P)⁻¹) (i : ι) (hi : dep i + 1 + s ≤ m) : ∃ (w : EuclideanSpace ℝ (Fin d) → ℝ), w =ᵐ[MeasureTheory.volume.restrict (Metric.ball c r)] F i ∧ ∃ (M : NNReal), HolderOnWith M (morreyExponent d ↑P) w (Metric.ball c r)

Hölder clause at a general base exponent. The ladder run for s rungs from L^{p₀} lands at any P the reciprocal relation 1/p₀ - s/d ≤ 1/P admits, and Morrey at P > d reads off the exponent 1 - d/P.

theorem EllipticPdes.Embedding.morreyExponent_eq_ladder {d : ℕ} (hd : 0 < d) {p₀ P : NNReal} {s : ℕ} (hp₀ : 0 < ↑p₀) (hPd : ↑d ≤ ↑P) (hP : (↑P)⁻¹ = (↑p₀)⁻¹ - ↑s * (↑d)⁻¹) : ↑(morreyExponent d ↑P) = ↑s + 1 - ↑d / ↑p₀

Agreement of the ladder's exponent with the cited one. At the landing reciprocal 1/P = 1/p₀ - s/d, Morrey's exponent is s + 1 - d/p₀, which at s = ⌊d/p₀⌋ is the ⌊n/p⌋ + 1 - n/p of Evans §5.6.3 Theorem 6 and Guo Theorem IV.2.3.