Discrete Fourier transform in the compact normalisation

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

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

The discrete Fourier transform.

Equations

• cft f ψ = nl2Inner (⇑ψ) f

theorem cft_apply {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : cft f ψ = nl2Inner (⇑ψ) f

@[simp]

theorem cft_zero {α : Type u_1} [AddCommGroup α] [Fintype α] : cft 0 = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Parseval-Plancherel identity for the discrete Fourier transform.

@[simp]

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

Parseval-Plancherel identity for the discrete Fourier transform.

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

Fourier inversion for the discrete Fourier transform.

theorem dft_cft_doubleDualEmb {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : dft (cft f) (AddChar.doubleDualEmb a) = f (-a)

theorem cft_dft_doubleDualEmb {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : cft (dft f) (AddChar.doubleDualEmb a) = f (-a)

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

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

theorem cft_injective {α : Type u_1} [AddCommGroup α] [Fintype α] : Function.Injective cft

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem cft_trivNChar {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] : cft trivNChar = 1

@[simp]

theorem cft_one {α : Type u_1} [AddCommGroup α] [Fintype α] : cft 1 = trivChar

@[simp]

theorem cft_indicate_zero {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (s : Finset α) : cft (𝟭 s) 0 = s.dens

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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