Subdomains of smooth coset FFT domains

This file develops the hierarchy of subdomains of a smooth coset FFT domain.

It also studies roots, cardinalities of fibers of powering maps, and provides a root-finding procedure.

Main definitions

• CosetFftDomainClass.subdomain_embed: Embedding of subdomain indices into the ambient domain.
• CosetFftDomainClass.subdomain: The ith subdomain.
• CosetFftDomain.twoNthRoot: A constructive 2 ^ ith-root operation.

Main results

• pow_mem_of_mem: Powers move elements down the subdomain tower.
• card_roots: Exact cardinality of fibers of powering maps.
• root_exists: Existence of roots in higher subdomains.
• square_roots_explicit: Explicit description of square roots.
• twoNthRoot_correct: Correctness of the root-finding algorithm.

def Domain.CosetFftDomainClass.subdomain_embed {n : ℕ} (i : ℕ) (k : Fin (2 ^ (n - i))) : Fin (2 ^ n)

Embed the index type of the ith subdomain into the index type of the ambient smooth coset FFT domain. When i < n, this sends k to 2 ^ i * k; when i ≥ n, the subdomain is trivial and everything maps to 0.

theorem Domain.CosetFftDomainClass.subdomain_embed_add {n : ℕ} (i : ℕ) (a b : Fin (2 ^ (n - i))) : CosetFftDomainClass.subdomain_embed i (a + b) = CosetFftDomainClass.subdomain_embed i a + CosetFftDomainClass.subdomain_embed i b

The subdomain embedding preserves addition.

theorem Domain.CosetFftDomainClass.subdomain_embed_zero {n : ℕ} (i : ℕ) : CosetFftDomainClass.subdomain_embed i 0 = 0

The subdomain embedding sends 0 to 0.

theorem Domain.CosetFftDomainClass.subdomain_embed_injective {n : ℕ} (i : ℕ) : Function.Injective (CosetFftDomainClass.subdomain_embed i)

The subdomain embedding is injective.

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

Given a smooth coset FFT domain ω of log-order n, return its subdomain of log-order n - i.

The resulting coset generator is ω 0 ^ 2 ^ i.

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

Membership in subdomains is invariant under equal subdomain indices.

@[simp]

theorem Domain.CosetFftDomainClass.subdomain_generator_pow_generator {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} (i : ℕ) : ↑(subdomain ω i).cosetGenerator = ω 0 ^ 2 ^ i

The coset generator of the ith subdomain is ω 0 ^ 2 ^ i.

@[simp]

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

Membership to the 0th subdomain is the same as membership to the original coset FFT domain.

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

The nth subdomain consists exactly of the single element ω 0 ^ 2 ^ n.

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

If x lies in the jth subdomain, then x ^ 2 ^ i lies in the (j + i)th subdomain, provided j + i ≤ n.

theorem Domain.CosetFftDomainClass.pow_mem_subdomain_of_mem_subdomain_0 {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i : ℕ} (hi : i ≤ n) (h : x ∈ subdomain ω 0) : x ^ 2 ^ i ∈ subdomain ω i

If x lies in the original domain, then x ^ 2 ^ i lies in the ith subdomain.

theorem Domain.CosetFftDomainClass.pow_mem_subdomain_of_mem_subdomain_0_toFinset {F : Type} [Field F] [DecidableEq F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i : ℕ} (hi : i ≤ n) (h : x ∈ CosetFftDomain.toFinset (subdomain ω 0)) : x ^ 2 ^ i ∈ CosetFftDomain.toFinset (subdomain ω i)

toFinset-version of pow_mem_subdomain_of_mem_subdomain_0.

theorem Domain.CosetFftDomainClass.mem_subdomain_of_le_of_mem_subdomain {F : Type} [Field F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i j : ℕ} (h : j ≤ i) (hx : x ∈ subdomain ω i) : ω 0 ^ 2 ^ j * (ω 0)⁻¹ ^ 2 ^ i * x ∈ subdomain ω j

