Discrete Fourier transform

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

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

The discrete Fourier transform.

Equations

• dft f ψ = RCLike.wInner 1 (⇑ψ) f

theorem dft_apply {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : dft f ψ = RCLike.wInner 1 (⇑ψ) 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} [AddCommGroup α] [Fintype α] {𝕝 : Type u_3} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 ℂ] [StarModule 𝕝 ℂ] [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝) (f : α → ℂ) : dft (c • f) = c • dft f

@[simp]

theorem wInner_cWeight_dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f g : α → ℂ) : RCLike.wInner RCLike.cWeight (dft f) (dft g) = RCLike.wInner 1 f g

Parseval-Plancherel identity for the discrete Fourier transform.

@[simp]

theorem cL2Norm_dft {α : Type u_1} [AddCommGroup α] [Fintype α] [MeasurableSpace α] [DiscreteMeasurableSpace α] (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.univ.expect fun (ψ : AddChar α ℂ) => dft f ψ * ψ a) = f a

Fourier inversion for the discrete Fourier transform.

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

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 ∘ ⇑AddChar.doubleDualEquiv.symm ∘ 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)

theorem dft_comp_neg_apply {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (ψ : AddChar α ℂ) : dft (fun (x : α) => f (-x)) ψ = dft f (-ψ)

@[simp]

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

@[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