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 {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) : AddChar G ℂ → ℂ

The discrete Fourier transform.

Equations

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

theorem dft_apply {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (ψ : AddChar G ℂ) : dft f ψ = RCLike.wInner 1 (⇑ψ) f

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem dft_smul {G : Type u_1} [AddCommGroup G] [Fintype G] {𝕝 : Type u_2} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 ℂ] [StarModule 𝕝 ℂ] [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝) (f : G → ℂ) : dft (c • f) = c • dft f

@[simp]

theorem wInner_cWeight_dft {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : 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 {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (f : G → ℂ) : ‖dft f‖ₙ_[2] = ‖f‖_[2]

Parseval-Plancherel identity for the discrete Fourier transform.

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

Fourier inversion for the discrete Fourier transform.

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

Fourier inversion for the discrete Fourier transform.

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem dft_indicator_one_zero {G : Type u_1} [AddCommGroup G] [Fintype G] (A : Finset G) : dft ((↑A).indicator fun (x : G) => 1) 0 = ↑A.card

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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