If j ≤ i, then we do not have x ∈ subdomain ω i → x ∈ subdomain ω j in the general case but rescaling x as ω 0 ^ 2 ^ j * (ω 0)⁻¹ ^ 2 ^ i * x gives us a member of subdomain ω j.

theorem Domain.CosetFftDomainClass.card_roots {F : Type} [Field F] [DecidableEq F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i j : ℕ} (hij : i + j ≤ n) (h : x ∈ subdomain ω (i + j)) : {y ∈ CosetFftDomain.toFinset (subdomain ω i) | y ^ 2 ^ j = x}.card = 2 ^ j

If x lies in the (i + j)th subdomain, then it has exactly 2 ^ j preimages under y ↦ y ^ 2 ^ j from the ith subdomain.

theorem Domain.CosetFftDomainClass.root_exists {F : Type} [Field F] [DecidableEq F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i j : ℕ} (hij : i + j ≤ n) (h : x ∈ subdomain ω (i + j)) : ∃ y ∈ subdomain ω i, y ^ 2 ^ j = x

Every element of the (i + j)th subdomain has a 2 ^ jth root in the ith subdomain.

theorem Domain.CosetFftDomainClass.sq_root_mem_subdomain {F : Type} [Field F] [DecidableEq F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i : ℕ} (hi : i < n) {y : F} (hx : x ∈ subdomain ω (i + 1)) (hy : y ^ 2 = x) : y ∈ subdomain ω i

Any square root of an element of the (i + 1)th subdomain lies in the ith subdomain.

theorem Domain.CosetFftDomainClass.square_roots_explicit {F : Type} [Field F] [DecidableEq F] {n : ℕ} {D : Type} [FunLike D (Fin (2 ^ n)) F] [CosetFftDomainClass D (Fin (2 ^ n)) F] {ω : D} {x : F} {i : ℕ} (hi : i < n) {y : F} (hx : x ∈ subdomain ω (i + 1)) (hy : y ^ 2 = x) : {y ∈ CosetFftDomain.toFinset (subdomain ω i) | y ^ 2 = x} = {y, -y}

The square roots of x inside the ith subdomain are exactly y and -y, for any square root y of x.

@[reducible, inline]

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

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

def Domain.CosetFftDomain.twoNthRootAux {F : Type} [Field F] [DecidableEq F] (n i : ℕ) (ω : SmoothCosetFftDomain n F) (x : F) (fuel : ℕ) : ↥(CosetFftDomainClass.toFinset ω)

Search through a smooth coset FFT domain for an element whose 2 ^ ith power is x, using fuel as the remaining search bound.

def Domain.CosetFftDomain.twoNthRoot {F : Type} [Field F] [DecidableEq F] {n i : ℕ} {ω : SmoothCosetFftDomain n F} (x : ↥(CosetFftDomainClass.toFinset (subdomain ω i))) : ↥(CosetFftDomainClass.toFinset ω)

Finds a 2 ^ nth root of x.

theorem Domain.CosetFftDomain.twoNthRoot_correct {F : Type} [Field F] [DecidableEq F] {n i : ℕ} {ω : SmoothCosetFftDomain n F} (hi : i ≤ n) {x : ↥(CosetFftDomainClass.toFinset (subdomain ω i))} : ↑(twoNthRoot x) ^ 2 ^ i = ↑x

The value returned by twoNthRoot is a 2 ^ ith root of its input.

@[simp]

theorem Domain.CosetFftDomain.twoNthRoot_correct_one {F : Type} [Field F] [DecidableEq F] {n : ℕ} {ω : SmoothCosetFftDomain n F} [nz : NeZero n] {x : ↥(CosetFftDomainClass.toFinset (subdomain ω 1))} : ↑(twoNthRoot x) ^ 2 = ↑x

Specialized correctness statement for square roots from the first subdomain.