The continuous characters of the circle are the Fourier monomials

Mathlib's fourier n : C(AddCircle T, ℂ) is developed as a family of L² monomials: the lemmas about it record how it behaves in the index n (fourier_add, fourier_neg) and what it contributes to the Fourier basis. Read the other way, as a family of characters of the group AddCircle T indexed by n, the two facts a representation-theoretic consumer needs are that the family is faithful (distinct indices give distinct characters, so the corresponding one-dimensional representations are pairwise inequivalent) and that it is exhaustive (there are no other continuous characters). This file proves both, and packages them as an isomorphism of groups between Multiplicative ℤ and the Pontryagin dual of the circle group.

Both halves need the period to be nondegenerate, and they need it to differing extents. Faithfulness holds as soon as T ≠ 0, and that hypothesis is carried explicitly. Exhaustiveness rests on Mathlib's Fourier analysis on AddCircle T, which is set up under [Fact (0 < T)], so that instance is assumed for the classification results and for the isomorphism of groups.

Faithfulness is elementary: two monomials already differ at the point T / 2 / (m - n). Exhaustiveness is where analysis enters. A continuous character χ is in particular a nonzero continuous function, so some Fourier coefficient fourierCoeff χ n is nonzero — that is Mathlib's fourierBasis, a Hilbert basis of L², together with the injectivity of the map C(AddCircle T, ℂ) → L². Translating that coefficient by y and using that both fourier (-n) and χ turn a sum into a product rewrites fourierCoeff χ n as fourier (-n) y * χ y * fourierCoeff χ n, whence fourier (-n) y * χ y = 1, and therefore χ y = fourier n y.

Nothing here assumes that χ takes values in the unit circle: on a compact group that is automatic, and here it comes out as a corollary, since a continuous character is a Fourier monomial.

TauCeti/RepresentationTheory/Compact/Circle.lean reads this classification for the circle group Multiplicative (AddCircle T) with [Fact (0 < T)], where the group is compact and the statement becomes that the continuous representations of the circle on ℂ are exactly the Fourier ones.

Main definitions

• TauCeti.fourierAddChar: the n-th Fourier monomial as a bundled additive character AddChar (AddCircle T) ℂ.
• TauCeti.fourierPontryaginDual: the n-th Fourier monomial as an element of the Pontryagin dual PontryaginDual (Multiplicative (AddCircle T)) of the circle group, i.e. as a continuous homomorphism to the unit circle.
• TauCeti.fourierPontryaginDualEquiv: the resulting isomorphism of groups between Multiplicative ℤ and that Pontryagin dual.

Main statements

• TauCeti.fourier_injective: n ↦ fourier n is injective, so distinct indices give distinct characters.
• ContinuousMap.eq_zero_of_forall_fourierCoeff_eq_zero: a continuous function on the circle all of whose Fourier coefficients vanish is the zero function.
• AddChar.exists_fourierAddChar_eq: every continuous additive character of the circle is a Fourier monomial.
• AddChar.norm_apply_eq_one_of_continuous: consequently a continuous additive character of the circle takes values of modulus one.

Tags

Fourier, additive circle, character, Pontryagin dual

theorem TauCeti.fourier_injective {T : ℝ} (hT : T ≠ 0) : Function.Injective fourier

Distinct indices give distinct Fourier monomials. At the point T / 2 / (m - n) the two monomials fourier m and fourier n differ by Complex.exp (π * I) = -1, so they are already different there. Only T ≠ 0 is needed: for T = 0 the circle is trivial and every monomial is the constant 1.

noncomputable def TauCeti.fourierAddChar {T : ℝ} (n : ℤ) : AddChar (AddCircle T) ℂ

The n-th Fourier monomial as a bundled additive character of the circle. It is Mathlib's AddCircle.toCircle_addChar precomposed with multiplication by n and postcomposed with the inclusion of the unit circle into ℂ; TauCeti.fourierAddChar_apply identifies its value with fourier n.

Equations

• TauCeti.fourierAddChar n = Circle.coeHom.compAddChar (AddCircle.toCircle_addChar.compAddMonoidHom (zsmulAddGroupHom n))

@[simp]

theorem TauCeti.fourierAddChar_apply {T : ℝ} (n : ℤ) (x : AddCircle T) : (fourierAddChar n) x = (fourier n) x

theorem TauCeti.continuous_fourierAddChar {T : ℝ} (n : ℤ) : Continuous ⇑(fourierAddChar n)

noncomputable def TauCeti.fourierPontryaginDual {T : ℝ} (n : ℤ) : PontryaginDual (Multiplicative (AddCircle T))

