The circle Sobolev space H⁰ is L² of the circle

The Fourier-coefficient Sobolev space H^s of TauCeti/Analysis/Sobolev/Circle/Basic.lean has the weights (1 + |n|) ^ s, which are all 1 when s = 0. So H⁰ is the space ℓ²(ℤ) of square-summable coefficient sequences, and Mathlib's Fourier basis fourierBasis of L²(AddCircle T) identifies it with the square-integrable functions on the circle, normalized Haar measure, by Parseval's identity. Under this identification an element of H⁰ is the L² function whose Fourier coefficients are its coefficients, and for s > 1/2 the L² function of an element of H^s is its continuous representative CircleSobolev.toContinuousMap.

Operations on functions on the circle which are not diagonal in the Fourier basis, such as precomposition with a diffeomorphism of the circle, are defined on H⁰ through this identification.

Main definitions

• TauCeti.CircleSobolev.toLpₗᵢ T: the linear isometric equivalence H⁰ ≃ₗᵢ[ℂ] L²(AddCircle T).

Main statements

• TauCeti.CircleSobolev.fourierCoeff_toLpₗᵢ and TauCeti.CircleSobolev.coeff_toLpₗᵢ_symm: the Fourier coefficients of toLpₗᵢ T a are the coefficients of a.
• TauCeti.CircleSobolev.toLpₗᵢ_inclusion_eq_toLp_toContinuousMap: for s > 1/2 and a ∈ H^s, the L² function of a is the class of its continuous representative.

References

• Y. Katznelson, An Introduction to Harmonic Analysis, 3rd ed., Cambridge University Press, 2004, Chapter I (the Fourier coefficients of L² functions and Parseval's identity).

noncomputable def TauCeti.CircleSobolev.toLpₗᵢ (T : ℝ) [hT : Fact (0 < T)] : CircleSobolev 0 ℂ ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)

H⁰ is L² of the circle. The linear isometric equivalence between H⁰ and the space of square-integrable functions on AddCircle T, for normalized Haar measure, sending a coefficient sequence to the L² sum of its Fourier series.

@[simp]

theorem TauCeti.CircleSobolev.fourierCoeff_toLpₗᵢ (T : ℝ) [hT : Fact (0 < T)] (a : CircleSobolev 0 ℂ) (n : ℤ) : fourierCoeff (↑↑((toLpₗᵢ T) a)) n = a.coeff n

The Fourier coefficients of the L² function of a ∈ H⁰ are the coefficients of a.

@[simp]

theorem TauCeti.CircleSobolev.coeff_toLpₗᵢ_symm (T : ℝ) [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) (n : ℤ) : ((toLpₗᵢ T).symm f).coeff n = fourierCoeff (↑↑f) n

The coefficients of the element of H⁰ attached to an L² function are its Fourier coefficients.

@[simp]

theorem TauCeti.CircleSobolev.toLpₗᵢ_single (T : ℝ) [hT : Fact (0 < T)] (n : ℤ) (x : ℂ) : (toLpₗᵢ T) ((single n) x) = x • fourierLp 2 n

The Fourier monomial x e^{inθ} of H⁰ is the L² Fourier mode x e_n.

theorem TauCeti.CircleSobolev.toLpₗᵢ_inclusion_eq_toLp_toContinuousMap (T : ℝ) [hT : Fact (0 < T)] {s : ℝ} (hs : 1 / 2 < s) (a : CircleSobolev s ℂ) : (toLpₗᵢ T) ((inclusion ⋯) a) = (ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) ((toContinuousMap T hs) a)

The L² function of a continuous element. For s > 1/2 and a ∈ H^s, the L² function of a, regarded as an element of H⁰, is the class of its continuous representative.