theorem ProximityGap.correlatedAgreement_affine_curves {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k deg : ℕ} {domain : ι ↪ F} {δ : NNReal} (hδ : δ ≤ 1 - ReedSolomon.sqrtRate deg domain) : δ_ε_correlatedAgreementCurves (↑(ReedSolomon.code domain deg)) δ (errorBound δ deg domain)

Theorem 1.5 (Correlated agreement for low-degree parameterised curves) in [BCIKS20].

Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and a curve passing through words u₀, ..., uκ, such that the probability that a random point on the curve is δ-close to the Reed-Solomon code is at most ε. Then, the words u₀, ..., uκ have correlated agreement.

noncomputable def ProximityGap.coeffs_of_close_proximity_curve {F : Type} [Field F] [Fintype F] [DecidableEq F] {n l : ℕ} (δ : ℚ≥0) (u : Fin l → Fin n → F) (V : Finset (Fin n → F)) : Finset F

The parameters for which the curve points are δ-close to a set V (typically, a linear code). This is the set S from the proximity gap paper.

theorem ProximityGap.large_agreement_set_on_curve_implies_correlated_agreement {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] {l : ℕ} {rho δ : ℚ≥0} {V : Finset (Fin n → F)} (hδ : δ ≤ (1 - rho) / 2) {u : Fin l → Fin n → F} (hS : n * l < (coeffs_of_close_proximity_curve δ u V).card) : coeffs_of_close_proximity_curve δ u V = Finset.univ ∧ ∃ (v : Fin l → Fin n → F), ∀ (z : F), δᵣ(Curve.polynomialCurveEval u z, Curve.polynomialCurveEval v z) ≤ δ ∧ ↑{x : Fin n | Finset.image u ≠ Finset.image v}.card ≤ δ * ↑n

If the set of points δ-close to the code V has at least n * l + 1 points, then there exists a curve defined by vectors v from V such that the points of curve u and curve v are δ-close with the same parameters. Moreover, u and v differ at at most δ * n positions.

noncomputable def ProximityGap.δ₀ (rho : ℚ) (m : ℕ) : ℝ

The distance bound from [BCIKS20].

theorem ProximityGap.large_agreement_set_on_curve_implies_correlated_agreement' {F : Type} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} [NeZero n] {l : ℕ} [Finite F] {m : ℕ} {rho δ : ℚ≥0} (hm : 3 ≤ m) {V : Finset (Fin n → F)} (hδ : ↑δ ≤ δ₀ (↑rho) m) {u : Fin l → Fin n → F} (hS : (1 + 1 / (2 * ↑m)) ^ 7 * ↑m ^ 7 / (3 * (↑rho).rpow ↑(3 / 2)) * ↑n ^ 2 * ↑l < ↑(coeffs_of_close_proximity_curve δ u V).card) : ∃ (v : Fin l → Fin n → F), ∀ (i : Fin l), v i ∈ V ∧ (1 - δ) * ↑n ≤ ↑{x : Fin n | ∀ (i : Fin l), u i x = v i x}.card

If the set of points on the curve defined by u close to V has at least ((1 + 1 / (2 * m)) ^ 7 * m ^ 7) / (3 * (Real.rpow rho (3 / 2 : ℚ))) * n ^ 2 * l + 1 points, then there exist vectors v from V that are (1 - δ) * n close to u.