Section 4.5 from STIR [ACFY24]

theorem Combine.geometric_sum_units {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {r : Fˣ} {a : ℕ} : ∑ j : Fin (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) : Fin m → F

Coefficients r_i as used in the definition of Combine, for i < m, r_i := r^{i - 1 + sum_{j < i}(d* - d_j)}

Equations

• Combine.ri dstar degs r i = r ^ ((↑i).pred + ∑ j ∈ Finset.Iio i, (dstar - degs j))

def Combine.combineInterm {m : ℕ} {F : Type u_1} [Field F] {ι : Type u_2} {φ : ι ↪ F} (dstar : ℕ) (r : F) (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ (i : Fin m), degs i ≤ dstar) : ι → 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 )

Equations

• Combine.combineInterm dstar r fs degs hdegs x = ∑ i : Fin m, Combine.ri dstar degs r i * fs i x * ∑ l ∈ Finset.Iio (dstar - degs i + 1), (r * φ x) ^ l

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

if (r * φ(x)) = 1, then (dstar - degree + 1) else (1 - r * φ(x)^(dstar - degree + 1)) / (1 - r * φ(x))

Equations

• Combine.conditionalExp φ dstar degree r x = if r * φ x = 1 then ↑dstar - ↑degree + 1 else (1 - (r * φ x) ^ (dstar - degree + 1)) / (1 - r * φ x)

def Combine.combineFinal {m : ℕ} {F : Type u_1} [Field F] [DecidableEq F] {ι : Type u_2} (φ : ι ↪ F) (dstar : ℕ) (r : F) (fs : Fin m → ι → F) (degs : Fin m → ℕ) (hdegs : ∀ (i : Fin m), degs i ≤ dstar) : ι → F

Definition 4.11.2 Combine(d*, r, (f_0, d_0), …, (f_{m-1}, d_{m-1}))(x) := sum_{i < m} r_i * f_i(x) * conditionExp(dstar, degsᵢ, r)

Equations

• Combine.combineFinal φ dstar r fs degs hdegs x = ∑ i : Fin m, Combine.ri dstar degs r i * fs i x * Combine.conditionalExp φ dstar (degs i) r x

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

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

Equations

• Combine.degreeCorrInterm dstar degree r f hd x = f x * ∑ l ∈ Finset.Iio (dstar - degree + 1), (r * φ x) ^ l

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

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

Equations

• Combine.degreeCorrFinal dstar degree r f hd x = f x * Combine.conditionalExp φ dstar degree r x

theorem Combine.combine {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 - Bstar ↑(ρ ReedSolomon.code φ degree)) (1 - ↑(ρ ReedSolomon.code φ degree) - 1 / ↑(Fintype.card ι))) (hProb : ↑(do let r ← PMF.uniformOfFintype F pure (↑δᵣ(combineFinal φ dstar r fs degs hdegs, ↑(ReedSolomon.code φ dstar)) ≤ δ)) True > ENNReal.ofReal (err' F dstar (↑(ρ ReedSolomon.code φ degree)) δ (m * (dstar + 1) - ∑ i : Fin m, degs i))) : ∃ (S : Finset ι), ↑S.card ≥ (1 - δ) * ↑(Fintype.card ι) ∧ ∀ (i : Fin m), ∃ u ∈ ReedSolomon.code φ (degs i), ∀ x ∈ S, fs i x = u x

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