Coset FFT domains

This file defines coset FFT domains and their abstract interface.

A coset FFT domain is a multiplicative coset of a finite subgroup of a field, indexed additively. The typeclass CosetFftDomainClass provides an abstract axiomatization of such domains, while CosetFftDomain gives a concrete representation.

Main definitions

• CosetFftDomain: A concrete coset FFT domain.
• CosetFftDomainClass: Typeclass for objects behaving like coset FFT domains.
• CosetFftDomainClass.mkSubgroupUnit: Recovers the underlying subgroup element.
• CosetFftDomainClass.toCosetFftDomain: Constructs a concrete domain from a class instance.
• SmoothCosetFftDomain: Coset FFT domains indexed by Fin (2 ^ n).

Main results

• CosetFftDomainClass.ne_zero: Elements of a coset FFT domain are nonzero.
• CosetFftDomainClass.toCosetFftDomain_of_CosetFftDomain: Reconstruction is the identity on concrete domains.
• CosetFftDomain.map_0_eq_coset_generator: The value at zero is the coset generator.
• CosetFftDomain.injective: Coset FFT domains are injective.

structure Domain.CosetFftDomain (ι : Type) [AddCommGroup ι] (F : Type) [Field F] : Type

A coset FFT domain is a domain of the form x · G for an FFT domain G.

• subgroupDomain : Multiplicative ι →* Fˣ
• subgroupDomain_inj : Function.Injective ⇑self.subgroupDomain
• cosetGenerator : Fˣ

class Domain.CosetFftDomainClass (D : Type u) (ι : outParam (Type v)) [AddCommGroup ι] (F : outParam (Type v)) [Field F] [FunLike D ι F] : Prop

Typeclass for objects behaving like coset FFT domains as functions ι → F. The axioms say that the image is a shifted multiplicative subgroup: ω 0 is the coset representative, multiplication in the subgroup corresponds to addition in ι, negation gives inverses up to the coset factor, and the map is injective.

• map_zero_unit (ω : D) : IsUnit (ω 0)
• map_add (ω : D) (i j : ι) : ω (i + j) = (ω 0)⁻¹ * ω i * ω j
• map_neg (ω : D) (i : ι) : ω (-i) = ω 0 ^ 2 * (ω i)⁻¹
• injective (ω : D) : Function.Injective ⇑ω

@[simp]

theorem Domain.CosetFftDomainClass.ne_zero {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) (i : ι) : ω i ≠ 0

Every point of a coset FFT domain is nonzero.

@[implicit_reducible]

instance Domain.instFunLikeCosetFftDomain {ι : Type} [AddCommGroup ι] {F : Type} [Field F] : FunLike (CosetFftDomain ι F) ι F

theorem Domain.CosetFftDomain.eval_coset_fft_domain_eq_eval_generator_mul_domain {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {cosetDomain : CosetFftDomain ι F} {i : ι} : cosetDomain i = ↑cosetDomain.cosetGenerator * ↑(cosetDomain.subgroupDomain i)

Evaluation of a concrete coset FFT domain is multiplication of the coset generator by the subgroup element indexed by i.

instance Domain.instCosetFftDomainClassCosetFftDomain {ι : Type} [AddCommGroup ι] {F : Type} [Field F] : CosetFftDomainClass (CosetFftDomain ι F) ι F

CosetFftDomain is indeed an instance of CosetFftDomainClass.

def Domain.CosetFftDomainClass.mkSubgroupUnit {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) (i : ι) : Fˣ

The normalized value (ω 0)⁻¹ * ω i, packaged as a unit of F.

This removes the coset shift and recovers the underlying subgroup element.

def Domain.CosetFftDomainClass.toCosetFftDomain {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) : CosetFftDomain ι F

Reconstruct a concrete CosetFftDomain from any object of a type satisfying CosetFftDomainClass.

theorem Domain.CosetFftDomainClass.toCosetFftDomain_of_CosetFftDomain {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {ω : CosetFftDomain ι F} : toCosetFftDomain ω = ω

Reconstructing a concrete coset FFT domain from its class instance gives back the original domain.

theorem Domain.CosetFftDomainClass.toCosetFftDomain_apply_self {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {ω : CosetFftDomain ι F} {i : ι} : (toCosetFftDomain ω) i = ω i

Reconstructing a concrete coset FFT domain preserves evaluation.

@[implicit_reducible]

instance Domain.instCoeOutEmbeddingOfCosetFftDomainClass {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] : CoeOut D (ι ↪ F)

Any class-level coset FFT domain coerces to an embedding into F.

theorem Domain.CosetFftDomainClass.ext {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω₁ ω₂ : D} (h : ∀ (i : ι), ω₁ i = ω₂ i) : ω₁ = ω₂

Extensionality for class-level coset FFT domains. Domains are equal if their evaluations are equal.

theorem Domain.CosetFftDomainClass.ext_iff {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω₁ ω₂ : D} : ω₁ = ω₂ ↔ ∀ (i : ι), ω₁ i = ω₂ i

theorem Domain.CosetFftDomain.map_0_eq_coset_generator {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {ω : CosetFftDomain ι F} : ω 0 = ↑ω.cosetGenerator

The value at zero is the coset generator.

@[simp]

theorem Domain.CosetFftDomain.injective {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {ω : CosetFftDomain ι F} : Function.Injective ⇑ω

A concrete coset FFT domain is injective as a function.

@[simp]

theorem Domain.CosetFftDomain.injOn {ι : Type} [AddCommGroup ι] {F : Type} [Field F] {ω : CosetFftDomain ι F} {s : Set ι} : Set.InjOn (⇑ω) s

A concrete coset FFT domain is injective on every set.

@[reducible, inline]

abbrev Domain.SmoothCosetFftDomain (n : ℕ) (F : Type) [Field F] : Type

A smooth coset FFT domain is a coset domain indexed by Fin (2 ^ n).

def Domain.CosetFftDomainClass.toFinset {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) : Finset F

The elements of a domain as a finset.

@[simp]

theorem Domain.CosetFftDomainClass.card_toFinset {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} : (toFinset ω).card = Fintype.card ι

The cardinality of the finset of elements of a domain is the cardinality of the indexing type.

@[reducible, inline]

abbrev Domain.CosetFftDomain.toFinset {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] (ω : CosetFftDomain ι F) : Finset F

The finset of elements of a concrete coset FFT domain.