Section 4.5 from STIR [ACFY24a]

References

• Arnon, G., Chiesa, A., Fenzi, G., and Yogev, E., STIR: Reed-Solomon proximity testing with fewer queries

theorem Combine.geometric_sum_units {F : Type u_1} [Field F] [DecidableEq F] {r : Fˣ} {a : ℕ} : ∑ j ∈ Finset.range (a + 1), ↑r ^ j = if r = 1 then ↑a + 1 else (1 - ↑r ^ (a + 1)) / (1 - ↑r)

Fact 4.10 Geometric series formula in a field, for a unit r : F.

def Combine.ri {m : ℕ} {F : Type u_1} [Field F] (dstar : ℕ) (degs : Fin m → ℕ) (r : F) (i : Fin m) : F

def Combine.combine {m : ℕ} {F : Type u_1} [Field F] {ι : Type u_2} (φ : ι ↪ F) (dstar : ℕ) (r : F) (fs : Fin m → ι → F) (degs : Fin m → ℕ) (x : ι) : F

Definition 4.11.1 Combine(d*, r, (f_0, d_0), …, (f_{m-1}, d_{m-1}))(x) := sum_{i < m} r_i * f_i(x) * ( sum_{l < (d* - d_i + 1)} (r * φ(x))^l )

@[simp]

theorem Combine.combine_dstar_zero {m : ℕ} {F : Type u_1} [Field F] {ι : Type u_2} {φ : ι ↪ F} {r : F} {fs : Fin m → ι → F} {degs : Fin m → ℕ} : combine φ 0 r fs degs = ∑ i : Fin m, r ^ ↑i • fs i

theorem Combine.combine_eq_cases {m : ℕ} {F : Type u_3} {ι : Type u_4} [Field F] [DecidableEq F] (φ : ι ↪ F) (dstar : ℕ) (r : F) (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ (i : Fin m), degs i ≤ dstar) : combine φ dstar r fs degs = fun (x : ι) => have q := φ x * r; if q ≠ 1 then ∑ i : Fin m, ri dstar degs r i * fs i x * (1 - q ^ (dstar - degs i + 1)) / (1 - q) else ∑ i : Fin m, ri dstar degs r i * fs i x * (↑dstar - ↑(degs i) + 1)

Definition 4.11.2 Combine(d*, r, (f_0, d_0), …, (f_{m-1}, d_{m-1}))(x) := if (r * φ(x)) = 1 then sum_{i < m} r_i * f_i(x) * (dstar - degree + 1) else sum_{i < m} r_i * f_i(x) * (1 - r * φ(x)^(dstar - degree + 1)) / (1 - r * φ(x))

def Combine.degCor {F : Type u_1} [Field F] {ι : Type u_2} (φ : ι ↪ F) (dstar degree : ℕ) (r : F) (f : ι → F) (x : ι) : F

Definition 4.12.1 DegCor(d*, r, f, degree)(x) := f(x) * ( sum_{ l < d* - d + 1 } (r * φ(x))^l )

theorem Combine.degreeCor_eq {F : Type u_1} [Field F] [DecidableEq F] {ι : Type u_2} (φ : ι ↪ F) (dstar degree : ℕ) (r : F) (f : ι → F) (hd : degree ≤ dstar) (x : ι) : have q := φ x * r; degCor φ dstar degree r f x = if q ≠ 1 then f x * (1 - q ^ (dstar - degree + 1)) / (1 - q) else f x * (↑dstar - ↑degree + 1)

Definition 4.12.2 DegCor(d*, r, f, d)(x) := f(x) * conditionalExp(x)

theorem Combine.master_lemma {F : Type} [Field F] {ι : Type} [Fintype ι] [Nonempty ι] {φ : ι ↪ F} {dstar m : ℕ} {fs : Fin m → ι → F} {degs : Fin m → ℕ} (hdegs : ∀ (i : Fin m), degs i ≤ dstar) {δ : NNReal} (hδLt : δ < min (1 - ReedSolomon.sqrtRate dstar φ) (1 - ↑(LinearCode.rate (ReedSolomon.code φ dstar)) - 1 / ↑(Fintype.card ι))) {S : Finset ι} (hS_card : (1 - δ) * ↑(Fintype.card ι) ≤ ↑S.card) {v : (i : Fin m) → Fin (Combine.block_size✝ dstar degs i) → Polynomial F} (hv_deg : ∀ (i : Fin m) (j : Fin (Combine.block_size✝ dstar degs i)), (v i j).degree < ↑dstar) (hv_eval : ∀ (i : Fin m) (j : Fin (Combine.block_size✝ dstar degs i)), ∀ x ∈ S, Polynomial.eval (φ x) (v i j) = φ x ^ ↑j * fs i x) (i : Fin m) (j : Fin (Combine.block_size✝ dstar degs i)) : (v i j).degree < ↑(degs i) + ↑↑j

theorem Combine.combine_theorem {F : Type} [Field F] [Fintype F] [DecidableEq F] {ι : Type} [Fintype ι] {φ : ι ↪ F} {dstar m : ℕ} (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ (i : Fin m), degs i ≤ dstar) (δ : NNReal) (hδPos : δ > 0) (hδLt : δ < min (1 - ReedSolomon.sqrtRate dstar φ) (1 - ↑(LinearCode.rate (ReedSolomon.code φ dstar)) - 1 / ↑(Fintype.card ι))) (hProb : (do let r ← PMF.uniformOfFintype F pure (δᵣ(combine φ dstar r fs degs, ↑(ReedSolomon.code φ dstar)) ≤ ↑δ)) True > (↑m * (↑dstar + 1) - ↑(∑ i : Fin m, degs i) - 1) * ↑(ProximityGap.errorBound δ dstar φ)) : ∃ (S : Finset ι), ↑S.card ≥ (1 - δ) * ↑(Fintype.card ι) ∧ ∃ (v : Fin m → ι → F), ∀ (i : Fin m), v i ∈ ReedSolomon.code φ (degs i) ∧ S ⊆ {j : ι | v i j = fs i j}

Lemma 4.13 Let dstar be the target degree, f₁,...,f_{m-1} : ι → F, 0 < degs₁,...,degs_{m-1} < dstar be degrees and δ ∈ (0, min{(1-BStar(ρ)), (1-ρ-1/|ι|)}) be a distance parameter, then Pr_{r ← F} [δᵣ(Combine(dstar,r,(f₁,degs₁),...,(fₘ,degsₘ)))] > err' (dstar, ρ, δ, m * (dstar + 1) - ∑ i degsᵢ)