Compact Fourier transform

This file defines the compact Fourier transform for finite groups 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 ψ = RCLike.wInner RCLike.cWeight (⇑ψ) f

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

@[simp]

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

Parseval-Plancherel identity for the discrete Fourier transform.

@[simp]

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

Parseval-Plancherel identity for the discrete Fourier transform.

theorem cft_inversion {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) (a : α) : ∑ ψ : AddChar α ℂ, cft f ψ * ψ a = f a

Fourier inversion for the discrete Fourier transform.

theorem cft_inversion' {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : ∑ ψ : AddChar α ℂ, cft f ψ • ⇑ψ = f

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

theorem cft_dft {α : Type u_1} [AddCommGroup α] [Fintype α] (f : α → ℂ) : cft (dft f) = f ∘ ⇑AddChar.doubleDualEquiv.symm ∘ 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 (Fintype.balance f) ψ = cft f ψ

@[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_cconv_apply {α : Type u_1} [AddCommGroup α] [Fintype α] [DecidableEq α] (f g : α → ℂ) (ψ : AddChar α ℂ) : cft (f ∗ₙ g) ψ = cft f ψ * cft g ψ

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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