@[reducible, inline]

abbrev BlrPcp.Vec (F : Type u_3) (Idx : Type u_4) : Type (max u_3 u_4)

Equations

• BlrPcp.Vec F Idx = (Idx → F)

@[reducible, inline]

abbrev BlrPcp.ScalarFn (F : Type u_3) (Idx : Type u_4) : Type (max u_3 u_4)

Equations

• BlrPcp.ScalarFn F Idx = (BlrPcp.Vec F Idx → F)

@[reducible, inline]

abbrev BlrPcp.ComplexFn (F : Type u_3) (Idx : Type u_4) : Type (max u_4 u_3)

Equations

• BlrPcp.ComplexFn F Idx = (BlrPcp.Vec F Idx → ℂ)

def BlrPcp.linearFn {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] (a : Vec F Idx) : ScalarFn F Idx

The linear scalar function ℓ_a(x) = ∑ i, a i * x i.

Equations

• BlrPcp.linearFn a x = ∑ i : Idx, a i * x i

def BlrPcp.IsLinear {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] (f : ScalarFn F Idx) : Prop

Equations

• BlrPcp.IsLinear f = ∃ (a : BlrPcp.Vec F Idx), ∀ (x : BlrPcp.Vec F Idx), f x = BlrPcp.linearFn a x

def BlrPcp.LinearSet {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] : Set (ScalarFn F Idx)

Equations

• BlrPcp.LinearSet = {f : BlrPcp.ScalarFn F Idx | BlrPcp.IsLinear f}

noncomputable def BlrPcp.linearSetIndicator {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] (f : ScalarFn F Idx) : ℝ

The real-valued indicator of membership in the set of linear scalar functions.

Equations

• BlrPcp.linearSetIndicator f = if f ∈ BlrPcp.LinearSet then 1 else 0

def BlrPcp.BLRAcceptsAt {F : Type u_1} {Idx : Type u_2} [Field F] (f : ScalarFn F Idx) (a b : F) (x y : Vec F Idx) : Prop

Equations

• BlrPcp.BLRAcceptsAt f a b x y = (a * f x + b * f y = f fun (i : Idx) => a * x i + b * y i)

def BlrPcp.nonzeroScalars {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] : Finset F

The nonzero field elements used as BLR scalar samples.

Equations

• BlrPcp.nonzeroScalars = {a : F | a ≠ 0}

noncomputable def BlrPcp.acceptanceProbabilityBLR {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] (f : ScalarFn F Idx) : ℝ

The uniform acceptance probability of the finite-field BLR test: a,b are sampled uniformly from F \ {0} and x,y from F^Idx.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BlrPcp.rejectionProbabilityBLR {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] (f : ScalarFn F Idx) : ℝ

Equations

• BlrPcp.rejectionProbabilityBLR f = 1 - BlrPcp.acceptanceProbabilityBLR f

noncomputable def BlrPcp.distance {F : Type u_1} {Idx : Type u_2} [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] (f g : ScalarFn F Idx) : ℝ

The relative Hamming distance between two scalar functions, i.e. the uniform probability that they disagree on a point of F^Idx.

Equations

• BlrPcp.distance f g = (↑(Fintype.card (BlrPcp.Vec F Idx)))⁻¹ * ∑ x : BlrPcp.Vec F Idx, if f x ≠ g x then 1 else 0

