Bessel-potential regularity from first derivatives #
For 1 < p < ∞, a tempered distribution lies in Mathlib's Bessel-potential space H^{s+1,p}
exactly when it and all its first directional derivatives lie in H^{s,p}. Mathlib proves the
inclusion H^{s+1,2} ⊆ H^{s,2} and that derivatives map H^{s,2} to H^{s-1,2}
(TemperedDistribution.MemSobolev.mono, TemperedDistribution.MemSobolev.lineDerivOp) by
Plancherel, since for p = 2 every bounded symbol is a multiplier. For other p, the symbols
involved, (1 + ‖ξ‖ ^ 2) ^ (-t / 2) with t ≥ 0 and ⟪ξ, v⟫ (1 + ‖ξ‖ ^ 2) ^ (-1 / 2), are
symbols of order 0 (TauCeti.exists_norm_iteratedFDeriv_one_add_norm_sq_rpow_le,
TauCeti.exists_norm_iteratedFDeriv_inner_mul_one_add_norm_sq_rpow_le), so they satisfy
Mihlin's condition, and the Mihlin–Hörmander multiplier theorem makes them bounded on Lᵖ
(TauCeti.exists_fourierMultiplierCLM_eq_and_norm_le_of_norm_iteratedFDeriv_le). The converse
direction needs the derivatives only along an orthonormal basis: J¹ f = J⁻¹ (J² f) with
J² = 1 - (2π)⁻² Δ.
Use the regularity criteria to characterize Sobolev membership through directional derivatives,
either in all directions or along an orthonormal basis. The order-two operator identity relates
the Bessel potential to the Laplacian, with the factor 2π from Mathlib's Fourier normalization.
Main declarations #
TemperedDistribution.besselPotential_two_eq_sub_laplacian: the Bessel potential of order2is1 - (2π)⁻² Δ.TemperedDistribution.MemSobolev.sum:H^{s,p}is closed under finite sums.TemperedDistribution.MemSobolev.smul_of_tower:H^{s,p}is closed under scalar multiplication by scalars acting throughℂ, such as real numbers.TemperedDistribution.sobolevSubmodule:H^{s,p}as a complex submodule of tempered distributions.TemperedDistribution.realSobolevSubmodule: the realLᵖfunctions whose complexification lies inH^{s,p}, as a real submodule ofLᵖ.TemperedDistribution.realSobolevFunctions: the pointwise representatives of these, as a real submodule of the functionsE → ℝ.TemperedDistribution.exists_memSobolev_ae_eq_of_mem_realSobolevFunctions: two real functionsf,ginrealSobolevFunctions E s pgive a complexH^{s,p}functionf + i g.TemperedDistribution.memLp_of_mem_realSobolevFunctions,TemperedDistribution.mem_realSobolevFunctions_zero_iff: these lie inLᵖ, and at order0they are exactly the realLᵖfunctions.TemperedDistribution.MemSobolev.fourierMultiplierCLM_of_norm_iteratedFDeriv_le: for1 < p < ∞, Fourier multipliers whose symbols satisfy Mihlin's condition mapH^{s,p}toH^{s,p}; a symbol without temperate growth gives the junk value0, so only symbols of temperate growth are covered.MemSobolev.fourierMultiplierCLM_ofReal_of_norm_iteratedFDeriv_le_one_add_norm_sq_rpow: for1 < p < ∞, real symbols of order0, whosek-th derivatives are bounded byC_k (1 + ‖x‖ ^ 2) ^ (-k / 2), mapH^{s,p}toH^{s,p}.TemperedDistribution.MemSobolev.mono_of_one_lt:H^{s,p} ⊆ H^{s',p}fors' ≤ s.TemperedDistribution.MemSobolev.lineDerivOp_of_one_lt:∂_mmapsH^{s,p}toH^{s-1,p}.TemperedDistribution.memSobolev_add_one_of_lineDerivOp: iffand its derivatives along an orthonormal basis lie inH^{s,p}, thenflies inH^{s+1,p}.TemperedDistribution.memSobolev_add_one_iff:f ∈ H^{s+1,p}exactly whenf ∈ H^{s,p}and∂_m f ∈ H^{s,p}for every directionm.TemperedDistribution.memSobolev_natCast_add_one_iff: at a natural orderk,f ∈ H^{k+1,p}exactly whenf ∈ H^{0,p}and∂_m f ∈ H^{k,p}for every directionm.
References #
- M. Taylor, Partial Differential Equations I, Chapter 4, §1.
- E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Chapter V, §3
(the Bessel-potential spaces
ℒᵖ_kand their characterization by derivatives).
The Bessel potential of order 2 is 1 - (2π)⁻² Δ. The factor (2π)⁻² comes from
Mathlib's normalisation of the Fourier transform.
A finite sum of tempered distributions in H^{s,p} lies in H^{s,p}.
H^{s,p} is closed under scalar multiplication by any scalars acting on tempered
distributions through ℂ, such as real numbers.
An Lᵖ function that agrees almost everywhere with a smooth compactly supported function lies
in every Bessel-potential space H^{s,p}.
The tempered distributions in the Bessel-potential space H^{s,p}, as a complex submodule of
𝓢'(E, F). This is the image in 𝓢'(E, F) of Mathlib's bundled BesselPotentialSpace.
Instances For
Membership in sobolevSubmodule is MemSobolev.
The real Lᵖ functions whose complexified tempered distribution lies in the
Bessel-potential space H^{s,p}, as a real submodule of Lᵖ.
Instances For
A real Lᵖ function lies in realSobolevSubmodule exactly when its complexification lies
in H^{s,p}.
Mihlin multipliers act on H^{s,p}. For 1 < p < ∞, the Fourier multiplier with a symbol
satisfying Mihlin's condition of order N, 2N > dim E, away from the origin maps H^{s,p} to
H^{s,p}. For p = 2 every bounded symbol does (MemSobolev.fourierMultiplierCLM_of_bounded).
Temperate growth of g is not assumed: if g lacks it, fourierMultiplierCLM F g is the junk
value 0 (TemperedDistribution.fourierMultiplierCLM_eq_zero_of_not_hasTemperateGrowth), so the
statement has content only for symbols of temperate growth, and symbols singular at the origin,
such as the Riesz symbols ξⱼ / ‖ξ‖, are not covered.
Order-zero real symbols act on H^{s,p}. For 1 < p < ∞, the Fourier multiplier with a
real symbol g of order 0 in Hörmander's sense, ‖D^k g x‖ ≤ C_k (1 + ‖x‖ ^ 2) ^ (-k / 2) for
every k, maps H^{s,p} to H^{s,p}. This is the Japanese-bracket form of Mihlin's condition in
MemSobolev.fourierMultiplierCLM_of_norm_iteratedFDeriv_le. As there, temperate growth of g is
not assumed: without it the multiplier is the junk value 0.
For 1 < p < ∞, H^{s,p} is contained in H^{s',p} whenever s' ≤ s. For p = 2 this is
MemSobolev.mono.
For 1 < p < ∞, the directional derivative maps H^{s,p} to H^{s-1,p}. For p = 2 this is
MemSobolev.lineDerivOp.
For 1 < p < ∞, a tempered distribution in H^{s,p} whose derivatives along an orthonormal
basis lie in H^{s,p} lies in H^{s+1,p}.
For 1 < p < ∞, a tempered distribution lies in H^{s+1,p} exactly when it and all its
first directional derivatives lie in H^{s,p}.
For 1 < p < ∞ and a natural order k, a tempered distribution lies in H^{k+1,p} exactly
when it lies in H^{0,p} and all its first directional derivatives lie in H^{k,p}.
The real functions on E that agree almost everywhere with an element of
realSobolevSubmodule E s p: the pointwise representatives of real H^{s,p} functions.
Membership only depends on the function up to a null set
(mem_realSobolevFunctions_of_ae_eq).
Instances For
A real function lies in realSobolevFunctions E s p exactly when it agrees almost everywhere
with a real Lᵖ function whose complexification lies in H^{s,p}.
The values of an element of realSobolevSubmodule E s p lie in realSobolevFunctions E s p.
Membership in realSobolevFunctions E s p is invariant under almost-everywhere equality.
Two real functions f, g in realSobolevFunctions E s p assemble into a complex H^{s,p}
function: f + i g agrees almost everywhere with a complex Lᵖ function in H^{s,p}.
Every element of realSobolevFunctions E s p lies in Lᵖ, whatever the order s.
A real function lies in realSobolevFunctions E 0 p exactly when it lies in Lᵖ.
For 1 < p < ∞, the real H^{s,p} functions decrease as the order increases.
A smooth compactly supported real function lies in every real Bessel-potential space.