Morrey's embedding for `W^{1,p}(ℝⁿ)` #

Let E be a finite-dimensional real inner product space of dimension n, with an additive Haar measure μ, and let n < p < ∞. This file proves Morrey's embedding on the whole space: every u ∈ W^{1,p}(ℝⁿ) has a representative which is Hölder continuous of exponent 1 - n / p,

‖u x - u y‖ ≤ C(n, p, μ) * ‖x - y‖ ^ (1 - n / p) * ‖∇u‖_{Lᵖ},

with the explicit constant of Morrey's inequality for C¹ functions (TauCeti.holderWith_of_contDiff_of_finrank_lt): writing ω = μ(B(0, 1)) and K = n ω (p - 1) / (p - n), it is C = 2 ^ (n + 1) / (n ω) * K ^ (1 - 1 / p) * 2 ^ (1 - n / p). Only the gradient enters the Hölder constant, as it must: adding a constant to u changes nothing on the right-hand side.

The argument #

Test functions are dense in W^{1,p}(ℝⁿ) (TauCeti.W1p.denseRange_ofTestFunctionₗ_top), so u is the Sobolev limit of test functions φₖ. Each φₖ satisfies Morrey's inequality with its own gradient norm, and these norms converge to ‖∇u‖_{Lᵖ}. Convergence in Lᵖ gives a subsequence converging to u almost everywhere, so the Hölder inequality passes to the limit at every pair of points of a set of full measure. That set is dense, and a Hölder function on a dense set extends to a Hölder function on the whole space (HolderOnWith.extend_of_dense), which is the required representative.

Main declarations #

TauCeti.W1p.exists_holderWith_ae_eq_value: Morrey's embedding; a function in W^{1,p}(ℝⁿ), n < p < ∞, agrees almost everywhere with a Hölder continuous function of exponent 1 - n / p, whose Hölder constant is controlled by ‖∇u‖_{Lᵖ}.
TauCeti.W1p.morreyRepresentative: the canonical continuous representative supplied by Morrey's estimate.

References #

D. Gilbarg, N. S. Trudinger, Elliptic Partial Differential Equations of Second Order, Theorem 7.17.
L. C. Evans, Partial Differential Equations, §5.6.2, Theorem 4.

source

theorem TauCeti.W1p.exists_holderWith_ae_eq_value {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (hp : ↑(Module.finrank ℝ E) < p) (u : ↥(W1p mu ⊤ ↑p)) :

∃ (g : E → ℝ), HolderWith ((2 ^ (Module.finrank ℝ E + 1) / (↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1)) * (↑(Module.finrank ℝ E) * mu.real (Metric.ball 0 1) * (↑p - 1) / (↑p - ↑(Module.finrank ℝ E))) ^ (1 - 1 / ↑p) * 2 ^ (1 - ↑(Module.finrank ℝ E) / ↑p)).toNNReal * ‖gradient u‖₊) (1 - ↑(Module.finrank ℝ E) / p) g ∧ ↑↑(value u) =ᵐ[mu] g

Morrey's embedding for W^{1,p}(ℝⁿ). If p exceeds the dimension n of the space and is finite, then every u ∈ W^{1,p}(ℝⁿ) agrees almost everywhere with a function which is Hölder continuous of exponent 1 - n / p, with constant 2 ^ (n + 1) / (n ω) * K ^ (1 - 1 / p) * 2 ^ (1 - n / p) * ‖∇u‖_{Lᵖ}, where ω = μ(B(0, 1)) and K = n ω (p - 1) / (p - n).

source

noncomputable def TauCeti.W1p.morreyRepresentative {E : Type u_1} [MeasurableSpace E] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E] {mu : MeasureTheory.Measure E} [mu.IsAddHaarMeasure] {p : NNReal} [Fact (1 ≤ ↑p)] (u : ↥(W1p mu ⊤ ↑p)) (hp : ↑(Module.finrank ℝ E) < p) :

E → ℝ

The canonical continuous representative of a whole-space Sobolev function in Morrey's supercritical range. It is canonical because two continuous representatives that agree almost everywhere for Haar measure agree everywhere.

Equations