Sobolev ladder for a compactly supported family

The ladder of EllipticPdes.Embedding.SobolevLadderGeneral runs on a ball and shrinks it at every rung, because each rung multiplies by a cutoff. A compactly supported class needs no cutoff, so the same induction runs on the whole space with no loss of domain, and the conclusion is global.

Two facts replace the finite measure of the ball. A compactly supported Lᵖ class is integrable, and its exponent lowers freely: both come from MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top applied to the support.

This is the half of the classical order-k embedding that asks nothing of a boundary. The general statement on a bounded domain with C¹ boundary reduces to it through an extension operator, which is where the boundary hypothesis is spent.

Main declarations

• EllipticPdes.Embedding.integrable_of_memLp_compactSupport: a compactly supported Lᵖ class is integrable.
• EllipticPdes.Embedding.memLp_sobolevConj_of_le_compactSupport: one rung on the whole space, fed by data at an exponent at or above p.
• EllipticPdes.Embedding.memLp_of_gradClosed_compactSupport: the ladder, on the whole space.
• EllipticPdes.Embedding.memLp_of_gradClosed_compactSupport_ideal: the ladder at the exponent case (i) names, under the strict condition p₀ s < d.

References

L. C. Evans, Partial Differential Equations (2nd ed.), §5.6.1 Thm 1 and §5.6.3 Thm 6.

Compact support in place of a finite measure

theorem EllipticPdes.Embedding.memLp_mono_exponent_compactSupport {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hcs : HasCompactSupport f) {p q : ENNReal} (hf : MeasureTheory.MemLp f q MeasureTheory.volume) (hpq : p ≤ q) : MeasureTheory.MemLp f p MeasureTheory.volume

Free lowering of the exponent of a compactly supported class. The support has finite measure, so Hölder's inequality on it gives the smaller exponent, with no hypothesis on the measure of the whole space.

theorem EllipticPdes.Embedding.integrable_of_memLp_compactSupport {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} (hcs : HasCompactSupport f) {p : NNReal} (hp : 1 ≤ p) (hf : MeasureTheory.MemLp f (↑p) MeasureTheory.volume) : MeasureTheory.Integrable f MeasureTheory.volume

Integrability of a compactly supported Lᵖ class, for any p ≥ 1.

One rung

theorem EllipticPdes.Embedding.memLp_sobolevConj_of_le_compactSupport {d : ℕ} (hd : 0 < d) {p q p' : NNReal} (hp : 1 ≤ p) (hpq : p ≤ q) (hpp' : (↑p')⁻¹ = (↑p)⁻¹ - (↑d)⁻¹) {v : EuclideanSpace ℝ (Fin d) → ℝ} {g : Fin d → EuclideanSpace ℝ (Fin d) → ℝ} (hvcs : HasCompactSupport v) (hgcs : ∀ (k : Fin d), HasCompactSupport (g k)) (hv : MeasureTheory.MemLp v (↑q) MeasureTheory.volume) (hg : ∀ (k : Fin d), MeasureTheory.MemLp (g k) (↑q) MeasureTheory.volume) (hwg : HasWeakGradOn Set.univ v g) : MeasureTheory.MemLp v (↑p') MeasureTheory.volume

One rung on the whole space. A compactly supported v whose weak gradient g is compactly supported and lies in L^q for some q ≥ p lies in Lᵖ', where 1/p' = 1/p - 1/d. The exponents drop from q to p on the support, and exists_eLpNorm_sobolevConj_le_compactSupport runs the rung.

The ladder

theorem EllipticPdes.Embedding.memLp_of_gradClosed_compactSupport {d : ℕ} (hd : 1 < d) {ι : 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) (hcs : ∀ (i : ι), HasCompactSupport (F i)) (s : ℕ) {q : NNReal} : ↑p₀ * ↑s ≤ ↑d → p₀ ≤ q → (↑p₀)⁻¹ - ↑s * (↑d)⁻¹ ≤ (↑q)⁻¹ → (∀ (i : ι), dep i < m → HasWeakGradOn Set.univ (F i) fun (k : Fin d) => F (nxt i k)) → (∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) (↑p₀) MeasureTheory.volume) → ∀ (i : ι), dep i + s ≤ m → MeasureTheory.MemLp (F i) (↑q) MeasureTheory.volume

Sobolev ladder on the whole space. Let F assign a function to each index of ι, let nxt i k name a weak k-derivative of F i on Set.univ, and let dep record how far an index sits above the root. If every member of the family is compactly supported, every index of depth at most m lies in L^{p₀}, and every index of depth below m has its weak gradient in the family, then at rung s with p₀ s ≤ d every index of depth at most m - s lies in L^q, for any q ≥ p₀ whose reciprocal is at least 1/p₀ - s/d.

The statement is the one of memLp_of_gradClosed_general with the ball replaced by the whole space and the radii gone: no rung shrinks the domain.

The exponent of case (i)

theorem EllipticPdes.Embedding.memLp_of_gradClosed_compactSupport_ideal {d : ℕ} (hd : 1 < d) {ι : 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) (hcs : ∀ (i : ι), HasCompactSupport (F i)) (s : ℕ) (hsd : ↑p₀ * ↑s < ↑d) (hgrad : ∀ (i : ι), dep i < m → HasWeakGradOn Set.univ (F i) fun (k : Fin d) => F (nxt i k)) (hmem : ∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) (↑p₀) MeasureTheory.volume) (i : ι) : dep i + s ≤ m → MeasureTheory.MemLp (F i) (↑((↑p₀)⁻¹ - ↑s * (↑d)⁻¹)⁻¹.toNNReal) MeasureTheory.volume

Whole-space bootstrap at the exponent case (i) names. Under the strict step condition p₀ s < d, which is the k < n/p of Evans §5.6.3 Theorem 6, the reciprocal 1/p₀ - s/d is positive and names a finite exponent, and the bootstrap lands on it with no loss of domain.

The cited statement takes a bounded Ω with C¹ boundary and concludes on it, with a norm estimate. The statement here asks nothing of a boundary, takes a family of compact support on the whole space, and is qualitative. The passage from the one to the other goes through the extension operator, EllipticPdes.Extension.exists_extension_subset_bound, and the statement it reaches on a bounded C¹ domain is EllipticPdes.Embedding.exists_const_memLp_of_gradClosed_domain.