Hölder regularity of finite order from a bounded supply of weak derivatives #
Guo's Sobolev embedding (Guo, Partial Differential Equations, Theorem IV.2.3) has two cases.
The first raises the exponent, and EllipticPdes.Embedding.memLp_of_gradClosed_fullStep runs it.
The second reads a bounded supply of weak derivatives as classical ones: for u ∈ W^{m,p}(Ω)
with m > n/p, the conclusion is u ∈ C^{m-1-⌊n/p⌋, γ}(Ω). This file proves the second case at
p = 2, locally, for a family closed under weak differentiation as far as m.
Order the supply pays for #
The supply is spent in three places. Morrey asks for the weak gradient, so one order goes there;
the ladder takes ⌊d/2⌋ more raising that gradient from L² to L^{2d}; and reading the n-th
classical derivative asks the same of every index n levels up. So an index of depth dep i
reaches C^n while dep i + n + 1 + ⌊d/2⌋ ≤ m, and at dep i = 0 that is
n = m - 1 - ⌊d/2⌋, which is Guo's order exactly.
Hölder exponent #
The ladder lands on L^{2d} and EllipticPdes.Embedding.morrey_ball reads off 1 - d/(2d), so
the exponent is 1/2 in every dimension. For d odd this is Guo's ⌊d/2⌋ + 1 - d/2 on the
nose. For d even d/2 is an integer, Guo's statement leaves γ free in (0, 1), and 1/2 is
one admissible choice: the ladder's landing reciprocal is 0 there, so every finite exponent is
reached and 2d is the one this file fixes.
Main declarations #
EllipticPdes.Embedding.morreyExponent_two_mul: the landing exponent is1/2.EllipticPdes.Embedding.contDiffOn_holder_of_gradClosed: representatives of classC^{n, 1/2}, for every order the supply pays for, together with the identification of the family's entries as their classical partial derivatives.
References #
Guo, Partial Differential Equations, Theorem IV.2.3. Evans, Partial Differential Equations (2nd ed.), §5.6.3.
At the exponent 2d the Morrey exponent is 1/2, whatever the dimension.
Classical derivatives of finite order from a bounded supply of weak ones. 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² there and every index of depth below m has its weak gradient in
the family, then on any smaller concentric ball each index has a representative of class C^n
whenever dep i + n + 1 + ⌊d/2⌋ ≤ m, and that representative is Hölder-1/2 as soon as
dep i + 1 + ⌊d/2⌋ ≤ m.
The proof is the one EllipticPdes.Embedding.contDiffOn_of_gradClosed takes, run against a
supply that runs out. The ladder raises the weak gradient of a qualifying index to L^{2d},
Morrey converts that into a Hölder representative, and a continuous function with a continuous
weak gradient is classically differentiable, so an induction on the order reads the family as
C^n with no further shrinking of the ball. Each induction step spends one order, which is what
the depth condition records.
The last component states what the family means: on the inner ball the classical derivative of
v i is the tuple of the v (nxt i k), so an entry of depth n is the order-n classical
partial derivative of the root and the Hölder bound above is a bound on that derivative.
Hölder exponent Guo leaves open #
Hölder clause at a general exponent. The ladder run for s rungs lands at any P
the reciprocal relation 1/2 - s/d ≤ 1/P admits, and Morrey at P > d reads off the exponent
1 - d/P. The fixed exponent 1/2 of contDiffOn_holder_of_gradClosed is this at s = ⌊d/2⌋
and P = 2d.
Guo's free Hölder exponent in even dimension. When d/2 is an integer, which at p = 2
is Guo's case n/p ∈ ℕ, the ladder reaches every finite exponent, so the Hölder exponent may be
any value in (0,1). In odd dimension the reciprocal 1/2 - ⌊d/2⌋/d = 1/(2d) caps the exponent
at 2d and the Hölder exponent at 1/2, which is Guo's other case.
Hölder estimate with its constant, in the shape Guo states: one constant, depending
on the dimension, the exponent and the ball alone, bounding the Hölder seminorm of every member
of every family by the L^P norms of that member's first derivatives.
exists_holderOnWith_of_gradClosed is this with the constant discarded. The remaining step to
Guo's ‖u‖_{C^{k-1-⌊n/p⌋,γ}} ≤ C‖u‖_{W^{k,p}} is the ladder's own constant, which takes the
L^P norms here back to the L² data.
Guo's clause (ii) with its constant against the L² data. Composing the ladder's
constant with Morrey's gives one constant, depending on the dimension, the rung count, the
exponent and the two radii, bounding the Hölder seminorm of every member by a uniform L² bound
on the family over the outer ball. This is the shape of Guo's
‖u‖_{C^{k-1-⌊n/p⌋,γ}} ≤ C‖u‖_{W^{k,p}} at p = 2.