Linear equations

This file defines the LINEQ language, its executable LPCP verifier, and the linear PCP theorem for LINEQ.

@[reducible, inline]

abbrev LINEQ (F : Type) (m n : ℕ) [Field F] : Set (Matrix (Fin m) (Fin n) F × (Fin m → F))

Equations

• LINEQ F m n = {(M, c) : Matrix (Fin m) (Fin n) F × (Fin m → F) | ∃ (b : Fin n → F), M.mulVec b = c}

def LINEQ.size {F : Type} [Fintype F] {m n : ℕ} : Matrix (Fin m) (Fin n) F × (Fin m → F) → ℕ

Equations

• LINEQ.size x✝ = (m * n + m) * Nat.clog 2 (Fintype.card F)

theorem LINEQ.dotProduct_transpose_mulVec_eq {F : Type} [Field F] {m n : ℕ} (M : Matrix (Fin m) (Fin n) F) (b : Fin n → F) (c r : Fin m → F) (h : M.mulVec b = c) : b ⬝ᵥ M.transpose.mulVec r = c ⬝ᵥ r

theorem LINEQ.dotProduct_eq_add_sum_erase {F : Type} [Field F] {m : ℕ} (a b : Fin m → F) (k : Fin m) : a ⬝ᵥ b = a k * b k + ∑ i ∈ Finset.univ.erase k, a i * b i

noncomputable def LINEQ.normalizeLinearForm {F : Type} [Field F] {m : ℕ} (a : Fin m → F) (k : Fin m) : (Fin m → F) → Fin m → F

Equations

• LINEQ.normalizeLinearForm a k r i = if i = k then a ⬝ᵥ r / a k else r i

noncomputable def LINEQ.normalizeLinearFormInv {F : Type} [Field F] {m : ℕ} (a : Fin m → F) (k : Fin m) : (Fin m → F) → Fin m → F

Equations

• LINEQ.normalizeLinearFormInv a k r i = if i = k then r k - (∑ j ∈ Finset.univ.erase k, a j * r j) / a k else r i

theorem LINEQ.normalizeLinearForm_left_inv {F : Type} [Field F] {m : ℕ} {a : Fin m → F} {k : Fin m} (hk : a k ≠ 0) : Function.LeftInverse (normalizeLinearFormInv a k) (normalizeLinearForm a k)

theorem LINEQ.normalizeLinearForm_right_inv {F : Type} [Field F] {m : ℕ} {a : Fin m → F} {k : Fin m} (hk : a k ≠ 0) : Function.RightInverse (normalizeLinearFormInv a k) (normalizeLinearForm a k)

theorem LINEQ.normalizeLinearForm_bijective {F : Type} [Field F] {m : ℕ} {a : Fin m → F} {k : Fin m} (hk : a k ≠ 0) : Function.Bijective (normalizeLinearForm a k)

theorem LINEQ.coordinate_zero_card_div_le {F : Type} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} (k : Fin m) : ↑{r : Fin m → F | r k = 0}.card / ↑(Fintype.card F) ^ m ≤ 1 / ↑(Fintype.card F)

theorem LINEQ.uniform_coordinate_zero_prob_mul_card_le_one {F : Type} [Field F] [Fintype F] [DecidableEq F] [Inhabited F] [SampleableType F] {m : ℕ} (k : Fin m) : Pr[fun (r : Fin m → F) => r k = 0 | $ᵗ(Fin m → F)] * ↑(Fintype.card F) ≤ 1

theorem LINEQ.linear_form_uniform_prob_mul_card_le_one {F : Type} [Field F] [Fintype F] [DecidableEq F] [Inhabited F] [SampleableType F] {m : ℕ} {a : Fin m → F} (ha : a ≠ 0) : Pr[fun (r : Fin m → F) => a ⬝ᵥ r = 0 | $ᵗ(Fin m → F)] * ↑(Fintype.card F) ≤ 1

theorem LINEQ.card_sub_one_add_one (α : Type) [Fintype α] [Nonempty α] : Fintype.card α - 1 + 1 = Fintype.card α

def LINEQ.decodeUniformFin (α : Type) [Fintype α] [Encodable α] [Nonempty α] : Fin (Fintype.card α - 1 + 1) → α

Equations

• LINEQ.decodeUniformFin α i = Encodable.fintypeEquivFin.symm (Fin.cast ⋯ i)

theorem LINEQ.decodeUniformFin_bijective (α : Type) [Fintype α] [Encodable α] [Nonempty α] : Function.Bijective (decodeUniformFin α)

theorem LINEQ.probEvent_decodeUniformFin (α : Type) [Fintype α] [Encodable α] [Nonempty α] [SampleableType α] (p : α → Prop) : Pr[p ∘ decodeUniformFin α | $ᵗFin (Fintype.card α - 1 + 1)] = Pr[p | $ᵗα]

def LINEQ.sampleRandomVector (m n : ℕ) (F : Type) [Field F] [Fintype F] [Encodable F] [DecidableEq F] [Inhabited F] : OracleComp (LPCPOracleSpec F n) (Fin m → F)

Equations

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

def LINEQ.verifier {F : Type} [Field F] [Fintype F] [DecidableEq F] [Inhabited F] {m n : ℕ} [Encodable F] : LPCPVerifier (Matrix (Fin m) (Fin n) F × (Fin m → F)) size F fun (x : ℕ) => n

Equations

• LINEQ.verifier x = do let r ← LINEQ.sampleRandomVector m n F have u : Fin n → F := x.1.transpose.mulVec r let y ← liftM (OracleQuery.query (Sum.inr u)) pure (decide (y = x.2 ⬝ᵥ r))

theorem LINEQ.randomVector_card_clog_le {F : Type} [Fintype F] (m : ℕ) : Nat.clog 2 (Fintype.card (Fin m → F)) ≤ m * Nat.clog 2 (Fintype.card F)

theorem LINEQ.verifier_queryBound {F : Type} [Field F] [Fintype F] [DecidableEq F] [Inhabited F] {m n : ℕ} [Encodable F] (x : Matrix (Fin m) (Fin n) F × (Fin m → F)) : QueryBound (verifier x) 1 (m * Nat.clog 2 (Fintype.card F))

theorem LINEQ_LPCP {F : Type} [Field F] [Fintype F] [DecidableEq F] [Inhabited F] [SampleableType F] {m n : ℕ} : LINEQ F m n ∈ LPCP LINEQ.size 0 (1 / ↑(Fintype.card F)) F (fun (x : ℕ) => n) (fun (x : ℕ) => 1) fun (x : ℕ) => m * Nat.clog 2 (Fintype.card F)