Uniqueness of Fourier coefficients

TheoremUniqueness of Fourier coefficients in L²#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). If an element \(F\) of \(L^2(\mathbb{R}/T\mathbb{Z}, \mu; \mathbb{C})\) has Fourier coefficients \(\hat F(n) = \int e^{-2\pi i n t / T} F(t)\,d\mu(t)\) equal to \(0\) for every \(n \in \mathbb{Z}\), then \(F = 0\) in \(L^2(\mathbb{R}/T\mathbb{Z}, \mu; \mathbb{C})\).

theorem eq_zero_of_fourierCoeff_eq_zero_Lp
    {F : Lp ℂ 2 (AddCircle.haarAddCircle (T := T))}
    (h : ∀ n : ℤ, fourierCoeff F n = 0) :
    F = 0

Used by 1

Used byUniqueness of Fourier coefficients for continuous functions

TheoremUniqueness of Fourier coefficients for continuous functions#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). If a continuous function \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) has Fourier coefficients \(\hat f(n) = \int e^{-2\pi i n t / T} f(t)\,d\mu(t)\) equal to \(0\) for every \(n \in \mathbb{Z}\), then \(f = 0\).

theorem eq_zero_of_fourierCoeff_eq_zero
    {f : C(AddCircle T, ℂ)} (h : ∀ n : ℤ, fourierCoeff f n = 0) : f = 0

Uses 1 · Used by 1

Proof usesUniqueness of Fourier coefficients in L²

Used byUniqueness of Fourier coefficients on an interval

TheoremFourier coefficients determine a continuous function#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). For a function \(h : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) and \(n \in \mathbb{Z}\), let \(\hat h(n) = \int e^{-2\pi i n t / T} h(t)\,d\mu(t)\) be the \(n\)-th Fourier coefficient of \(h\). If two continuous functions \(f, g : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) satisfy \(\hat f(n) = \hat g(n)\) for every \(n \in \mathbb{Z}\), then \(f = g\).

theorem eq_of_fourierCoeff_eq
    {f g : C(AddCircle T, ℂ)} (h : ∀ n : ℤ, fourierCoeff f n = fourierCoeff g n) :
    f = g

Used by 1

Used byInjectivity of the Fourier-coefficient map

TheoremInjectivity of the Fourier-coefficient map#✓fully proved

Let \(T > 0\) and let \(\mu\) be the Haar probability measure on the circle \(\mathbb{R}/T\mathbb{Z}\). The map sending a continuous function \(f : \mathbb{R}/T\mathbb{Z} \to \mathbb{C}\) to its sequence of Fourier coefficients \((\hat f(n))_{n \in \mathbb{Z}}\), where \(\hat f(n) = \int e^{-2\pi i n t / T} f(t)\,d\mu(t)\), is injective.

theorem fourierCoeff_injective :
    Function.Injective (fun f : C(AddCircle T, ℂ) => fun n : ℤ => fourierCoeff f n)

Uses 1

Proof usesFourier coefficients determine a continuous function

TheoremUniqueness of Fourier coefficients on an interval#✓fully proved

Let \(a, T \in \mathbb{R}\) with \(T > 0\), and let \(f : \mathbb{R} \to \mathbb{C}\) be continuous with \(f(a) = f(a + T)\). If the Fourier coefficients of \(f\) on \([a, a + T]\),

\[\hat f(n) = \frac{1}{T} \int_a^{a+T} e^{-2\pi i n x / T} f(x)\,dx,\]

are \(0\) for every \(n \in \mathbb{Z}\), then \(f(x) = 0\) for every \(x \in [a, a + T]\).

This is a corollary of uniqueness on the circle: the endpoint condition makes \(f\) on \([a, a + T]\) descend to a continuous function on \(\mathbb{R}/T\mathbb{Z}\).

theorem eq_zero_of_fourierCoeffOn_eq_zero {a T : ℝ} (hT : 0 < T)
    {f : ℝ → ℂ} (hf : Continuous f) (hper : f a = f (a + T))
    (h : ∀ n : ℤ,
      fourierCoeffOn (lt_add_of_pos_right a hT) f n = 0) :
    ∀ x ∈ Set.Icc a (a + T), f x = 0

Uses 1

Proof usesUniqueness of Fourier coefficients for continuous functions

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.