Iterating the Sobolev ladder

One Gagliardo-Nirenberg-Sobolev step raises the exponent from p to p' with 1/p' = 1/p - 1/d, and EllipticPdes.Embedding.morrey_ball asks for p' > d. Starting from the L² data an H² estimate delivers, a single step reaches p' > d only in dimensions one to three, which is where EllipticPdes.Embedding.exists_eLpNorm_six_le and EllipticPdes.Embedding.exists_eLpNorm_four_le stop.

Iterating the step reaches every dimension, at the price of consuming a weak derivative per rung. The family that pays for it is one closed under differentiation: an index type ι, a function F i for each index, and a successor nxt i k naming the k-th weak derivative of F i. A solution with weak derivatives of every order has such a family, indexed by lists of directions, and closure is what lets a single induction climb without bookkeeping of orders.

Rungs

Each rung improves the reciprocal exponent by 1/(2d) rather than the full 1/d the inequality allows. The half-step is deliberate. Starting at 1/2 and taking d - 1 rungs of 1/(2d) lands at 1/(2d), so the exponent reached is 2d, comfortably past d, while every intermediate reciprocal 1/2 - s/(2d) stays strictly positive for s < d. Full steps would land on 1/p' = 0 in even dimensions and on p' = d exactly one rung earlier, both degenerate.

A rung consumes two exponents: the data sits at q_s with 1/q_s = 1/2 - s/(2d), the inequality is applied at p with 1/p = 1/q_{s+1} + 1/d, and p ≤ q_s follows from the half-step, so EllipticPdes.Embedding.exists_eLpNorm_sobolevConj_le_of_le takes the drop from q_s to p on the ball's finite measure. That p may sit below 2, which is why the ladder is stated against the exponent-lowering form of the bootstrap rather than the sharp one.

Each rung also shrinks the ball. The induction hands the shrinking back to its own hypothesis, so the statement is between one fixed pair of radii r < R however many rungs it runs.

Main declarations

• EllipticPdes.Embedding.memLp_of_gradClosed: the ladder, at rung s and any exponent the rung reaches.
• EllipticPdes.Embedding.memLp_two_mul_of_gradClosed: the ladder run to the top, landing at 2d > d, which is what EllipticPdes.Embedding.morrey_ball consumes.

References

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

Ladder

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

Sobolev ladder on a family closed under differentiation. 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 every F i lie in L² there. Then at rung s < d every F i lies in Lq on Metric.ball c r, for any exponent q ≥ 2 whose reciprocal is at least 1/2 - s/(2d).

The induction is on the rung. Each step splits the gap r < R at its midpoint, applies the hypothesis at rung s on the outer half to the whole family at once, and takes one Gagliardo-Nirenberg-Sobolev step on the inner half. Closure is what makes the second half work: the gradient of F i is again a member of the family, so the hypothesis supplies its Lq bound with no separate induction on the order of differentiation.

theorem EllipticPdes.Embedding.memLp_two_mul_of_gradClosed {d : ℕ} (hd : 0 < d) (c : EuclideanSpace ℝ (Fin d)) {ι : Type u_1} {F : ι → EuclideanSpace ℝ (Fin d) → ℝ} {nxt : ι → Fin d → ι} {r R : ℝ} (hr : 0 < r) (hrR : r < R) (hgrad : ∀ (i : ι), HasWeakGradOn (Metric.ball c R) (F i) fun (k : Fin d) => F (nxt i k)) (hmem : ∀ (i : ι), MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (Metric.ball c R))) (i : ι) : MeasureTheory.MemLp (F i) (2 * ↑↑d) (MeasureTheory.volume.restrict (Metric.ball c r))

Ladder run to the top. A family closed under differentiation, 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 - 1, and the reciprocal it lands on is 1/2 - (d-1)/(2d) = 1/(2d).