Sobolev bootstrap from Lᵖ to the conjugate exponent #
morrey_ball needs a gradient in Lᵖ with p > d, and the interior H² estimate delivers one
in L², so the two compose directly only when d = 1. The Gagliardo-Nirenberg-Sobolev
inequality closes the gap in low dimension: an Lᵖ weak gradient with 1 ≤ p < d upgrades to
Lᵖ' at the Sobolev conjugate 1/p' = 1/p - 1/d, and Morrey then applies whenever p' > d.
Dimensions the chain reaches #
p' > d is equivalent to p > d/2, and L² data on a ball of finite measure is Lᵖ data
exactly when p ≤ 2, so a single Sobolev step feeds Morrey precisely when the window
d/2 < p ≤ min 2 d is inhabited.
d = 1: Morrey applies to the first-order gradient atp = 2 > 1, so no bootstrap is needed.d = 2:p = 4/3has conjugate4 > 2(exists_eLpNorm_four_le).d = 3:p = 2has conjugate6 > 3(exists_eLpNorm_six_le).d ≥ 4: the window is empty, sinced/2 ≥ 2, so one Sobolev step never reachesp' > d.
The bootstrap itself holds in every dimension. Only its composition with Morrey out of L² data
is limited, and EllipticPdes.Embedding.memLp_of_gradClosed lifts that limit by iterating the
step, at the price of a weak derivative per rung.
Mathlib's MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq asks for ContDiff ℝ 1 and compact
support, neither of which an Lᵖ class with weak derivatives has. Two devices bridge that.
- A smooth cutoff
ηsupported in the ball turns a weak gradient on the ball into a compactly supported weak gradient on the whole space, with the product-rule termv ∂ₖη(hasWeakGradOn_univ_mul_cutoff). - Mollification turns that into a smooth compactly supported function whose classical partials
are the mollified weak gradient (
partialD_convolution_eq_of_hasWeakGradOnatSet.univ), whoseLᵖseminorms Young's inequality (eLpNorm_convolution_le) keeps bounded uniformly in the mollifier radius, and which converges almost everywhere to the original function, so Fatou (MeasureTheory.eLpNorm_le_of_ae_tendsto) passes theLᵖ'bound to the limit.
Main declarations #
HasWeakGradOn.mono: a weak gradient restricts to a subset.hasWeakGradOn_univ_mul_cutoff: the product rule against a smooth cutoff.exists_eLpNorm_sobolevConj_le: the bootstrap in general dimension and at a general exponent pair, with a constant independent of the function.exists_eLpNorm_sobolevConj_le_of_le: the same, fed by data at a higher exponent.exists_eLpNorm_six_leandexists_eLpNorm_four_le: thed = 3andd = 2specialisations.
References #
Evans, Partial Differential Equations (2nd ed.), §5.6.1 Thm 1.
Restriction of a weak gradient #
Restriction of a weak gradient to a subset. Both integration-by-parts integrals localise to
the support of the test function, which lies in the smaller set, so the identity over the larger
set transfers verbatim. No measurability of either set is needed: each integrand vanishes off
tsupport φ, and setIntegral_eq_integral_of_forall_compl_eq_zero collapses both set integrals
to the same whole-space integral.
Dependence of a weak gradient on the almost-everywhere classes alone. Replacing u and
g by functions agreeing with them almost everywhere on B leaves the integration-by-parts
identity untouched. This moves a statement about a restricted Lp class onto whichever
representative is convenient, in particular onto the extension by zero, which is shared across
every set.
Product rule against a smooth cutoff #
The product rule for the coordinate partial derivative.
Cutting a weak gradient off. If g is the weak gradient of u on B and η is a
smooth compactly supported function with tsupport η ⊆ B, then the extension by zero of η u
has a weak gradient on the whole space, namely η gₖ + u ∂ₖη. Testing against φ reduces to
testing the hypothesis against η φ, which is again a test function supported in B, and the
product rule supplies the extra term. This is what makes the mollification argument reach a
compactly supported function without a boundary contribution from ∂B.
Bootstrap #
Gagliardo-Nirenberg-Sobolev for a compactly supported weak gradient. A compactly
supported w on ℝᵈ whose weak gradient G lies in Lᵖ lies in Lᵖ', where
1/p' = 1/p - 1/d, bounded by the gradient alone with a constant depending only on d and
p.
Mathlib's MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq asks for ContDiff ℝ 1, so a weak
gradient reaches it through a mollification, whose classical partials are the mollified weak
gradient (partialD_convolution_eq_of_hasWeakGradOn) and whose Lᵖ seminorms Young's
inequality keeps bounded uniformly in the mollifier radius. Fatou passes the bound to the
almost-everywhere limit.
No cutoff enters, so the conclusion is on the whole space and the bound has no ‖w‖_{Lᵖ}
term. exists_eLpNorm_sobolevConj_le is this statement composed with a cutoff, and the cutoff
is what forces the smaller ball and the extra term.
From Lᵖ to the Sobolev conjugate Lᵖ' (Evans, Partial Differential Equations
(2nd ed.), §5.6.1 Thm 1). On a ball Metric.ball c R of ℝᵈ with d ≥ 1, a function v with
an Lᵖ weak gradient g lies in Lᵖ' of the smaller ball Metric.ball c r, where the exponents
satisfy 1/p' = 1/p - 1/d, with a bound linear in ‖v‖_{Lᵖ} + ∑ₖ ‖gₖ‖_{Lᵖ} and a constant
depending only on d, p, c, r and R.
The inequality itself is Mathlib's MeasureTheory.eLpNorm_le_eLpNorm_fderiv_of_eq, which asks
for ContDiff ℝ 1 and compact support. Two devices transport it to a weak gradient on a ball: a
smooth cutoff supported in Metric.ball c R and equal to 1 on Metric.closedBall c r, and a
mollification, whose classical partials are the mollified weak gradient and whose Lᵖ seminorms
Young's inequality keeps bounded uniformly in the mollifier radius. Fatou passes the resulting
Lᵖ' bound to the almost-everywhere limit.
Outside the range 1 ≤ p < d, which is the range Evans' statement takes, the hypothesis
1/p' = 1/p - 1/d says nothing about a Sobolev conjugate. At p = d it forces p' = 0 and
the conclusion degenerates, eLpNorm at exponent zero being zero; above p = d its right
side is negative while the left is a reciprocal of a nonnegative number, so no p' meets it
and the statement is vacuous.
Bootstrap fed by a higher exponent. The ball has finite measure, so Lq data with
p ≤ q is Lᵖ data, at the price of a factor |B|^{1/p - 1/q} which the constant absorbs.
This is the form the dimension-two chain uses: the interior H² estimate delivers L² data,
while the exponent that reaches Morrey through 1/p' = 1/p - 1/d is p = 4/3.
From L² to L⁶ in dimension three. The Sobolev conjugate of 2 in dimension 3 is
2·3/(3-2) = 6, so a function with an L² weak gradient on Metric.ball c R lies in L⁶ of
Metric.ball c r. Since 6 > 3, this single step feeds morrey_ball.
From L² to L⁴ in dimension two. At d = 2 the Sobolev conjugate of 2 degenerates,
so the step is taken at p = 4/3, whose conjugate is 4. The ball has finite measure, so the
L² data of the interior H² estimate is L^{4/3} data. Since 4 > 2, the result feeds
morrey_ball, with Hölder exponent 1 - 2/4 = 1/2.