Documentation

APAP.Prereqs.FourierTransform.Compact

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.

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

The discrete Fourier transform.

Equations
Instances For
    source
    theorem cft_apply {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (ψ : AddChar G ℂ) :
    cft f ψ = ⟪⇑ψ, f⟫ₙ_[ℂ]
    source
    @[simp]
    theorem cft_zero {G : Type u_1} [AddCommGroup G] [Fintype G] :
    cft 0 = 0
    source
    @[simp]
    theorem cft_add {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : G → ℂ) :
    cft (f + g) = cft f + cft g
    source
    @[simp]
    theorem cft_neg {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    cft (-f) = -cft f
    source
    @[simp]
    theorem cft_sub {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : G → ℂ) :
    cft (f - g) = cft f - cft g
    source
    @[simp]
    theorem cft_const {G : Type u_1} [AddCommGroup G] [Fintype G] {ψ : AddChar G ℂ} (a : ℂ) (hψ : ψ ≠ 0) :
    cft (Function.const G a) ψ = 0
    source
    @[simp]
    theorem cft_smul {G : Type u_1} [AddCommGroup G] [Fintype G] {𝕝 : Type u_3} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 ℂ] [StarModule 𝕝 ℂ] [IsScalarTower 𝕝 ℂ ℂ] (c : 𝕝) (f : G → ℂ) :
    cft (c • f) = c • cft f
    source
    @[simp]
    theorem wInner_one_cft {G : Type u_1} [AddCommGroup G] [Fintype G] (f g : G → ℂ) :
    ⟪cft f, cft g⟫_[ℂ] = ⟪f, g⟫ₙ_[ℂ]

    Parseval-Plancherel identity for the discrete Fourier transform.

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

    Parseval-Plancherel identity for the discrete Fourier transform.

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

    Fourier inversion for the discrete Fourier transform.

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

    Fourier inversion for the discrete Fourier transform.

    source
    theorem dft_cft_doubleDualEmb {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (a : G) :
    dft (cft f) (AddChar.doubleDualEmb a) = f (-a)
    source
    theorem cft_dft_doubleDualEmb {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (a : G) :
    cft (dft f) (AddChar.doubleDualEmb a) = f (-a)
    source
    theorem dft_cft {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    dft (cft f) = f ∘ ⇑AddChar.doubleDualEquiv.symm ∘ Neg.neg
    source
    theorem cft_dft {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    cft (dft f) = f ∘ ⇑AddChar.doubleDualEquiv.symm ∘ Neg.neg
    source
    theorem cft_injective {G : Type u_1} [AddCommGroup G] [Fintype G] :
    Function.Injective cft
    source
    theorem cft_inv {G : Type u_1} [AddCommGroup G] [Fintype G] {f : G → ℂ} (ψ : AddChar G ℂ) (hf : IsSelfAdjoint f) :
    cft f ψ⁻¹ = (starRingEnd ℂ) (cft f ψ)
    source
    @[simp]
    theorem cft_conj {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (ψ : AddChar G ℂ) :
    cft ((starRingEnd (G → ℂ)) f) ψ = (starRingEnd ℂ) (cft f ψ⁻¹)
    source
    theorem cft_conjneg_apply {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) (ψ : AddChar G ℂ) :
    cft (conjneg f) ψ = (starRingEnd ℂ) (cft f ψ)
    source
    @[simp]
    theorem cft_conjneg {G : Type u_1} [AddCommGroup G] [Fintype G] (f : G → ℂ) :
    cft (conjneg f) = (starRingEnd (AddChar G ℂ → ℂ)) (cft f)
    source
    @[simp]
    theorem cft_balance {G : Type u_1} [AddCommGroup G] [Fintype G] {ψ : AddChar G ℂ} (f : G → ℂ) (hψ : ψ ≠ 0) :
    cft (Fintype.balance f) ψ = cft f ψ
    source
    @[simp]
    theorem cft_trivNChar {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] :
    cft trivNChar = 1
    source
    @[simp]
    theorem cft_one {G : Type u_1} [AddCommGroup G] [Fintype G] :
    cft 1 = trivChar
    source
    @[simp]
    theorem cft_indicator_one_zero {G : Type u_1} [AddCommGroup G] [Fintype G] (s : Finset G) :
    cft ((↑s).indicator fun (x : G) => 1) 0 = ↑s.dens
    source
    theorem cft_conv_apply {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f g : G → ℂ) (ψ : AddChar G ℂ) :
    cft (f ∗ g) ψ = cft f ψ * cft g ψ
    source
    theorem cft_dconv_apply {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f g : G → ℂ) (ψ : AddChar G ℂ) :
    cft (f ○ g) ψ = cft f ψ * (starRingEnd ℂ) (cft g ψ)
    source
    @[simp]
    theorem cft_conv {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f g : G → ℂ) :
    cft (f ∗ g) = cft f * cft g
    source
    @[simp]
    theorem cft_dconv {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f g : G → ℂ) :
    cft (f ○ g) = cft f * (starRingEnd (AddChar G ℂ → ℂ)) (cft g)
    source
    @[simp]
    theorem cft_iterCConv {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℂ) (n : ℕ) :
    cft (f ∗^ₙ n) = cft f ^ n
    source
    @[simp]
    theorem cft_iterCConv_apply {G : Type u_1} [AddCommGroup G] [Fintype G] [DecidableEq G] (f : G → ℂ) (n : ℕ) (ψ : AddChar G ℂ) :
    cft (f ∗^ₙ n) ψ = cft f ψ ^ n