The n-th Fourier monomial as an element of the Pontryagin dual of the circle group. The circle group is Multiplicative (AddCircle T), and this character sends x to AddCircle.toCircle (n • x), the value of fourier n read in the unit circle rather than in ℂ; TauCeti.coe_fourierPontryaginDual identifies its value with fourier n.

Equations

• TauCeti.fourierPontryaginDual n = { toFun := fun (x : Multiplicative (AddCircle T)) => (n • Multiplicative.toAdd x).toCircle, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.coe_fourierPontryaginDual {T : ℝ} (n : ℤ) (x : Multiplicative (AddCircle T)) : ↑((fourierPontryaginDual n) x) = (fourier n) (Multiplicative.toAdd x)

theorem TauCeti.fourierPontryaginDual_injective {T : ℝ} (hT : T ≠ 0) : Function.Injective fourierPontryaginDual

Distinct indices give distinct elements of the Pontryagin dual: TauCeti.fourier_injective again.

theorem TauCeti.fourierAddChar_injective {T : ℝ} (hT : T ≠ 0) : Function.Injective fourierAddChar

Distinct indices give distinct additive characters: TauCeti.fourier_injective again.

theorem ContinuousMap.eq_zero_of_forall_fourierCoeff_eq_zero {T : ℝ} [Fact (0 < T)] (F : C(AddCircle T, ℂ)) (h : ∀ (n : ℤ), fourierCoeff (⇑F) n = 0) : F = 0

A continuous function on the circle with vanishing Fourier coefficients is zero. The separation statement for the Fourier coefficients of a continuous function, at the level of C(AddCircle T, ℂ) rather than of L²; it is what makes a nonzero continuous function have a nonzero Fourier coefficient.

theorem AddChar.exists_fourierAddChar_eq {T : ℝ} [Fact (0 < T)] (χ : AddChar (AddCircle T) ℂ) (hχ : Continuous ⇑χ) : ∃ (n : ℤ), TauCeti.fourierAddChar n = χ

Every continuous additive character of the circle is a Fourier monomial. Continuity is the only hypothesis: no unitarity is assumed, and none is needed. Together with TauCeti.fourierAddChar_injective this identifies the continuous characters of AddCircle T with ℤ, which is the content of TauCeti.fourierPontryaginDualEquiv.

theorem AddChar.existsUnique_fourierAddChar_eq {T : ℝ} [Fact (0 < T)] (χ : AddChar (AddCircle T) ℂ) (hχ : Continuous ⇑χ) : ∃! n : ℤ, TauCeti.fourierAddChar n = χ

The Fourier index of a continuous additive character of the circle is unique.

theorem AddChar.norm_apply_eq_one_of_continuous {T : ℝ} [Fact (0 < T)] (χ : AddChar (AddCircle T) ℂ) (hχ : Continuous ⇑χ) (x : AddCircle T) : ‖χ x‖ = 1

A continuous additive character of the circle takes values of modulus one. No unitarity hypothesis is needed anywhere above: continuity alone forces the character to be a Fourier monomial, and fourier n is valued in the unit circle.

noncomputable def TauCeti.fourierPontryaginDualEquiv {T : ℝ} [Fact (0 < T)] : Multiplicative ℤ ≃* PontryaginDual (Multiplicative (AddCircle T))

The Fourier monomials are the Pontryagin dual of the circle. The map n ↦ fourierPontryaginDual n is an isomorphism of groups from Multiplicative ℤ onto PontryaginDual (Multiplicative (AddCircle T)), the group of continuous characters of the circle group: it is a homomorphism because fourier (m + n) = fourier m * fourier n, injective by TauCeti.fourierPontryaginDual_injective, and surjective by AddChar.exists_fourierAddChar_eq.

The multiplicative type tags are what make this a statement about groups: the dual multiplies characters pointwise, and that multiplication corresponds to addition of Fourier indices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.fourierPontryaginDualEquiv_apply {T : ℝ} [Fact (0 < T)] (n : Multiplicative ℤ) : fourierPontryaginDualEquiv n = fourierPontryaginDual (Multiplicative.toAdd n)

@[simp]

theorem TauCeti.fourierPontryaginDualEquiv_apply_symm_apply {T : ℝ} [Fact (0 < T)] (ψ : PontryaginDual (Multiplicative (AddCircle T))) : fourierPontryaginDual (Multiplicative.toAdd (fourierPontryaginDualEquiv.symm ψ)) = ψ

The inverse of TauCeti.fourierPontryaginDualEquiv returns the Fourier index of a continuous character: the monomial at that index is the character one started from.