Sobolev ladder at the full step

EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le raises the exponent from p to p' with 1/p' = 1/p - 1/d. Iterating it s times lands on 1/p - s/d, which is the exponent Guo's Sobolev embedding writes as p^{∗⋯∗} (Guo, Partial Differential Equations, Theorem IV.2.3). This file runs that iteration from p = 2, at the full step and to a bounded depth.

Rung condition

A rung is available while the reciprocal below it stays positive, and 2 * s ≤ d is what keeps it so: at the top rung the reciprocal is 1/2 - s/d ≥ 0, and at every rung below it exceeds 1/d. So ⌊d/2⌋ rungs run, against the d - 1 a half-step ladder needs, and both reach L^{2d}.

The top rung is where the two dimensional parities separate. For d even the reciprocal at s = d/2 is exactly 0, so the rung reaches every finite exponent and attains none of them; for d odd it is 1/(2d), and that one is attained. Neither case is special in the proof, since the statement asks only that the target reciprocal be at least 1/2 - s/d, and EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_of_le is what lets a rung be fed from an exponent above the one it consumes. That is the same mechanism EllipticPdes.Embedding.exists_eLpNorm_four_le uses in dimension two.

Bounded depth

The family is closed under differentiation only as far as dep records. An index i sits at depth dep i, differentiating adds at most one, and m is the total supply. Running s rungs on F i consumes s of the orders above dep i, so the conclusion is stated for those i with dep i + s ≤ m. A family closed at every order is the case dep = 0.

Main declarations

• EllipticPdes.Embedding.memLp_of_gradClosed_fullStep: the ladder, at rung s and any exponent the rung reaches.
• EllipticPdes.Embedding.memLp_two_mul_of_gradClosed_fullStep: the ladder run to L^{2d}, which passes d in every dimension and is what EllipticPdes.Embedding.morrey_ball consumes.

References

Guo, Partial Differential Equations, Theorem IV.2.3. Evans, Partial Differential Equations (2nd ed.), §5.6.1 Thm 1 and §5.6.3.

Ladder

theorem EllipticPdes.Embedding.memLp_of_gradClosed_fullStep {d : ℕ} (hd : 0 < d) (c : EuclideanSpace ℝ (Fin d)) {ι : Type u_1} {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} {dep : ι → ℕ} {m : ℕ} (hdep : ∀ (i : ι) (k : Fin d), dep (nxt i k) ≤ dep i + 1) (s : ℕ) {q : NNReal} {r R : ℝ} : 2 * s ≤ d → 2 ≤ q → 2⁻¹ - ↑s * (↑d)⁻¹ ≤ (↑q)⁻¹ → 0 < r → r < R → (∀ (i : ι), dep i < m → HasWeakGradOn (Metric.ball c R) (F i) fun (k : Fin d) => F (nxt i k)) → (∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) → ∀ (i : ι), dep i + s ≤ m → MeasureTheory.MemLp (F i) (↑q) (MeasureTheory.volume.restrict (Metric.ball c r))

Sobolev bootstrap at the full step to bounded depth. Let F assign a function to each index of ι, let nxt i k name a weak k-derivative of F i on Metric.ball c R, and let dep record how far an index sits above the root, so that differentiating adds at most one. If every index of depth at most m lies in L² there and every index of depth below m has its weak gradient in the family, then at step s with 2 * s ≤ d every index of depth at most m - s lies in Lq on Metric.ball c r, for any exponent q ≥ 2 whose reciprocal is at least 1/2 - s/d.

The induction is on the step. Each one splits the gap r < R at its midpoint, applies the hypothesis at step s on the outer half to the index and to its derivatives, and takes one Gagliardo-Nirenberg-Sobolev step on the inner half. The depth bookkeeping is what replaces closure at every order: a derivative sits one level higher, so a step fewer is available to it, and that is what the recursive call is given.

theorem EllipticPdes.Embedding.memLp_two_mul_of_gradClosed_fullStep {d : ℕ} (hd : 0 < d) (c : EuclideanSpace ℝ (Fin d)) {ι : Type u_1} {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} {dep : ι → ℕ} {m : ℕ} (hdep : ∀ (i : ι) (k : Fin d), dep (nxt i k) ≤ dep i + 1) {r R : ℝ} (hr : 0 < r) (hrR : r < R) (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) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) (i : ι) (hi : dep i + d / 2 ≤ m) : MeasureTheory.MemLp (F i) (2 * ↑↑d) (MeasureTheory.volume.restrict (Metric.ball c r))

Full-step ladder run to the top. An index of depth at most m - ⌊d/2⌋ in a family closed under weak differentiation as far as m, with every member of depth at most m in L² on Metric.ball c R, lies in L^{2d} on any smaller concentric ball. Since 2d > d, this is the exponent EllipticPdes.Embedding.morrey_ball asks for, in every dimension.

The rung count is ⌊d/2⌋, and the reciprocal it lands on is 1/2 - ⌊d/2⌋/d, which is 0 when d is even and 1/(2d) when d is odd. Both are at most 1/(2d), which is why one statement serves the two parities.

The ladder with its constant

theorem EllipticPdes.Embedding.exists_const_eLpNorm_le_of_gradClosed_fullStep {d : ℕ} (hd : 0 < d) (c : EuclideanSpace ℝ (Fin d)) (ι : Type u_1) (s : ℕ) {q : NNReal} {r R : ℝ} : 2 * s ≤ d → 2 ≤ q → 2⁻¹ - ↑s * (↑d)⁻¹ ≤ (↑q)⁻¹ → 0 < r → r < R → ∃ (K : 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 (Metric.ball c R) (F i) fun (k : Fin d) => F (nxt i k)) → (∀ (i : ι), dep i ≤ m → MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) → ∀ (M : NNReal), (∀ (j : ι), dep j ≤ m → MeasureTheory.eLpNorm (F j) 2 (MeasureTheory.volume.restrict (Metric.ball c R)) ≤ ↑M) → ∀ (i : ι), dep i + s ≤ m → MeasureTheory.eLpNorm (F i) (↑q) (MeasureTheory.volume.restrict (Metric.ball c r)) ≤ ↑K * ↑M

Full-step ladder with a constant. One constant, depending on the dimension, the rung count, the exponent and the two radii alone, takes a uniform L² bound on the family over the outer ball to an L^q bound on the inner one, at every index the rungs reach.

memLp_of_gradClosed_fullStep is this with the constant discarded. Guo's ‖u‖_{L^q} ≤ C‖u‖_{W^{k,p}} at p = 2 is this estimate: the bound is by the L² data alone, uniformly over the members the rungs consume.