Sobolev ladder at a general base exponent

EllipticPdes.Embedding.memLp_of_gradClosed_fullStep iterates the rung from p to p' with 1/p' = 1/p - 1/d starting at p = 2. This file runs the same iteration from any p₀ ∈ [1, ∞), which is the first case of Guo, Partial Differential Equations, Theorem IV.2.3 at the exponent that statement quantifies over.

Two regimes of a rung

The step from rung s to rung s + 1 applies the inequality at the exponent p with 1/p = 1/q + 1/d, where q is the target. That p is admissible when 1/q + 1/d ≤ 1, and at p₀ = 2 the hypotheses already give it: q ≥ 2 and d ≥ 2 put both summands at or below 1/2. Below p₀ = 2 the target may sit under the conjugate exponent d/(d-1), and there the step runs the other way: one rung from p₀ overshoots the target, and the exponent is lowered onto it by the finiteness of the ball's measure.

Dimension one

The base exponent p₀ = 1 in dimension one asks the rung for the conjugate of 1, whose reciprocal is 1 - 1 = 0. The rung produces a finite exponent and cannot express that, so the statement takes 1 < d. In dimension one the rung condition p₀ * s ≤ d leaves only s = 0, where the conclusion is the hypothesis with its exponent lowered.

Main declarations

• EllipticPdes.Embedding.memLp_of_gradClosed_general: the ladder at a general base exponent.
• EllipticPdes.Embedding.memLp_of_gradClosed_general_ideal: the same at the exponent 1/p₀ - s/d names, which is the exponent of Theorem IV.2.3 case (i).

References

Evans, Partial Differential Equations (2nd ed.), §5.6.3 Theorem 6 clause (i), and §5.6.1 Theorem 1 for the single rung. Guo, Partial Differential Equations, Theorem IV.2.3 case (i).

The ladder

theorem EllipticPdes.Embedding.memLp_of_gradClosed_general {d : ℕ} (hd : 1 < d) (c : EuclideanSpace ℝ (Fin 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) (s : ℕ) {q : NNReal} {r R : ℝ} : ↑p₀ * ↑s ≤ ↑d → p₀ ≤ q → (↑p₀)⁻¹ - ↑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) (↑p₀) (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 ladder from a general base exponent. 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. If every index of depth at most m lies in L^{p₀} there 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 on Metric.ball c r, for any q ≥ p₀ whose reciprocal is at least 1/p₀ - s/d.

The exponent of case (i)

theorem EllipticPdes.Embedding.memLp_of_gradClosed_general_ideal {d : ℕ} (hd : 1 < d) (c : EuclideanSpace ℝ (Fin 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) (s : ℕ) {r R : ℝ} (hsd : ↑p₀ * ↑s < ↑d) (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) (↑p₀) (MeasureTheory.volume.restrict (Metric.ball c R))) (i : ι) (hi : dep i + s ≤ m) : MeasureTheory.MemLp (F i) (↑((↑p₀)⁻¹ - ↑s * (↑d)⁻¹)⁻¹.toNNReal) (MeasureTheory.volume.restrict (Metric.ball c r))

Ladder at the exponent case (i) names. Under the strict rung 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; the ladder lands on it.