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 ψ = ⟪⇑ψ, f⟫_[ℂ]

theorem dft_apply {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (ψ : AddChar G ℂ) : dft f ψ = ⟪⇑ψ, f⟫_[ℂ]

theorem norm_dft_le_dL1Norm {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (f : G → ℂ) (ψ : AddChar G ℂ) : ‖dft f ψ‖ ≤ ‖f‖_[1]

A special case of the Hausdorff-Young inequality for the discrete Fourier transform.

theorem cLinftyNorm_dft_le_dL1Norm {G : Type u_1} [AddCommGroup G] [Fintype G] [MeasurableSpace G] [DiscreteMeasurableSpace G] (f : G → ℂ) : ‖dft f‖ₙ_[⊤] ≤ ‖f‖_[1]

A special case of the Hausdorff-Young inequality for the discrete Fourier transform.

@[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 → ℂ) : ⟪dft f, dft g⟫ₙ_[ℂ] = ⟪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.

@[simp]

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

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 expect_iInf_ker_eq_expect_ite {G : Type u_1} [AddCommGroup G] [Fintype G] {Δ : Set (AddChar G ℂ)} [DecidablePred fun (x : AddChar G ℂ) => x ∈ AddSubgroup.closure Δ] {V : AddSubgroup G} [Fintype ↥V] (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker) (f : G → ℂ) : ((↑V).toFinset.expect fun (x : G) => f x) = Finset.univ.expect fun (ψ : AddChar G ℂ) => if ψ ∈ AddSubgroup.closure Δ then dft f ψ else 0

theorem expect_iInf_ker_sub_map_zero_eq_expect_ite {G : Type u_1} [AddCommGroup G] [Fintype G] {Δ : Set (AddChar G ℂ)} [DecidablePred fun (x : AddChar G ℂ) => x ∈ AddSubgroup.closure Δ] {V : AddSubgroup G} [Fintype ↥V] (hV : V = ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker) (f : G → ℂ) : ((↑V).toFinset.expect fun (x : G) => f x) - f 0 = Finset.univ.expect fun (ψ : AddChar G ℂ) => if ψ ∈ AddSubgroup.closure Δ then 0 else -dft f ψ

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