Fourier-coefficient Sobolev spaces on the circle #
For a real number s and a complex normed space E, the Sobolev space H^s of E-valued
functions on a circle is described through Fourier coefficients: it consists of the sequences
a : ℤ → E with
‖a‖² = ∑ₙ (1 + |n|) ^ (2 s) ‖a n‖² < ∞.
The order s is an arbitrary real number, so this covers the fractional and negative orders
needed for boundary traces. These spaces are the boundary function spaces on which the Hardy
decompositions of a cut Riemann surface are carried out (Robbin–Salamon).
The space is TauCeti.CircleSobolev s E, an extensional structure recording the coefficient
sequence coeff. Multiplication by the weights (1 + |n|) ^ s identifies it isometrically with
ℓ²(ℤ, E) (CircleSobolev.toℓ2ₗᵢ), which supplies its norm, and its completeness and inner
product when E has them.
Main definitions #
TauCeti.CircleSobolev.weight s n = (1 + |n|) ^ s, the Sobolev weight of the frequencyn.TauCeti.CircleSobolev s E: the Sobolev space of orders, with norm‖a‖² = ∑ₙ weight (2 s) n * ‖a.coeff n‖²(CircleSobolev.hasSum_norm_sq).TauCeti.CircleSobolev.single n x: the Fourier monomialx e^{inθ}.TauCeti.CircleSobolev.reflect: the linear isometric reflectionn ↦ -nof the Fourier coefficients.TauCeti.CircleSobolev.inclusion: the continuous inclusionH^s → H^tfort ≤ s.TauCeti.CircleSobolev.restrict: a continuous linear mapH^t → H^t'carryingH^sintoH^s', as a continuous linear mapH^s → H^s'(by the closed graph theorem), andTauCeti.CircleSobolev.restrictEquiv, its analogue for continuous linear isomorphisms.TauCeti.CircleSobolev.toContinuousMap: fors > 1/2, the continuous function onAddCircle Tgiven by the uniformly convergent Fourier series.
Main statements #
TauCeti.CircleSobolev.weight_add_le: Peetre's inequality(1 + |m + n|) ^ s ≤ (1 + |m|) ^ |s| (1 + |n|) ^ s, for every reals.TauCeti.CircleSobolev.hasSum_single: the Fourier series of an element converges to it inH^s, so trigonometric polynomials are dense (CircleSobolev.dense_finite_support_coeff). Continuous linear maps out ofH^sare therefore determined by their values on Fourier monomials (CircleSobolev.continuousLinearMap_ext_single).TauCeti.CircleSobolev.tendsto_of_tendsto_coeff: dominated convergence inH^s, convergence inH^sfrom convergence of the Fourier coefficients under a summable domination.TauCeti.CircleSobolev.isCompactOperator_inclusion: fort < sand finite-dimensionalE, the inclusionH^s → H^tis compact (Rellich's theorem).TauCeti.CircleSobolev.exists_norm_inclusion_le: forr ≤ t < s,‖a‖_{H^t} ≤ ε ‖a‖_{H^s} + C_ε ‖a‖_{H^r}for everyε > 0(Ehrling's inequality).TauCeti.CircleSobolev.tsum_norm_coeff_le: fors > 1/2, the Fourier coefficients are absolutely summable, with∑ₙ ‖a.coeff n‖ ≤ (∑ₙ (1 + |n|) ^ (-2 s)) ^ (1/2) ‖a‖.TauCeti.CircleSobolev.fourierCoeff_toContinuousMap: fors > 1/2, the continuous function attached toahas Fourier coefficientsa.coeff; in particularH^sembeds continuously into the continuous functions on the circle.TauCeti.CircleSobolev.toContinuousMap_equivAddCircle: the continuous functions attached toaon circles of different lengths correspond under rescaling.
References #
- M. E. Taylor, Partial Differential Equations I, Chapter 3 (Sobolev spaces on the torus via Fourier series).
- J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699 (boundary Sobolev spaces of Hardy decompositions).
The Sobolev weight (1 + |n|) ^ s of the frequency n.
Instances For
Peetre's inequality: (1 + |m + n|) ^ s ≤ (1 + |m|) ^ |s| (1 + |n|) ^ s for every real
s. Shifting frequencies by m therefore changes the weights of every order s by at most the
factor (1 + |m|) ^ |s|.
The Sobolev space H^s of E-valued functions on the circle, described by Fourier
coefficients: a sequence coeff : ℤ → E with ∑ₙ (1 + |n|) ^ (2 s) ‖coeff n‖² < ∞.
- coeff : ℤ → E
The
n-th Fourier coefficient. The weighted coefficients
(1 + |n|) ^ s • coeff nare square-summable.
Instances For
The vector space structure #
The real scalar multiplication, restricted from the complex one, acts on the coefficients.
The Fourier coefficient sequence, as a linear map.
Instances For
The identification with ℓ² #
An element of ℓ²(ℤ, E) divided by the weights (1 + |n|) ^ s is a Fourier-coefficient
sequence of order s.
Instances For
Multiplication by the weights (1 + |n|) ^ s, an isometric isomorphism onto ℓ²(ℤ, E)
(see CircleSobolev.toℓ2ₗᵢ).
Instances For
A sequence is the coefficient sequence of an element of H^s exactly when its weighted
sequence is square-summable.
A sequence lies in H^s exactly when its weighted norms are square-summable.
The isometric identification of H^s with ℓ²(ℤ, E) by the weights (1 + |n|) ^ s.
Instances For
The squared norm of H^s is the sum of the squared weighted coefficient norms.
Parseval's identity for H^s in ℝ≥0∞: the squared norm is the weighted sum of the squared
coefficient norms.
A coefficientwise bound of weighted norms gives the corresponding bound on the norms, possibly between different orders.
The n-th Fourier coefficient of an element of H^s is bounded by (1 + |n|) ^ (-s) times
its norm.
The n-th Fourier coefficient is a continuous linear functional on H^s.
Instances For
A sequence whose weighted norms of order t are bounded by a multiple of the weighted norms of
order s of an element of H^s is the coefficient sequence of an element of H^t.
The reflection n ↦ -n of the Fourier coefficients, as a linear isometric automorphism of
H^s. It corresponds to the reflection x ↦ -x of the circle.
Instances For
Dominated convergence in H^s: if the Fourier coefficients of b x converge to those of a
and the squared weighted norms ((1 + |n|) ^ s ‖(b x).coeff n - a.coeff n‖) ^ 2 are eventually
dominated by a summable sequence, then b x converges to a in H^s.
Hilbert structure #
The inner product of H^s is ∑ₙ (1 + |n|) ^ (2 s) ⟪a.coeff n, b.coeff n⟫.
Fourier monomials and density of trigonometric polynomials #
The Fourier monomial x e^{inθ} in H^s, as a continuous linear map in x.
Instances For
The Fourier series of an element of H^s converges to it in H^s.
Continuous linear maps out of H^s are determined by their values on the Fourier monomials.
Trigonometric polynomials, the elements of H^s with finitely many nonzero Fourier
coefficients, are dense in H^s.
Inclusions between the Sobolev spaces #
The continuous inclusion H^s → H^t for t ≤ s, which keeps the Fourier coefficients.
Instances For
Restriction of an operator to smaller Sobolev spaces. A continuous linear map
P : H^t → H^t' carrying H^s into H^s', for t ≤ s and t' ≤ s', as a continuous linear map
H^s → H^s'. It is continuous by the closed graph theorem.
Instances For
In H^t', restrict is P: the inclusion of the image of u is P applied to the inclusion
of u.
Restriction of an isomorphism to smaller Sobolev spaces. A continuous linear isomorphism
P : H^t → H^t' such that P carries H^s into H^s' and P⁻¹ carries H^s' into H^s, for
t ≤ s and t' ≤ s', as a continuous linear isomorphism H^s → H^s'.
Instances For
In H^t', restrictEquiv is P.
In H^t, the inverse of restrictEquiv is the inverse of P.
Rellich's theorem on the circle: the inclusion H^s → H^t is a compact operator for
t < s when E is finite-dimensional.
Ehrling's inequality on the circle: for r ≤ t < s, the H^t norm is bounded by an
arbitrarily small multiple of the H^s norm plus a multiple of the weaker H^r norm.
Absolute convergence and continuity for s > 1/2 #
For s > 1/2 the Fourier coefficients of an element of H^s are absolutely summable.
For s > 1/2, the ℓ¹ norm of the Fourier coefficients is bounded by the H^s norm:
∑ₙ ‖a.coeff n‖ ≤ (∑ₙ (1 + |n|) ^ (-2 s)) ^ (1/2) ‖a‖.
For s > 1/2, the continuous function on AddCircle T attached to an element of H^s:
the sum of its uniformly convergent Fourier series ∑ₙ a.coeff n e^{2πinx/T}.
Instances For
The Fourier series of an element of H^s, s > 1/2, converges uniformly to its continuous
function.
For 1/2 < t ≤ s, the continuous function attached to a ∈ H^s does not depend on whether
a is regarded as an element of H^s or of H^t.
For s > 1/2, the continuous function attached to a ∈ H^s has Fourier coefficients
a.coeff.
For s > 1/2, the continuous representatives of a ∈ H^s on circles of different lengths
correspond under the rescaling AddCircle.equivAddCircle.
For s > 1/2 and an open set U, the elements of H^s whose continuous representatives take
values in U form an open subset of H^s.