Existence form of the Schwartz Fourier isomorphism (Theorem 9.1 of
Melrose): the Fourier transform on the Schwartz space is a continuous
ℂ-linear equivalence whose inverse is the inverse Fourier transform.
The Fourier transform as a continuous ℂ-linear equivalence on the
Schwartz space 𝓢(V, E).
Instances For
The continuous linear equivalence fourierSchwartzCLE acts as the
Fourier transform 𝓕 on Schwartz functions.
The inverse of fourierSchwartzCLE acts as the inverse Fourier
transform 𝓕⁻ on Schwartz functions.
Parseval's identity (Lemma 9.2 of Melrose): for two Schwartz functions
φ, ψ : V → ℂ, the integral of φ(x) · conj(ψ(x)) equals the integral of
𝓕φ(ξ) · conj(𝓕ψ(ξ)).
The Fourier transform on tempered distributions packaged as a ℂ-linear
equivalence 𝓢'(E, F) ≃ₗ[ℂ] 𝓢'(E, F).
Instances For
Fourier inversion on tempered distributions: 𝓕⁻(𝓕 u) = u.
Fourier inversion on tempered distributions: 𝓕(𝓕⁻ u) = u.
The k-fold iterated distributional derivative in the j-th coordinate
direction, applied to a tempered distribution u.
Instances For
The mixed iterated distributional derivative ∂^α u indexed by a
multi-index α : Fin n → ℕ, defined by composing the per-coordinate iterated
derivatives over all coordinates.
Instances For
The k-fold iterated operation of multiplication by 2πi·ξ_j on a
tempered distribution, which is the Fourier-side counterpart of the iterated
derivative in the j-th coordinate.
Instances For
The multi-index iterated multiplication operation (2πi)^|α| ξ^α u on a
tempered distribution, Fourier-dual to the multi-index derivative ∂^α.
Instances For
The k-fold iterated operation of multiplication by -2πi·x_j on a
tempered distribution, used to express the iterated coordinate derivative on
the Fourier side after inversion.
Instances For
The multi-index iterated multiplication (-2πi)^|α| x^α u on a tempered
distribution, packaged via a fold over coordinates.
Instances For
The Fourier transform exchanges iterated coordinate derivatives with
iterated coordinate multiplication by 2πi·ξ_j:
𝓕 (∂_j^k u) = (2πi ξ_j)^k · 𝓕 u.
Multi-index version of the Fourier-derivative exchange:
𝓕 (∂^α u) = (2πi ξ)^α · 𝓕 u.
Dual identity: the iterated coordinate derivative on 𝓕 u equals the
Fourier transform of (-2πi x_j)^k u.
The Sobolev weight ⟨ξ⟩^s = (1 + ‖ξ‖²)^{s/2}, written using the
Japanese bracket. This is the standard symbol whose L²-decay determines
the Sobolev exponent s.
Instances For
The Sobolev weight ⟨ξ⟩^s is strictly positive for every ξ and every
real exponent s.
The Sobolev weight is nonzero, which is needed when inverting it inside integrals.
Membership in the Sobolev space H^s(ℝⁿ): a tempered distribution u
belongs to H^s if there exists g ∈ L² such that, for every Schwartz
function φ, (𝓕 u)(φ) = ∫ ⟨ξ⟩^{-s} g(ξ) φ(ξ) dξ. Equivalently, 𝓕 u
is given by integration against the L² function ⟨ξ⟩^{-s} g.
Instances For
Monotonicity of Sobolev spaces: H^s ⊆ H^t whenever t ≤ s. The
witness L² function for H^t is obtained by multiplying the witness for
H^s by ⟨ξ⟩^{t-s} ≤ 1.
The L² "witness" function attached to a Sobolev distribution: it is
the function g produced by the existential in MemHs. Concretely,
𝓕 u = ⟨ξ⟩^{-s} · witnessFunc s u as distributions.
Instances For
The witness function attached to a Sobolev distribution is in L².
The witness function packaged as an honest element of the Hilbert space
L²(ℝⁿ; ℂ).
Instances For
The defining property of Hs.witnessFunc: pairing 𝓕 u against a
Schwartz function recovers the integral of ⟨ξ⟩^{-s} · witnessFunc · φ.
Given an L² function f, construct the element of H^s whose witness
function is f: namely, 𝓕⁻¹ (⟨ξ⟩^{-s} f) as a tempered distribution.
Instances For
Right inverse: extracting the L² witness from Hs.fromL2 s f recovers
f. Uses Lebesgue uniqueness of integration against smooth, compactly
supported test functions to conclude the underlying functions are equal a.e.
The set-level bijection Hs n s ≃ L²(ℝⁿ; ℂ) provided by the witness
function construction.
Instances For
Transport the NormedAddCommGroup structure from L²(ℝⁿ; ℂ) to
Hs n s along the bijection Hs.equivLp.
Transport the complex inner-product-space structure from L²(ℝⁿ; ℂ) to
Hs n s along the bijection Hs.equivLp. The inner product on H^s is
⟨u, v⟩_{H^s} := ⟨witnessL2 u, witnessL2 v⟩_{L²}.
The Sobolev space H^s is complete: it inherits completeness from
L²(ℝⁿ; ℂ) via the isometric bijection Hs.equivLp.
The "Fourier-weight" linear isometric equivalence between H^s(ℝⁿ) and
L²(ℝⁿ; ℂ) sending each u to its L² witness ⟨ξ⟩^s · 𝓕u. This is the
fundamental Hilbert-space identification underlying the definition of
H^s.
Instances For
Schwartz functions are dense in H^s: for any linear isometric
identification Φ : H^s ≃ₗᵢ L², the composition Φ⁻¹ ∘ toLp of the
canonical Schwartz-to-L² map has dense range.
The Sobolev duality identification: H^{-s} ≃ (H^s)' as anti-linear
isometric equivalences, obtained by composing the two Fourier-weight
isometries with the Riesz representation H^s ≃ (H^s)'. This is part of
Proposition 9.8 of Melrose.
Instances For
The duality identification is a bijection between H^{-s} and the
continuous dual (H^s)'.
Proposition 9.8 of Melrose: for each s ∈ ℝ, the Sobolev space H^s
is a Hilbert space (linearly isometric to L² with Schwartz functions
dense), and there is an anti-linear isometric identification of H^{-s} with
the continuous dual of H^s.
The complex-valued Sobolev weight ξ ↦ ⟨ξ⟩^s has temperate growth, so
multiplication by it acts on Schwartz functions.
Every Schwartz function belongs to H^s for every real s: the
witness function is ⟨ξ⟩^s · 𝓕f, which is again Schwartz and in particular
in L².
Fourier exchange between derivatives and monomial multiplication on
Schwartz functions: ∂^α (𝓕 φ) = 𝓕 (x^α · φ).
Combining Fourier inversion with iterSchwartzDeriv_fourier_exchange:
𝓕⁻ (∂^α 𝓕 φ)(ξ) = ξ^α · φ(ξ), evaluated pointwise.
L²/Fourier pairing identity: for f ∈ L² and a Schwartz function
φ, the integral of f · ∂^α(𝓕 φ) equals the integral of
𝓕 f · ξ^α · φ, using the L² Fourier transform on the right.
The Japanese bracket ⟨ξ⟩ = √(1 + ‖ξ‖²) is at least 1.
Each coordinate |ξ i| is bounded by the Japanese bracket ⟨ξ⟩.
Pointwise norm bound: for any multi-index α of order at most m, the
product of the monomial ξ^α and the negative-Sobolev weight
⟨ξ⟩^{-m} has complex norm at most 1. This is the key bound that makes
the construction of L² witnesses for H^{-m} work.
Existence form: for each L² function f and multi-index α, there
exists an L² function fhat (concretely the L² Fourier transform of
f) such that pairing f with ∂^α (𝓕 ψ) equals pairing ξ^α · fhat
with ψ.
Restatement of monomial_sobolevWeight_norm_le_one using the explicit
product ∏ ξ_i^{α_i} instead of monomial α.
If h is bounded by 1 almost everywhere and g ∈ L², then the
pointwise product h · g lies in L². This is the order in which the
measurability argument is most convenient.
A finite product of functions with temperate growth has temperate growth. The proof is a Finset induction using closure of temperate growth under multiplication.
The monomial ξ ↦ ∏_i (ξ_i)^{α_i} (as a complex-valued function) has
temperate growth.
The integrand ξ^α · f · φ is integrable when f ∈ L² and φ is a
Schwartz function (so ξ^α · φ is still Schwartz, hence in L²).
One direction of Proposition 9.7 of Melrose: if a tempered distribution
u can be written as a finite sum u = ∑_{|α| ≤ m} ∂^α (v_α) with each
v_α ∈ L², then u ∈ H^{-m}. The witness function for H^{-m} is built
from the L² Fourier transforms of the v_α.
Convenience reordering of memLp_mul_of_bound_one_backward: if h is
a.e. bounded by 1 (and strongly measurable) and g ∈ L², then h · g
is in L².
Pointwise norm bound for the prefactor used in the explicit Sobolev
representation: the product sign(ξ^α) · (∑_β ‖ξ^β‖)⁻¹ · ⟨ξ⟩^m has complex
norm at most 1.
Dual L²/Fourier pairing identity: for f ∈ L² and a Schwartz
function φ, the integral of ξ^α · f · 𝓕⁻¹ φ equals the integral of
f · ∂^α φ.
Bridge step in the proof of the Sobolev derivative decomposition: given
the Fourier witness g for u ∈ H^{-m} and L² functions v_α summing
(after multiplication by ξ^α) to ⟨ξ⟩^m · g, the distribution u equals
∑_{|α| ≤ m} ∂^α v_α. The proof uses Fourier inversion together with
l2_monomial_fourierInv_schwartz_eq.
Pointwise algebraic identity for the explicit v_α used in the
Sobolev decomposition: if v_α(ξ) = sign(ξ^α) · (∑_β ‖ξ^β‖)⁻¹ · ⟨ξ⟩^m · g(ξ)
for every α of order at most m, then ∑_α ξ^α · v_α(ξ) = ⟨ξ⟩^m · g(ξ).
Converse direction of Proposition 9.7 of Melrose: every distribution
u ∈ H^{-m} admits a representation as a finite sum
u = ∑_{|α| ≤ m} ∂^α v_α with each v_α ∈ L². The proof constructs an
explicit v_α from the Fourier witness using the polar-decomposition
identity.
Proposition 9.7 of Melrose: a tempered distribution u belongs to
H^{-m} if and only if it can be written as a finite sum
u = ∑_{|α| ≤ m} ∂^α v_α with all v_α ∈ L².