Subdomains of smooth FFT domains

This file develops the subdomain tower for smooth FFT domains and relates it to the corresponding construction for coset FFT domains.

Main definitions

• FftDomainClass.subdomain: The ith FFT subdomain.
• FftDomain.subdomain: Concrete notation for FFT subdomains.

Main results

• mem_fft_subdomain_iff_mem_coset_subdomain: FFT and coset subdomains have the same underlying elements.
• mem_subdomain_of_mem_subdomain_of_le: Membership descends along the subdomain tower.
• subdomain_toFinset_subset_subdomain_toFinset_of_le: Inclusion of image finsets.
• subdomain_toSubgroup_subset_subdomain_toSubgroup_of_le: Inclusion of associated subgroups.
• subdomain_toFftDomain_comm: Taking subdomains commutes with normalization.

def Domain.FftDomainClass.subdomain {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [FftDomainClass D (Fin (2 ^ n)) F] (ω : D) (i : ℕ) : SmoothFftDomain (n - i) F

The ith subdomain of a smooth FFT domain, obtained by taking the corresponding coset subdomain and normalizing it back to an FFT domain.

theorem Domain.FftDomainClass.mem_fft_subdomain_iff_mem_coset_subdomain {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [FftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i : ℕ} : x ∈ subdomain ω i ↔ x ∈ CosetFftDomainClass.subdomain ω i

Membership in an FFT subdomain is the same as membership in the corresponding coset subdomain.

theorem Domain.FftDomainClass.mem_subdomain_of_mem_subdomain_of_le {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [FftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i j : ℕ} (h : x ∈ subdomain ω i) (hji : j ≤ i) : x ∈ subdomain ω j

If x is a member of subdomain ω i it is a member of any subdomain ω j with j ≤ i.

theorem Domain.FftDomainClass.subdomain_toFinset_subset_subdomain_toFinset_of_le {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [FftDomainClass D (Fin (2 ^ n)) F] {ω : D} [DecidableEq F] {i j : ℕ} (hji : j ≤ i) : FftDomain.toFinset (subdomain ω i) ⊆ FftDomain.toFinset (subdomain ω j)

If j ≤ i, then the finset of elements of the ith FFT subdomain is contained in the finset of elements of the jth FFT subdomain.

theorem Domain.FftDomainClass.subdomain_toSubgroup_subset_subdomain_toSubgroup_of_le {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [FftDomainClass D (Fin (2 ^ n)) F] {ω : D} [DecidableEq F] {i j : ℕ} (hji : j ≤ i) : FftDomain.toSubgroup (subdomain ω i) ≤ FftDomain.toSubgroup (subdomain ω j)

If j ≤ i, then the subgroup associated to the ith FFT subdomain is contained in the subgroup associated to the jth FFT subdomain.

theorem Domain.CosetFftDomainClass.subdomain_toFftDomain_comm {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {i : ℕ} : CosetFftDomain.toFftDomain (subdomain ω i) = FftDomainClass.subdomain (toFftDomain ω) i

Normalizing the ith coset subdomain agrees with taking the ith FFT subdomain of the normalized domain.

theorem Domain.CosetFftDomainClass.mem_subdomain_of_mem_subdomain_of_mem_fft_subdomain {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {i j : ℕ} (hji : j ≤ i) {a b : F} (ha : a ∈ subdomain ω j) (hb : b ∈ FftDomainClass.subdomain (toFftDomain ω) i) : a * b ∈ subdomain ω j

Multiplying an element of a coset subdomain by an element of a deeper FFT subdomain of the normalized domain stays in the original coset subdomain.

theorem Domain.CosetFftDomainClass.mem_subdomain_of_mem_fft_subdomain_of_mem_subdomain {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {i j : ℕ} (hji : j ≤ i) {a b : F} (ha : a ∈ FftDomainClass.subdomain (toFftDomain ω) i) (hb : b ∈ subdomain ω j) : a * b ∈ subdomain ω j

Multiplying an element of a deeper FFT subdomain of the normalized domain by an element of a coset subdomain stays in the coset subdomain.

@[reducible, inline]

abbrev Domain.FftDomain.subdomain {F : Type} [Field F] {n : ℕ} (ω : SmoothFftDomain n F) (i : ℕ) : SmoothFftDomain (n - i) F

Concrete notation for the ith subdomain of a smooth FFT domain.