instance ProximityGap.WeightedAgreement.instNonemptySubtypeForallMemFinsetFinCarrier {ι : Type} [Fintype ι] {F : Type} [Field F] [Fintype F] {domain : ι ↪ F} {deg : ℕ} : Nonempty ↥(ReedSolomon.finCarrier domain deg)

theorem ProximityGap.WeightedAgreement.weighted_correlated_agreement_for_parameterized_curves {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] [DecidableEq ι] {l k : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {δ : NNReal} {μ : ι → ↑(Set.Icc 0 1)} {M : ℕ} {α : NNReal} (hμ : ∀ (i : ι), ∃ (n : ℤ), ↑(μ i) = ↑n / ↑M) (hα : ReedSolomon.sqrtRate deg domain < α) (hα₁ : α < 1) (hproximity : (let curvePts := Curve.polynomialCurveFinite u; (do let y ← PMF.uniformOfFintype ↥curvePts pure (agree_set μ (↑y) (ReedSolomon.finCarrier domain deg) ≥ ↑α)) True) > ↑(↑l + 1) * ↑(errorBound δ deg domain)) (h_additionally : (let curvePts := Curve.polynomialCurveFinite u; (do let y ← PMF.uniformOfFintype ↥curvePts pure (agree_set μ (↑y) (ReedSolomon.finCarrier domain deg) ≥ ↑α)) True) ≥ ENNReal.ofReal ((↑l + 1) * (↑M * ↑(Fintype.card ι) + 1) / ↑(Fintype.card F) * (1 / ↑(min (α - ReedSolomon.sqrtRate deg domain) (ReedSolomon.sqrtRate deg domain / 20)) + 3 / ↑(ReedSolomon.sqrtRate deg domain)))) : ∃ (ι' : Finset ι) (v : Fin (l + 2) → ι → F), (∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) ∧ mu_set μ ι' ≥ ↑α ∧ ∀ (i : Fin (l + 2)), ∀ x ∈ ι', u i x = v i x

Weighted correlated agreement over curves. Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and a curve generated by vectors u, such that the probability that a random point on the curve is δ-close to Reed-Solomon code is at most ε. Then, the words u have weighted correlated agreement.

theorem ProximityGap.WeightedAgreement.weighted_correlated_agreement_for_parameterized_curves' {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {δ : NNReal} {μ : ι → ↑(Set.Icc 0 1)} {M m : ℕ} (hm : 3 ≤ m) (hμ : ∀ (i : ι), ∃ (n : ℤ), ↑(μ i) = ↑n / ↑M) {α : NNReal} (hα : ↑(ReedSolomon.sqrtRate deg domain) * (1 + 1 / (2 * ↑m)) ≤ ↑α) (hS : ↑{z : F | agree_set μ (Curve.polynomialCurveEval u z) (ReedSolomon.finCarrier domain deg) ≥ ↑α}.card > max ((1 + 1 / (2 * ↑m)) ^ 7 * ↑m ^ 7 * ↑(Fintype.card ι) ^ 2 * (↑l + 1) / (3 * ↑(ReedSolomon.sqrtRate deg domain) ^ 3)) ((2 * ↑m + 1) * (↑M * ↑(Fintype.card ι) + 1) * (↑l + 1) / ↑(ReedSolomon.sqrtRate deg domain))) : ∃ (v : Fin (l + 2) → ι → F), (∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) ∧ mu_set μ {i : ι | ∀ (j : Fin (l + 2)), u j i = v j i} ≥ ↑α

Weighted correlated agreement over curves. Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and a curve generated by vectors u, such that the probability that a random point on the curve is δ-close to Reed-Solomon code is at most ε. Then, the words u have weighted correlated agreement.

Version with different bounds.

theorem ProximityGap.WeightedAgreement.weighted_correlated_agreement_over_affine_spaces {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {μ : ι → ↑(Set.Icc 0 1)} {M : ℕ} {α : NNReal} (hα : ReedSolomon.sqrtRate deg domain < α) (hα₁ : α < 1) (hμ : ∀ (i : ι), ∃ (n : ℤ), ↑(μ i) = ↑n / ↑M) : (let spacePts := u 0 +ᵥ affineSpan F ↑(Finset.image (Fin.tail u) Finset.univ); (do let y ← PMF.uniformOfFintype ↥spacePts pure (agree_set μ (↑y) (ReedSolomon.finCarrier domain deg) ≥ ↑α)) True) > ↑(errorBound α deg domain) → (let spacePts := u 0 +ᵥ affineSpan F ↑(Finset.image (Fin.tail u) Finset.univ); (do let y ← PMF.uniformOfFintype ↥spacePts pure (agree_set μ (↑y) (ReedSolomon.finCarrier domain deg) ≥ ↑α)) True) ≥ ENNReal.ofReal ((↑M * ↑(Fintype.card ι) + 1) / ↑(Fintype.card F) * (1 / ↑(min (α - ReedSolomon.sqrtRate deg domain) (ReedSolomon.sqrtRate deg domain / 20)) + 3 / ↑(ReedSolomon.sqrtRate deg domain))) → ∃ (ι' : Finset ι) (v : Fin (l + 2) → ι → F), (∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) ∧ mu_set μ ι' ≥ ↑α ∧ ∀ (i : Fin (l + 2)), ∀ x ∈ ι', u i x = v i x

Weighted correlated agreement over affine spaces. Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and an affine space generated by vectors u, such that the probability that a random point from the space is δ-close to Reed-Solomon code is at most ε. Then, the words u have weighted correlated agreement.

theorem ProximityGap.WeightedAgreement.weighted_correlated_agreement_over_affine_spaces' {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {μ : ι → ↑(Set.Icc 0 1)} {α : NNReal} {M m : ℕ} (hm : 3 ≤ m) (hμ : ∀ (i : ι), ∃ (n : ℤ), ↑(μ i) = ↑n / ↑M) (hα : ↑(ReedSolomon.sqrtRate deg domain) * (1 + 1 / (2 * ↑m)) ≤ ↑α) : (let spacePts := u 0 +ᵥ affineSpan F ↑(Finset.image (Fin.tail u) Finset.univ); (do let y ← PMF.uniformOfFintype ↥spacePts pure (agree_set μ (↑y) (ReedSolomon.finCarrier domain deg) ≥ ↑α)) True) > ENNReal.ofReal (max ((1 + 1 / (2 * ↑m)) ^ 7 * ↑m ^ 7 * ↑(Fintype.card ι) ^ 2 / (3 * ↑(ReedSolomon.sqrtRate deg domain) ^ 3 * ↑(Fintype.card F))) ((2 * ↑m + 1) * (↑M * ↑(Fintype.card ι) + 1) / (↑(ReedSolomon.sqrtRate deg domain) * ↑(Fintype.card F)))) → ∃ (v : Fin (l + 2) → ι → F), (∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) ∧ mu_set μ {i : ι | ∀ (j : Fin (l + 2)), u j i = v j i} ≥ ↑α

Weighted correlated agreement over affine spaces. Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and an affine space generated by vectors u, such that the probability that a random point from the space is δ-close to Reed-Solomon code is at most ε. Then, the words u have weighted correlated agreement.

Version with different bounds.

theorem ProximityGap.WeightedAgreement.list_agreement_on_curve_implies_correlated_agreement_bound {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {μ : ι → ↑(Set.Icc 0 1)} {α : NNReal} {v : Fin (l + 2) → ι → F} (hv : ∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) {S' : Finset F} (hS'_card : S'.card > l + 1) (hS'_agree : ∀ z ∈ S', (agree μ (fun (x : ι) => (fun (x : ι) (z : F) => Curve.polynomialCurveEval u z x) x z) fun (x : ι) => (fun (x : ι) (z : F) => Curve.polynomialCurveEval v z x) x z) ≥ ↑α) : mu_set μ {x : ι | ∀ (i : Fin (l + 2)), u i x = v i x} > ↑α - (↑l + 1) / (↑S'.card - (↑l + 1))

Lemma 7.5 in [BCIKS20]. This is the "list agreement on a curve implies correlated agreement" lemma.

We are given two lists of functions u, v : Fin (l + 2) → ι → F, where each v i is a Reed-Solomon codeword of degree deg over the evaluation domain domain. From these lists we form the bivariate curve evaluations

• w x z = Curve.polynomialCurveEval u z x,
• wtilde x z = Curve.polynomialCurveEval v z x.

Fix a finite set S' ⊆ F with S'.card > l + 1, and a (product) measure μ on the evaluation domain ι. Assume that for every z ∈ S' the one-dimensional functions w · z and wtilde · z have agreement at least α with respect to μ. Then the set of points x on which all coordinates agree, i.e. u i x = v i x for every i, has μ-measure strictly larger than

α - (l + 1) / (S'.card - (l + 1)).

theorem ProximityGap.WeightedAgreement.sufficiently_large_list_agreement_on_curve_implies_correlated_agreement {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [DecidableEq F] {k l : ℕ} {u : Fin (l + 2) → ι → F} {deg : ℕ} {domain : ι ↪ F} {μ : ι → ↑(Set.Icc 0 1)} {α : NNReal} {M : ℕ} (hμ : ∀ (i : ι), ∃ (n : ℤ), ↑(μ i) = ↑n / ↑M) {v : Fin (l + 2) → ι → F} (hv : ∀ (i : Fin (l + 2)), v i ∈ ReedSolomon.code domain deg) {S' : Finset F} (hS'_card : S'.card > l + 1) (hS'_card₁ : S'.card ≥ (M * Fintype.card ι + 1) * (l + 1)) (hS'_agree : ∀ z ∈ S', (agree μ (fun (x : ι) => (fun (x : ι) (z : F) => Curve.polynomialCurveEval u z x) x z) fun (x : ι) => (fun (x : ι) (z : F) => Curve.polynomialCurveEval v z x) x z) ≥ ↑α) : mu_set μ {x : ι | ∀ (i : Fin (l + 2)), u i x = v i x} ≥ ↑α

Lemma 7.6 in [BCIKS20]. This is the "integral-weight" strengthening of the list-agreement-on-a-curve => correlated-agreement bound.

We have two lists of functions u, v : Fin (l + 2) → ι → F, where each v i is a Reed-Solomon codeword of degree deg over the evaluation domain domain. From these lists we form the bivariate curve evaluations

• w x z = Curve.polynomialCurveEval u z x,
• wtilde x z = Curve.polynomialCurveEval v z x.

The domain ι is finite and is equipped with a weighted measure μ, where each weight μ i is a rational with common denominator M. Let S' ⊆ F be a set of field points with

• S'.card > l + 1, and
• S'.card ≥ (M * Fintype.card ι + 1) * (l + 1).

Assume that for every z ∈ S' the µ-weighted agreement between w · z and wtilde · z is at least α. Then the µ-measure of the set of points where all coordinates agree, i.e. where u i x = v i x for every i, is at least α:

mu_set μ {x | ∀ i, u i x = v i x} ≥ α.