Section 4.5 from STIR [ACFY24]

theorem Combine.geometric_sum_units {F : Type u_3} [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 )

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) (φ_neq_0 : ∀ (i : ι), φ i ≠ 0) : 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.combine_theorem {F : Type} [Field F] [Fintype F] [DecidableEq F] {ι : Type} [Fintype ι] [Nonempty ι] {φ : ι ↪ F} {dstar m degree : ℕ} (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ (i : Fin m), degs i ≤ dstar) (δ : ℝ) (hδPos : δ > 0) (hδLt : δ < min (1 - STIR.Bstar ↑(LinearCode.rate (ReedSolomon.code φ degree))) (1 - ↑(LinearCode.rate (ReedSolomon.code φ degree)) - 1 / ↑(Fintype.card ι))) (hProb : (do let r ← PMF.uniformOfFintype F pure (↑δᵣ(combine φ dstar r fs degs, ↑(ReedSolomon.code φ dstar)) ≤ δ)) True > ENNReal.ofReal (STIR.proximityError F dstar (↑(LinearCode.rate (ReedSolomon.code φ degree))) δ (m * (dstar + 1) - ∑ i : Fin m, degs i))) : ProximityGap.correlatedAgreement ↑(ReedSolomon.code φ degree) ⟨δ, ⋯⟩ fs

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ᵢ)