A (strong) Sobolev space H^m on ℝ^n: smooth functions u : ℝ^n → ℂ of class
C^m such that each iterated Fréchet derivative D^j u (for j ≤ m) is square
integrable with respect to Lebesgue measure.
- toFun : EuclideanSpace ℝ (Fin n) → ℂ
- iteratedFDeriv_memLp (j : ℕ) (hj : j ≤ m) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j self.toFun x) 2 MeasureTheory.volume
Instances For
Treat a Sobolev space element as the underlying function ℝ^n → ℂ.
H^m ⊂ H^{m'} whenever m' ≤ m: lower the Sobolev order of an element by
restricting the derivative-integrability hypothesis.
Instances For
For u ∈ H^m and a coordinate direction j, the partial derivative
∂_j u has all iterated derivatives up to order m-1 in L^2. This is the
key technical lemma used to define SobolevSpace.partialDeriv.
Partial derivative ∂_j u as an element of H^{m-1}, given u ∈ H^m.
Instances For
Iterate the partial derivative in direction j exactly k times, mapping
H^m into H^{m-k}.
Instances For
Density of Schwartz functions in H^m in the simultaneous-derivative sense:
given f whose first m derivatives are in L^2, there is a Schwartz function φ
whose iterated derivatives of every order i ≤ m are within ε of those of f
in L^2.
Schwartz approximation in the H^m norm: there exists φ ∈ 𝓢 whose
combined L^2 error across all derivative orders up to m (the H^m-norm of
φ - f) is less than ε.
Reformulation of Schwartz density: from a small H^m-norm approximation we
derive that each individual L^2 derivative discrepancy is less than ε.
Variant of Schwartz density bounding the squared L^2 discrepancy of every
derivative order i ≤ m by a prescribed δ.
Core Schwartz approximation: bound the joint H^m-norm error
(∑ ‖D^i φ - D^i f‖_{L^2}^2)^{1/2} by ε.
Schwartz density in H^m: for every H^m function f and every ε > 0
there is a Schwartz function φ such that every derivative D^i φ approximates
D^i f in L^2 to within ε.
Sobolev L^∞ bound on derivatives: under the condition n < 2(m - j)
(Sobolev embedding threshold), the pointwise difference of j-th derivatives
is controlled by the sum of L^2 differences of all derivatives i ≤ m.
Combining Schwartz density with the Sobolev L^∞ bound: under
n < 2(m - j) we obtain a sequence of Schwartz functions whose j-th
derivatives converge uniformly to the j-th derivative of f.
Sobolev embedding (base case): if all derivatives of f up to order m
are in L^2 and n < 2(m - i), then D^i f is continuous. This is proved by
uniform convergence of Schwartz approximations.
Sobolev embedding (differentiability, base case): under n < 2(m - (i+1)),
the iterated derivative D^i f is differentiable, via uniform convergence of
Schwartz approximants together with their derivatives.
Sobolev embedding theorem (Melrose Thm 10.1): if n < 2(m - k) and k ≤ m,
then any f whose first m derivatives are in L^2 is of class C^k.
Continuity corollary of the Sobolev embedding: D^i f is continuous for
all i such that the embedding threshold is met.
Differentiability corollary of Sobolev embedding: D^i f is differentiable
whenever the strict embedding threshold is met.
Sobolev embedding theorem (final user-facing form): H^m ⊂ C^k when
n < 2(m - k).
Application of the Sobolev embedding to elements u ∈ H^m: continuity of
D^j u for j ≤ k.
Application of the Sobolev embedding to u ∈ H^m: differentiability of
D^j u for j < k.
Each iterated derivative of a Schwartz function vanishes at infinity (in the cocompact filter).
General principle: if F_i → g uniformly and each F_i vanishes at infinity
(cocompactly), then so does g.
Sobolev embedding into C_0^k: the iterated derivative D^j f vanishes at
infinity (cocompactly) when f has H^m regularity above the Sobolev threshold.
Specialization of sobolev_iteratedFDeriv_vanish_of_memLp to elements of
SobolevSpace n m.
Vanishing at infinity of derivatives D^j u for u ∈ H^m, j ≤ k,
under n < 2(m - k).
Auxiliary: any u ∈ H^m is continuous when n < 2m.
Auxiliary: any u ∈ H^m vanishes at infinity when n < 2m, so
H^m ⊂ C_0 whenever m > n/2.
Weak Sobolev space: a function whose iterated derivatives up to order m
are in L^2, but without an a priori smoothness assumption on the function
itself. Used as the input type for the Sobolev embedding.
- toFun : EuclideanSpace ℝ (Fin n) → ℂ
- iteratedFDeriv_memLp (j : ℕ) (hj : j ≤ m) : MeasureTheory.MemLp (fun (x : EuclideanSpace ℝ (Fin n)) => iteratedFDeriv ℝ j self.toFun x) 2 MeasureTheory.volume
Instances For
Treat a weak Sobolev space element as the underlying function ℝ^n → ℂ.
The (strong) Sobolev space embeds into the weak Sobolev space by forgetting the a priori smoothness.
Instances For
Sobolev embedding (Melrose Cor. 10.3): if k ≤ m and n < 2(m - k),
then every weak Sobolev function u ∈ H^m is (a.e. equal to) a C^k function
whose derivatives of order ≤ k all vanish at infinity, i.e. H^m ↪ C_0^k.
Instances For
Sobolev embedding restated for strong Sobolev space elements u ∈ H^m.
Instances For
The smooth Sobolev space H^∞ = ⋂_m H^m: a function u that lies in every
H^m with a consistent underlying function.
- mem_sobolev (m : ℕ) : SobolevSpace n m
Instances For
Base case k = 0 of the Sobolev embedding: H^m ⊂ C_0 when m > n/2.
Instances For
Membership criterion for multiIndicesBall: α ∈ multiIndicesBall n m iff
the total order |α| is at most m.
The monomial x^α = ∏ x_i^{α_i} viewed as a complex-valued function on
ℝ^n.
Instances For
Iterate the line derivative ∂_{x_j} exactly k times on a Schwartz
function.
Instances For
The multi-index partial derivative ∂^β on Schwartz functions, defined by
iteratively applying coordinate derivatives in each direction j exactly
β j times.
Instances For
iterSchwartzDerivCoord is additive in its Schwartz argument.
iterSchwartzDeriv β is additive in its Schwartz argument.
iterSchwartzDerivCoord is ℂ-linear in its Schwartz argument.
iterSchwartzDeriv β is ℂ-linear in its Schwartz argument.
Every Schwartz derivative ∂^α φ belongs to L^2.
Map a Schwartz function φ to the L^2 equivalence class of ∂^α φ.
Instances For
schwartzToLp is additive in the Schwartz argument.
schwartzToLp is ℂ-linear in the Schwartz argument.
Pairing ⟨f, φ⟩ = ∫ f(x) · φ(x) dx of a C_0 function f against a
Schwartz function φ, used to express tempered distributions of the form
arising in the Schwartz representation theorem.
Instances For
Hahn–Banach + Riesz representation for sums of L^2-bounded operators:
given a linear functional L : V → ℂ controlled by ‖L v‖ ≤ C ∑_α ‖T α v‖_{L²},
there exist L² functions g α such that L v = ∑_α ∫ g α · T α v. The key
analytic tool used to derive the Schwartz representation theorem.
If a continuous linear functional u on Schwartz space is bounded by the
sum of L^2 norms of Schwartz derivatives ∂^α φ over |α| ≤ m, then u
admits an L^2 representation u φ = ∑_α ∫ g_α · ∂^α φ.
Weighted pointwise bound: for a Schwartz function φ, the product
‖x‖^k · ‖D^l φ(x)‖ is dominated by a sum of L^2 norms of Schwartz
derivatives of order ≤ k + l + n + 1. Used to convert Schwartz seminorms
to L^2-based estimates.
Auxiliary form: a single Schwartz seminorm ‖φ‖_{k,l} is bounded above by
a sum of L^2 norms of Schwartz derivatives of order ≤ k + l + n + 1.
Pointwise Sobolev-type bound: for some m, C > 0, the weighted product
‖x‖^k · ‖D^l φ(x)‖ is bounded by C times the sum of L^2 norms of
Schwartz derivatives of order ≤ m.
A single Schwartz seminorm ‖·‖_{k,l} is bounded by C times a sum of
L^2 norms of Schwartz derivatives ∂^α over a multi-index ball.
Joint bound: the supremum of a finite family of Schwartz seminorms can be
controlled by a single sum of L^2 derivative norms.
Continuous linear functionals on Schwartz space are bounded by a sum of
L^2 norms of Schwartz derivatives, yielding a Sobolev-type estimate.
Every continuous linear functional u on Schwartz space admits an L^2
derivative representation: u φ = ∑_α ∫ g_α · ∂^α φ for some finite collection
of L^2 functions g_α indexed by multi-indices |α| ≤ m.
L^2 derivative representation for tempered distributions: every
u ∈ 𝓢'(ℝ^n, ℂ) is a finite sum of derivatives of L^2 functions paired with
test functions.
Fourier multiplier promotes any L^2 function to a representative with
H^{n+j+1} regularity (a placeholder for an appropriate Fourier-side lift,
used to feed the Sobolev embedding).
Any L^2 function is a.e. equal to an element of a Sobolev space
SobolevSpace n j, by combining Fourier regularization with the Sobolev
embedding.
Hölder-type bound for the L^2 × Schwartz pairing: ‖∫ g · ψ‖ is
controlled by a sum of L^2 norms of Schwartz derivatives over
multiIndicesBall n j.
The product g · ψ of an L^2 function and a Schwartz function is
integrable.
Decomposition of an L^2 pairing into Sobolev derivatives: every
L^2 function g admits a representation ∫ g·ψ = ∑_β ∫ w_β · ∂^β ψ where
each w_β lies in SobolevSpace n j.
Variant of l2_sobolev_decomp_for_order choosing j large enough so that
n < 2j, hence guaranteeing each Sobolev representative is automatically a
continuous C_0 function (via the Sobolev embedding).
L^2 to C_0-derivative decomposition: every L^2 pairing equals a sum
∑_β c0SchwartzPairing (v β) (∂^β ψ) with each v β a C_0 function (the
Sobolev representatives produced by the Sobolev embedding).
Directional derivatives on Schwartz space commute: ∂_v ∂_w φ = ∂_w ∂_v φ.
A consequence of Schwarz's symmetry of second derivatives.
Iterated directional derivatives commute past a single directional
derivative: ∂_v^k ∂_w φ = ∂_w ∂_v^k φ.
Two iterated directional derivatives commute: ∂_v^k ∂_w^m φ = ∂_w^m ∂_v^k φ.
Coordinate Schwartz derivatives commute: ∂_i^a ∂_j^b φ = ∂_j^b ∂_i^a φ.
A coordinate Schwartz derivative commutes with the foldr used to define
iterSchwartzDeriv, allowing rearrangement of derivative orderings.
Coordinate Schwartz derivatives compose by addition of orders:
∂_j^b ∂_j^a φ = ∂_j^{a+b} φ.
Composition of multi-index Schwartz derivatives:
∂^β (∂^α φ) = ∂^{α + β} φ.
Additivity of multi-index order: |α + β| = |α| + |β|.
For a fixed multi-index α, the pairing ∫ g · ∂^α φ can be rewritten
as a sum ∑_γ c0SchwartzPairing (w γ) (∂^γ φ) over a larger multi-index ball,
using the composition law ∂^β ∂^α = ∂^{α+β} together with L^2 → C_0
decomposition.
The multi-index ball is monotone in m.
The C_0–Schwartz pairing distributes over a finite sum of C_0
functions.
Joint L^2 → C_0 decomposition: a finite sum ∑_α ∫ g_α · ∂^α φ over
|α| ≤ m of L^2-functions can be rewritten as ∑_γ c0SchwartzPairing (v γ) (∂^γ φ)
with each v γ a C_0 function.
Intermediate form of the Schwartz representation theorem (Melrose
eq. (10.10)): every tempered distribution is a finite sum of derivatives of
C_0 functions paired with test functions.
The zero multi-index monomial is the constant function 1.
The C_0–Schwartz pairing is zero whenever the C_0 factor is zero.
The zero multi-index belongs to every multiIndicesBall n M.
Rewrite the C_0-derivative representation in the form
∑_{α,β} c0SchwartzPairing (f α β) (∂^β (x^α · φ)), by placing the monomial
factor inside the test function via SchwartzMap.smulLeftCLM.
Schwartz representation theorem (Melrose Thm 10.5, first form): every
tempered distribution u ∈ 𝓢'(ℝ^n, ℂ) can be written as
u φ = ∑_{α,β} c0SchwartzPairing (f α β) (∂^β (x^α · φ))
for some finite family of C_0 functions f α β.
Alternative rewrite where the monomial factor multiplies the derived test
function from outside: ∑_{α,β} c0SchwartzPairing (g α β) (x^α · ∂^β φ).
Schwartz representation theorem (Melrose Thm 10.5, second form): every
tempered distribution u ∈ 𝓢'(ℝ^n, ℂ) is a finite sum
u φ = ∑_{α,β} c0SchwartzPairing (v α β) (x^α · ∂^β φ)
with v α β continuous and vanishing at infinity.