Units and spectrum of the circle Sobolev algebras H^s, s > 1/2

For s > 1/2 and a complete normed ℂ-algebra A, the Fourier-coefficient Sobolev space H^s(A) of the circle is an algebra under the pointwise product (TauCeti.CircleSobolev.toContinuousMapAlgHom). This file proves Wiener's lemma for it when A is commutative: an element of H^s(A) is invertible in H^s(A) as soon as its continuous representative takes invertible values everywhere. For A = ℂ this says that 1 / u ∈ H^s for every nowhere-vanishing u ∈ H^s; that is, the holomorphic map z ↦ 1 / z on ℂ \ {0} acts on the elements of H^s with values in ℂ \ {0}, and the resolvents (z - u)⁻¹ exist in H^s for every z off the range of u.

The proof is Gelfand's. The multiplication operators b ↦ a * b form a closed subalgebra of the bounded operators on H^s(A), isomorphic to H^s(A); it is a Banach algebra, commutative when A is. A non-invertible element of H^s(A) is therefore annihilated by an algebra homomorphism φ : H^s(A) → ℂ. Such a φ is continuous, and it is determined by the value w = φ(e^{iθ}) together with its restriction to the constant functions; the polynomial growth ‖e^{inθ}‖ = (1 + |n|) ^ s of the monomials in H^s forces |w| = 1, so φ is evaluation at the point x of the circle with e^{ix} = w, followed by an algebra homomorphism A → ℂ.

Main statements

• TauCeti.CircleSobolev.continuous_algHom: every algebra homomorphism H^s(A) → ℂ is continuous.
• TauCeti.CircleSobolev.exists_forall_apply_eq_apply_single_zero: every algebra homomorphism φ : H^s(A) → ℂ factors through evaluation at a point x of the circle, as φ a = φ (a(x)), with a(x) regarded as a constant function; for A = ℂ, TauCeti.CircleSobolev.exists_forall_apply_eq_toContinuousMap_apply says that φ is evaluation at x.
• TauCeti.CircleSobolev.isUnit_iff_forall_isUnit (Wiener's lemma): for commutative A, a is a unit of H^s(A) if and only if a(x) is a unit of A for every x. Equivalently, toContinuousMap is a local homomorphism H^s(A) → C(AddCircle T, A) (TauCeti.CircleSobolev.isLocalHom_toContinuousMapAlgHom), so it commutes with Ring.inverse (TauCeti.CircleSobolev.toContinuousMap_ringInverse).
• TauCeti.CircleSobolev.spectrum_toContinuousMap: for commutative A, a and its continuous representative have the same spectrum. For A = ℂ, TauCeti.CircleSobolev.spectrum_eq_range identifies it with the range of the continuous representative, and TauCeti.CircleSobolev.isUnit_iff_forall_ne_zero says that the units are the nowhere-vanishing elements.

References

• N. Wiener, Tauberian theorems, Ann. of Math. 33 (1932), 1–100, for the corresponding statement for absolutely convergent Fourier series.
• I. M. Gelfand, Normierte Ringe, Rec. Math. [Mat. Sbornik] N. S. 9 (1941), 3–24, and Y. Katznelson, An Introduction to Harmonic Analysis, 3rd ed., Chapter VIII, for the proof through the maximal ideals of a commutative Banach algebra.

The algebra of multiplication operators

Characters of H^s(A)

theorem TauCeti.CircleSobolev.continuous_algHom {s : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (φ : CircleSobolev s A →ₐ[ℂ] ℂ) : Continuous ⇑φ

Every algebra homomorphism H^s(A) → ℂ is continuous.

theorem TauCeti.CircleSobolev.exists_forall_apply_eq_apply_single_zero {s : ℝ} {A : Type u_1} [NormedRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (φ : CircleSobolev s A →ₐ[ℂ] ℂ) : ∃ (x : AddCircle T), ∀ (a : CircleSobolev s A), φ a = φ ((single 0) (((toContinuousMap T ⋯) a) x))

Characters of H^s(A). Every algebra homomorphism φ : H^s(A) → ℂ factors through evaluation at a point x of the circle: φ a = φ (a(x)), where the value a(x) ∈ A is regarded as a constant function.

Wiener's lemma

theorem TauCeti.CircleSobolev.isUnit_iff_forall_isUnit {s : ℝ} {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] {a : CircleSobolev s A} : IsUnit a ↔ ∀ (x : AddCircle T), IsUnit (((toContinuousMap T ⋯) a) x)

Wiener's lemma for H^s(A), s > 1/2. An element of H^s(A) is a unit if and only if its continuous representative takes invertible values at every point of the circle.

instance TauCeti.CircleSobolev.isLocalHom_toContinuousMapAlgHom {s : ℝ} {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] : IsLocalHom (toContinuousMapAlgHom T)

toContinuousMap reflects units: an element of H^s(A) whose continuous representative is a unit of C(AddCircle T, A) is a unit of H^s(A).

@[simp]

theorem TauCeti.CircleSobolev.isUnit_toContinuousMap_iff {s : ℝ} {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] {a : CircleSobolev s A} : IsUnit ((toContinuousMap T ⋯) a) ↔ IsUnit a

An element of H^s(A) is a unit exactly when its continuous representative is a unit of C(AddCircle T, A).

@[simp]

theorem TauCeti.CircleSobolev.toContinuousMap_ringInverse {s : ℝ} {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (a : CircleSobolev s A) : (toContinuousMap T ⋯) (Ring.inverse a) = Ring.inverse ((toContinuousMap T ⋯) a)

The continuous representative of the inverse 1 / a is the inverse of the continuous representative of a; both sides are 0 when a is not a unit.

@[simp]

theorem TauCeti.CircleSobolev.spectrum_toContinuousMap {s : ℝ} {A : Type u_1} [NormedCommRing A] [NormedAlgebra ℂ A] [CompleteSpace A] [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (a : CircleSobolev s A) : spectrum ℂ ((toContinuousMap T ⋯) a) = spectrum ℂ a

An element of H^s(A) and its continuous representative have the same spectrum.

theorem TauCeti.CircleSobolev.exists_forall_apply_eq_toContinuousMap_apply {s : ℝ} [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (φ : CircleSobolev s ℂ →ₐ[ℂ] ℂ) : ∃ (x : AddCircle T), ∀ (a : CircleSobolev s ℂ), φ a = ((toContinuousMap T ⋯) a) x

Characters of H^s. Every algebra homomorphism H^s(ℂ) → ℂ is evaluation of the continuous representative at a point of the circle.

theorem TauCeti.CircleSobolev.isUnit_iff_forall_ne_zero {s : ℝ} [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] {a : CircleSobolev s ℂ} : IsUnit a ↔ ∀ (x : AddCircle T), ((toContinuousMap T ⋯) a) x ≠ 0

Wiener's lemma for H^s, s > 1/2. An element of H^s(ℂ) is a unit if and only if its continuous representative vanishes nowhere.

theorem TauCeti.CircleSobolev.spectrum_eq_range {s : ℝ} [hs : Fact (1 / 2 < s)] (T : ℝ) [Fact (0 < T)] (a : CircleSobolev s ℂ) : spectrum ℂ a = Set.range ⇑((toContinuousMap T ⋯) a)

The spectrum of an element of H^s(ℂ), s > 1/2, is the range of its continuous representative.