noncomputable def BlrPcp.distanceToLinear {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : ℝ

The distance from a scalar function to linearity, namely the minimum of distance f g over all g ∈ LinearSet.

Equations

• BlrPcp.distanceToLinear f = BlrPcp.linearFunctionsFinset✝.inf' ⋯ fun (g : BlrPcp.ScalarFn F Idx) => BlrPcp.distance f g

theorem BlrPcp.BLRAcceptsAt_linearFn {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] [Nonempty Idx] (α : Vec F Idx) (a b : F) (x y : Vec F Idx) : BLRAcceptsAt (linearFn α) a b x y

A linear function passes the BLR check for every choice of randomness.

theorem BlrPcp.BLRAcceptsAt_of_mem_linearSet {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] [Nonempty Idx] {f : ScalarFn F Idx} (hf : f ∈ LinearSet) (a b : F) (x y : Vec F Idx) : BLRAcceptsAt f a b x y

Every member of LinearSet passes the BLR check pointwise.

theorem BlrPcp.blr_completeness {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] {f : ScalarFn F Idx} (hf : f ∈ LinearSet) : acceptanceProbabilityBLR f = 1

Completeness of the finite-field BLR verifier: linear functions are accepted with probability one.

def BlrPcp.dotProduct {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype Idx] (a x : Vec F Idx) : F

The standard bilinear pairing on F^Idx.

Equations

• BlrPcp.dotProduct a x = ∑ i : Idx, a i * x i

def BlrPcp.«term⟪_,_⟫ᵥ» : Lean.ParserDescr

Notation for the standard bilinear pairing on F^Idx.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BlrPcp.expectation {F : Type u_1} {Idx : Type u_2} [Fintype F] [Fintype Idx] [DecidableEq Idx] (f : ComplexFn F Idx) : ℂ

The uniform expectation of a complex-valued function on F^Idx.

Equations

• BlrPcp.expectation f = ↑(↑(Fintype.card (BlrPcp.Vec F Idx)))⁻¹ * ∑ x : BlrPcp.Vec F Idx, f x

noncomputable def BlrPcp.fnInner {F : Type u_1} {Idx : Type u_2} [Fintype F] [Fintype Idx] [DecidableEq Idx] (f g : ComplexFn F Idx) : ℂ

The expectation-based Hermitian inner product on complex-valued functions on F^Idx.

Equations

• BlrPcp.fnInner f g = BlrPcp.expectation fun (x : BlrPcp.Vec F Idx) => f x * star (g x)

noncomputable def BlrPcp.fnNormSq {F : Type u_1} {Idx : Type u_2} [Fintype F] [Fintype Idx] [DecidableEq Idx] (f : ComplexFn F Idx) : ℝ

The squared L² norm associated to fnInner.

Equations

• BlrPcp.fnNormSq f = (↑(Fintype.card (BlrPcp.Vec F Idx)))⁻¹ * ∑ x : BlrPcp.Vec F Idx, ‖f x‖ ^ 2

noncomputable def BlrPcp.fnNorm {F : Type u_1} {Idx : Type u_2} [Fintype F] [Fintype Idx] [DecidableEq Idx] (f : ComplexFn F Idx) : ℝ

The L² norm associated to the expectation inner product.

Equations

• BlrPcp.fnNorm f = √(BlrPcp.fnNormSq f)

def BlrPcp.«term⟪_,_⟫» : Lean.ParserDescr

Notation for the expectation-based Hermitian inner product on F^Idx → ℂ.

Equations

• One or more equations did not get rendered due to their size.

def BlrPcp.«term‖_‖₂» : Lean.ParserDescr

Notation for the expectation-based L² norm on F^Idx → ℂ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BlrPcp.charFn {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [Fintype Idx] (α : Vec F Idx) : ComplexFn F Idx

The additive character indexed by α : F^Idx, defined by χ_α(x) = ω_p^{Tr(∑ i, α i * x i)} where p = ringChar F.

Equations

• BlrPcp.charFn α x = ZMod.stdAddChar ((Algebra.trace (ZMod (ringChar F)) F) (BlrPcp.dotProduct α x))

noncomputable def BlrPcp.phaseLift {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] (f : ScalarFn F Idx) (c : F) : ComplexFn F Idx

The c-phase of f : F^Idx → F, defined by f_c(x) = ω_p^{Tr(c * f(x))} where p = ringChar F.

Equations

• BlrPcp.phaseLift f c x = ZMod.stdAddChar ((Algebra.trace (ZMod (ringChar F)) F) (c * f x))

noncomputable def BlrPcp.fourierCoeff {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [Fintype Idx] [DecidableEq Idx] (f : ComplexFn F Idx) (α : Vec F Idx) : ℂ

The Fourier coefficient \hat f(\alpha) is the expectation inner product of f with the character χ_α.

Equations

• BlrPcp.fourierCoeff f α = BlrPcp.fnInner f (BlrPcp.charFn α)

def BlrPcp.«term_̂» : Lean.TrailingParserDescr

Postfix notation for the Fourier transform f ↦ \hat f.

Equations

• BlrPcp.«term_̂» = Lean.ParserDescr.trailingNode `BlrPcp.«term_̂» 1024 1024 (Lean.ParserDescr.symbol "̂")

def BlrPcp.«term_̂(_)» : Lean.TrailingParserDescr

Application notation for Fourier coefficients, allowing f̂(α).

Equations

• One or more equations did not get rendered due to their size.

theorem BlrPcp.character_sum_indicator_eq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (u v : F) : (if u = v then 1 else 0) = (↑(Fintype.card F))⁻¹ * ∑ c : F, BlrPcp.baseChar✝ (c * (u - v))

Character-sum indicator for equality in F: baseChar is the Lean encoding of ω_p^{Tr(·)}.

theorem BlrPcp.characters_orthogonal_basis {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] : (∀ (α β : Vec F Idx), fnInner (charFn α) (charFn β) = if α = β then 1 else 0) ∧ Submodule.span ℂ (Set.range charFn) = ⊤

theorem BlrPcp.phaseLift_linearFn {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (α : Vec F Idx) (c : F) : phaseLift (linearFn α) c = charFn fun (i : Idx) => c * α i

The c-phase of the linear function ℓ_α is the character χ_{cα}.

theorem BlrPcp.fourierCoeff_phaseLift_linearFn {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (α β : Vec F Idx) (c : F) : fourierCoeff (phaseLift (linearFn α) c) β = if β = fun (i : Idx) => c * α i then 1 else 0

Fourier expansion of a linear function: the c-phase of ℓ_α has a single Fourier coefficient, at cα.

theorem BlrPcp.parseval_identity {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (g : ComplexFn F Idx) : ∑ α : Vec F Idx, ‖fourierCoeff g α‖ ^ 2 = fnNormSq g

theorem BlrPcp.fourier_plancherel {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f g : ComplexFn F Idx) : ∑ α : Vec F Idx, fourierCoeff f α * star (fourierCoeff g α) = fnInner f g

theorem BlrPcp.fourier_inversion {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (g : ComplexFn F Idx) (x : Vec F Idx) : g x = ∑ α : Vec F Idx, fourierCoeff g α * charFn α x

Pointwise Fourier inversion for the character basis χ_α.

theorem BlrPcp.distance_formula_via_phase_fourier_coefficients {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f g : ScalarFn F Idx) : ↑(distance f g) = 1 - (↑(Fintype.card F))⁻¹ * (1 + ∑ c ∈ nonzeroScalars, ∑ α : Vec F Idx, fourierCoeff (phaseLift f c) α * star (fourierCoeff (phaseLift g c) α))

Relative Hamming distance in terms of the Fourier coefficients of the nonzero phase lifts of f and g.

noncomputable def BlrPcp.linearFourierScore {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : ℂ

The Fourier score of f against the linear function ℓ_α.

Equations

• BlrPcp.linearFourierScore f α = ∑ c ∈ BlrPcp.nonzeroScalars, BlrPcp.fourierCoeff (BlrPcp.phaseLift f c) fun (i : Idx) => c * α i

theorem BlrPcp.linearFourierScore_norm_sq_sum_le {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : ∑ α : Vec F Idx, ‖linearFourierScore f α‖ ^ 2 ≤ ↑nonzeroScalars.card ^ 2

The squared linear Fourier scores have total mass at most (q - 1)^2.

theorem BlrPcp.exact_blr_acceptance_formula {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : ↑(acceptanceProbabilityBLR f) = (↑(Fintype.card F))⁻¹ * (1 + (↑nonzeroScalars.card)⁻¹ ^ 2 * ∑ α : Vec F Idx, linearFourierScore f α ^ 3)

Exact BLR acceptance formula in terms of the Fourier scores ∑ c∈Fˣ, \widehat{f_c}(cα).

noncomputable def BlrPcp.linearFourierScoreReal {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : ℝ

The real part of the Fourier score of f against ℓ_α. The score is proved real in linearFourierScore_im_eq_zero.

Equations

• BlrPcp.linearFourierScoreReal f α = (BlrPcp.linearFourierScore f α).re

theorem BlrPcp.distance_linearFn_fourier {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : ↑(distance f (linearFn α)) = 1 - (↑(Fintype.card F))⁻¹ * (1 + linearFourierScore f α)

Relative Hamming distance from f to the linear function ℓ_α, written in terms of the Fourier coefficients of the nonzero phase lifts of f.

theorem BlrPcp.distance_linearFn_fourier_real {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : distance f (linearFn α) = 1 - (↑(Fintype.card F))⁻¹ * (1 + linearFourierScoreReal f α)

The fixed-linear-function Fourier distance formula, with real-valued score.

theorem BlrPcp.linearFourierScore_im_eq_zero {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : (linearFourierScore f α).im = 0

theorem BlrPcp.exact_blr_acceptance_formula_real {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : acceptanceProbabilityBLR f = (↑(Fintype.card F))⁻¹ * (1 + (↑nonzeroScalars.card)⁻¹ ^ 2 * ∑ α : Vec F Idx, linearFourierScoreReal f α ^ 3)

Real-valued form of the exact BLR acceptance formula.

theorem BlrPcp.linearFourierScoreReal_sq_sum_le {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : ∑ α : Vec F Idx, linearFourierScoreReal f α ^ 2 ≤ ↑nonzeroScalars.card ^ 2

Real form of linearFourierScore_norm_sq_sum_le.

theorem BlrPcp.linearFourierScoreReal_bounds {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) (α : Vec F Idx) : -1 ≤ linearFourierScoreReal f α ∧ linearFourierScoreReal f α ≤ ↑(Fintype.card F) - 1

theorem BlrPcp.distanceToLinear_fourier {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : distanceToLinear f = 1 - (↑(Fintype.card F))⁻¹ * (1 + Finset.univ.sup' ⋯ (linearFourierScoreReal f))

Distance to linearity in Fourier form.

theorem BlrPcp.distance_to_linearity_fourier {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : distanceToLinear f = 1 - (↑(Fintype.card F))⁻¹ * (1 + Finset.univ.sup' ⋯ (linearFourierScoreReal f)) ∧ ∀ (α : Vec F Idx), (linearFourierScore f α).im = 0 ∧ -1 ≤ linearFourierScoreReal f α ∧ linearFourierScoreReal f α ≤ ↑(Fintype.card F) - 1

Distance to linearity in Fourier form, together with the realness and range of each linear Fourier score.

theorem BlrPcp.finite_field_blr_soundness {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : acceptanceProbabilityBLR f ≤ 1 - distanceToLinear f

Soundness of the finite-field BLR test in the Fourier-score form used by the proof: acceptance is at most 1 - distanceToLinear f.

theorem BlrPcp.blr {F : Type u_1} {Idx : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype Idx] [DecidableEq Idx] [Nonempty Idx] (f : ScalarFn F Idx) : linearSetIndicator f ≤ acceptanceProbabilityBLR f ∧ acceptanceProbabilityBLR f ≤ 1 - distanceToLinear f

The finite-field BLR acceptance probability is sandwiched between completeness for linear functions and the soundness bound from distance to linearity.