ArkLib.Data.Domain.CosetFftDomain.Block

This module provides a definition of a block of a coset FFT domain (definition 4.16 from [ACFY24b]).

Main definitions #

block: A block of a coset FFT domain at a point x.
blockIdx: The indices of the elements of a block of a coset FFT domain at a point x.

Main results #

card_block_le: The cardinality bound of a block.
card_blockIdx: The cardinality of block and blockIdx coincide.

References #

Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., WHIR: Reed–Solomon Proximity Testing with Super-Fast Verification

def Domain.CosetFftDomainClass.block {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] (ω : D) (k : ℕ) (x : F) :

Finset F

The kth roots of x from the domain ω.

This is the definition 4.16 from [ACFY24b]. Note, we do not require x to be from a subdomain.

Instances For

source

@[simp]

theorem Domain.CosetFftDomainClass.mem_block {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x y : F} :

y ∈ block ω k x ↔ y ∈ ω ∧ y ^ 2 ^ k = x

An equivalent definition of the membership to a block.

source

@[simp]

theorem Domain.CosetFftDomainClass.block_x_0 {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} :

block ω k 0 = ∅

There are no roots of 0 in any domain.

source

@[simp]

theorem Domain.CosetFftDomainClass.block_k_1 {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {x : F} :

block ω 0 x = if x ∈ ω then {x} else ∅

source

theorem Domain.CosetFftDomainClass.block_eq_nthRootsFinset {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x : F} :

block ω k x = Polynomial.nthRootsFinset (2 ^ k) x ∩ toFinset ω

An alternative definition of block in terms of Polynomial.nthRootsFinset.

source

@[simp]

theorem Domain.CosetFftDomainClass.card_block_le {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x : F} :

(block ω k x).card ≤ 2 ^ k

The cardinality of a block does not exceed its degree.

source

def Domain.CosetFftDomainClass.blockIdx {ι : Type} [Fintype ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] (ω : D) (k : ℕ) (x : F) :

Finset ι

The set of indices of a block of ω at x of the degree k.

Instances For

source

theorem Domain.CosetFftDomainClass.mem_blockIdx {ι : Type} [Fintype ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] {ω : D} {k : ℕ} {x : F} {i : ι} :

i ∈ blockIdx ω k x ↔ ω i ^ 2 ^ k = x

The definition of membership to a blockIdx.

source

@[simp]

theorem Domain.CosetFftDomainClass.mem_blockIdx_self {ι : Type} [Fintype ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] {ω : D} {k : ℕ} {i : ι} :

i ∈ blockIdx ω k (ω i ^ 2 ^ k)

source

theorem Domain.CosetFftDomainClass.mem_blockIdx_iff_mem_block {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x : F} {i : ι} :

i ∈ blockIdx ω k x ↔ ω i ∈ block ω k x

source

@[simp]

theorem Domain.CosetFftDomainClass.blockIdx_x_0 {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} :

blockIdx ω k 0 = ∅

There are no roots of 0 in any domain.

source

theorem Domain.CosetFftDomainClass.blockIdx_k_1_of_eq {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {x : F} {i : ι} (hi : ω i = x) :

blockIdx ω 0 x = {i}

source

theorem Domain.CosetFftDomainClass.blockIdx_k_1_of_ne_mem {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {x : F} (hx : x ∉ ω) :

blockIdx ω 0 x = ∅

source

theorem Domain.CosetFftDomainClass.blockIdx_eq_preimage_block {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x : F} :

blockIdx ω k x = (block ω k x).preimage ⇑ω ⋯

blockIdx is the preimage of block.

source

@[simp]

theorem Domain.CosetFftDomainClass.card_blockIdx {ι : Type} [Fintype ι] [AddCommGroup ι] {F : Type} [Field F] [DecidableEq F] {D : Type} [FunLike D ι F] [CosetFftDomainClass D ι F] {ω : D} {k : ℕ} {x : F} :

(blockIdx ω k x).card = (block ω k x).card

The cardinality of blockIdx is that of block.