Discrete Fourier transform

This file defines the discrete Fourier transform and shows the Parseval-Plancherel identity and Fourier inversion formula for it.

theorem Complex.le_of_eq_sum_of_eq_sum_norm {ι : Type u_1} {a : ℝ} {b : ℝ} (f : ι → ℂ) (s : Finset ι) (ha₀ : 0 ≤ a) (ha : ↑a = Finset.sum s fun (i : ι) => f i) (hb : ↑b = Finset.sum s fun (i : ι) => ↑‖f i‖) : a ≤ b

def dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : AddChar α ℂ → ℂ

The discrete Fourier transform.

Equations

• dft f ψ = l2Inner (⇑ψ) f

theorem dft_apply {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = l2Inner (⇑ψ) f

@[simp]

theorem dft_zero {α : Type u_1} [AddCommGroup α] [Fintype α] : dft 0 = 0

@[simp]

theorem dft_add {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (g : α → ℂ) : dft (f + g) = dft f + dft g

@[simp]

theorem dft_neg {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : dft (-f) = -dft f

@[simp]

theorem dft_sub {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (g : α → ℂ) : dft (f - g) = dft f - dft g

@[simp]

theorem dft_const {α : Type u_1} [AddCommGroup α] [Fintype α] {ψ : AddChar α ℂ} (a : ℂ) (hψ : ψ ≠ 0) : dft (Function.const α a) ψ = 0

@[simp]

theorem dft_smul {α : Type u_1} {γ : Type u_2} [AddCommGroup α] [Fintype α] [DistribSMul γ ℂ] [Star γ] [StarModule γ ℂ] [SMulCommClass γ ℂ ℂ] (c : γ) (f : α → ℂ) : dft (c • f) = c • dft f

@[simp]

theorem nl2Inner_dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (g : α → ℂ) : nl2Inner (dft f) (dft g) = l2Inner f g

Parseval-Plancherel identity for the discrete Fourier transform.

@[simp]

theorem nl2Norm_dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2]

Parseval-Plancherel identity for the discrete Fourier transform.

theorem dft_inversion {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : (Finset.expect Finset.univ fun (ψ : AddChar α ℂ) => dft f ψ * ψ a) = f a

Fourier inversion for the discrete Fourier transform.

theorem dft_inversion' {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : (Finset.sum Finset.univ fun (ψ : AddChar α ℂ) => dft f ψ * ψ a) = ↑(Fintype.card α) * f a

Fourier inversion for the discrete Fourier transform.

theorem dft_dft_doubleDualEmb {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : dft (dft f) (AddChar.doubleDualEmb a) = ↑(Fintype.card α) * f (-a)

theorem dft_dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : dft (dft f) = ↑(Fintype.card α) * f ∘ ⇑(AddEquiv.symm AddChar.doubleDualEquiv) ∘ Neg.neg

theorem dft_injective {α : Type u_1} [AddCommGroup α] [Fintype α] : Function.Injective dft

theorem dft_inv {α : Type u_1} [AddCommGroup α] [Fintype α] {f : α → ℂ} (ψ : AddChar α ℂ) (hf : IsSelfAdjoint f) : dft f ψ⁻¹ = (starRingEnd ℂ) (dft f ψ)

@[simp]

theorem dft_conj {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : dft ((starRingEnd (α → ℂ)) f) ψ = (starRingEnd ℂ) (dft f ψ⁻¹)

theorem dft_conjneg_apply {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : dft (conjneg f) ψ = (starRingEnd ℂ) (dft f ψ)

@[simp]

theorem dft_conjneg {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : dft (conjneg f) = (starRingEnd (AddChar α ℂ → ℂ)) (dft f)

@[simp]

theorem dft_balance {α : Type u_1} [AddCommGroup α] [Fintype α] {ψ : AddChar α ℂ} (f : α → ℂ) (hψ : ψ ≠ 0) : dft (Finset.balance f) ψ = dft f ψ

theorem dft_dilate {α : Type u_1} [AddCommGroup α] [Fintype α] {n : ℕ} (f : α → ℂ) (ψ : AddChar α ℂ) (hn : Nat.Coprime (Fintype.card α) n) : dft (dilate f n) ψ = dft f (ψ ^ n)

@[simp]

theorem dft_trivChar {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] : dft trivChar = 1

@[simp]

theorem dft_one {α : Type u_1} [AddCommGroup α] [Fintype α] : dft 1 = Fintype.card α • trivChar

@[simp]

theorem dft_indicate_zero {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (A : Finset α) : dft (𝟭 A) 0 = ↑A.card

theorem dft_conv_apply {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (g : α → ℂ) (ψ : AddChar α ℂ) : dft (f ∗ g) ψ = dft f ψ * dft g ψ

theorem dft_dconv_apply {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (g : α → ℂ) (ψ : AddChar α ℂ) : dft (f ○ g) ψ = dft f ψ * (starRingEnd ℂ) (dft g ψ)

@[simp]

theorem dft_conv {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (g : α → ℂ) : dft (f ∗ g) = dft f * dft g

@[simp]

theorem dft_dconv {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (g : α → ℂ) : dft (f ○ g) = dft f * (starRingEnd (AddChar α ℂ → ℂ)) (dft g)

@[simp]

theorem dft_iterConv {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (n : ℕ) : dft (f ∗^ n) = dft f ^ n

@[simp]

theorem dft_iterConv_apply {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f : α → ℂ) (n : ℕ) (ψ : AddChar α ℂ) : dft (f ∗^ n) ψ = dft f ψ ^ n

theorem lpNorm_conv_le_lpNorm_dconv {α : Type u_1} [AddCommGroup α] [Fintype α] {n : ℕ} [DecidableEq α] (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℂ) : ‖f ∗ f‖_[↑n] ≤ ‖f ○ f‖_[↑n]

theorem lpNorm_conv_le_lpNorm_dconv' {α : Type u_1} [AddCommGroup α] [Fintype α] {n : ℕ} [DecidableEq α] (hn₀ : n ≠ 0) (hn : Even n) (f : α → ℝ) : ‖f ∗ f‖_[↑n] ≤ ‖f ○ f‖_[↑n]