Morrey's embedding into the Hölder Banach space

This file packages the continuous representative supplied by Morrey's inequality as a bounded linear map from W^{1,p}(ℝⁿ) to the global Hölder space of exponent 1 - n / p when n < p < ∞. The supremum part of the Hölder norm is controlled by averaging on unit balls: a Hölder representative differs from its unit-ball average by at most its Hölder constant, while Hölder's inequality controls the average by its Lᵖ norm.

Main declarations

• TauCeti.W1p.morreyEmbedding: Morrey's embedding as a continuous linear map into TauCeti.HolderSpace.

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.

noncomputable def TauCeti.W1p.morreyEmbedding {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) : ↥(W1p mu ⊤ ↑p) →L[ℝ] HolderSpace (1 - ↑(Module.finrank ℝ E) / p) E ℝ

Morrey's embedding into the Hölder Banach space. If p exceeds the dimension of E, this continuous linear map sends a whole-space W^{1,p} function to its unique continuous representative in the global Hölder space of exponent 1 - n / p.

Equations

• TauCeti.W1p.morreyEmbedding hp = (TauCeti.W1p.morreyEmbeddingLinearMap✝ hp).mkContinuous ⋯.choose ⋯

@[simp]

theorem TauCeti.W1p.morreyEmbedding_apply_apply {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)) (x : E) : ↑((morreyEmbedding hp) u).toHolderSubmodule x = morreyRepresentative u hp x

Evaluating the Morrey embedding gives the canonical continuous representative.

theorem TauCeti.W1p.value_ae_eq_morreyEmbedding {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)) : ↑↑(value u) =ᵐ[mu] ⇑↑((morreyEmbedding hp) u).toHolderSubmodule

The Hölder function produced by Morrey's embedding represents the original Sobolev value.

theorem TauCeti.W1p.morreyEmbedding_injective {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) : Function.Injective ⇑(morreyEmbedding hp)

Morrey's continuous linear map is an embedding: the continuous representative determines its Sobolev class.