diff --git a/ArkLib.lean b/ArkLib.lean index 6b64cfc6ba..bbb8030dd0 100644 --- a/ArkLib.lean +++ b/ArkLib.lean @@ -102,8 +102,10 @@ import ArkLib.Data.CodingTheory.ProximityGap.DG25.Basic import ArkLib.Data.CodingTheory.ProximityGap.DG25.MainResults import ArkLib.Data.CodingTheory.ProximityGap.DG25.ReedSolomon import ArkLib.Data.CodingTheory.ProximityGap.Folding -import ArkLib.Data.CodingTheory.ProximityGap.MCAGenerator -import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators +import ArkLib.Data.CodingTheory.ProximityGenerator.AffineGenerator +import ArkLib.Data.CodingTheory.ProximityGenerator.Basic +import ArkLib.Data.CodingTheory.ProximityGenerator.MCAGenerator +import ArkLib.Data.CodingTheory.ProximityGenerator.PolynomialGenerator import ArkLib.Data.CodingTheory.ReedSolomon import ArkLib.Data.CodingTheory.ReedSolomon.Multilinear import ArkLib.Data.Domain.CosetFftDomain.Block diff --git a/ArkLib/Data/CodingTheory/Basic/LinearCode.lean b/ArkLib/Data/CodingTheory/Basic/LinearCode.lean index 3f6d12548b..70a041ad2e 100644 --- a/ArkLib/Data/CodingTheory/Basic/LinearCode.lean +++ b/ArkLib/Data/CodingTheory/Basic/LinearCode.lean @@ -257,17 +257,51 @@ scoped macro_rules word `c` to `T` as the word obtained by restricting the indexing set of `c` to `T`. We denote this by `c|[T]`. Definition 3.7 [BCGM25]. -/ -def projectedWord (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c - -notation:60 c "|[" T "]" => projectedWord c T +def projectedWord [Fintype ι] (c : ι → F) (T : Finset ι) : T → F := Set.restrict T c /-- Let `C` be a code of length `ι`. For every finite `ι`-subset `T`, we define the projected code `C|[T]` as the set of projected codewords `c|[T]`, for `c ∈ C`. Definition 3.7 [BCGM25]. -/ -def projectedCode (C : Set (ι → F)) (T : Finset ι) : Set (T → F) := - {w | ∃ c ∈ C, w = c|[T]} - -notation:60 C "|[" T "]" => projectedCode C T +def projectedCode [Fintype ι] (C : Set (ι → F)) (T : Finset ι) : Set (T → F) := + {w | ∃ c ∈ C, w = projectedWord c T} + +open Submodule + +def projectedCode_submod + [Field F] + [Fintype ι] + (LC : LinearCode ι F) + (T : Finset ι) : + Submodule F (T → F) := +{ + carrier := projectedCode (LC.carrier) T, + zero_mem' := by + unfold projectedCode projectedWord + simp only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq] + use 0 + exact And.intro (Submodule.zero_mem LC) (List.map_inj.mp rfl) + + add_mem' := by + unfold projectedCode projectedWord + intros x y hx hy + simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq] + rcases hx with ⟨cx, hx⟩ + rcases hy with ⟨cy, hy⟩ + use (cx + cy) + apply And.intro ((Submodule.add_mem_iff_right LC hx.1).mpr hy.1) + ext i + simp [hx.2, hy.2] + + smul_mem' := by + unfold projectedCode projectedWord + intros m x hx + simp_all only [carrier_eq_coe, SetLike.mem_coe, Set.mem_setOf_eq] + rcases hx with ⟨cx,hx⟩ + use m • cx + apply And.intro (smul_mem LC m hx.1) + ext i + simp [hx.2] +} /-- Let `T` be a finite subset of `ι`. If every word in a collection lies in the projected code `C|[T]`, then so do all `F`-linear combinations of these. -/ diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean index fbc2990c90..ba53208d7f 100644 --- a/ArkLib/Data/CodingTheory/Prelims.lean +++ b/ArkLib/Data/CodingTheory/Prelims.lean @@ -10,6 +10,7 @@ import Mathlib.LinearAlgebra.AffineSpace.Pointwise import Mathlib.LinearAlgebra.AffineSpace.Combination import Mathlib.RingTheory.Henselian + /-! # Coding-Theory Preliminaries -/ section TensorCombination @@ -34,6 +35,7 @@ def multilinearCombine {ϑ : ℕ} {ι : Type*} (u : (Fin (2 ^ ϑ)) → ι → A) (r : Fin ϑ → F) : (ι → A) := fun colIdx => ∑ rowIdx : Fin (2^ϑ), ((multilinearWeight r rowIdx) : F) • ((u rowIdx colIdx) : A) notation:20 r " |⨂| " u => multilinearCombine (u := u) (r := r) + end TensorCombination noncomputable section @@ -297,6 +299,29 @@ instance instNonemptyAffineSubspace_mk' {V : Type*} [AddCommGroup V] [Module F V (p : V) (direction : Submodule F V) : Nonempty (AffineSubspace.mk' p direction) := nonempty_subtype.mpr ⟨p, AffineSubspace.self_mem_mk' p direction⟩ +/-- The affine-space combination of codewords `U` at seed `x`: +`U 0 + ∑ i, x i • U (i+1)`, i.e. `vecMul (1, x) U`. -/ +abbrev affineComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) : ι → F := + Matrix.vecMul (Fin.cons 1 x) U + +/-- The linear combination `∑ i, l i • U (i+1)` of the "direction" codewords. -/ +abbrev linComb {s : ℕ} (U : Fin (s + 1) → (ι → F)) (l : Fin s → F) : ι → F := + fun k => ∑ i, l i * U i.succ k + +omit [Fintype ι] [DecidableEq F] [Fintype F] in +/-- The affine combination along the line `x ↦ v + t • lam` in seed space. -/ +lemma affineComb_line {s : ℕ} (U : Fin (s + 1) → (ι → F)) (v lam : Fin s → F) (t : F) : + affineComb U (v + t • lam) = affineComb U v + t • (linComb U lam) := by + have hsplit : (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) = + Fin.cons 1 v + t • (Fin.cons (0 : F) lam : Fin (s + 1) → F) := by + ext i + refine Fin.cases ?_ ?_ i <;> simp + have hlin : Matrix.vecMul (Fin.cons (0 : F) lam : Fin (s + 1) → F) U = linComb U lam := by + ext k + simp [Matrix.vecMul, dotProduct, Fin.sum_univ_succ, linComb] + change Matrix.vecMul (Fin.cons 1 (v + t • lam) : Fin (s + 1) → F) U = _ + rw [hsplit, Matrix.add_vecMul, Matrix.smul_vecMul, hlin] + end end Affine diff --git a/ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean b/ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean deleted file mode 100644 index 2d3e9223b0..0000000000 --- a/ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean +++ /dev/null @@ -1,120 +0,0 @@ -/- -Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Katerina Hristova --/ - -import ArkLib.Data.CodingTheory.ProximityGap.ProximityGenerators -import ArkLib.Data.Matrix.Basic -import ArkLib.Data.Probability.Instances - -/-! -## Main Results - -- Lemma 4.1 [BCGM25] : Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `A` a matrix -with a left pseudoinverse. Then the generator `G'` obtained from `G` by right multiplication by `A` -is an MCA generator with the same error `ε_mca` as `G`. -- Corollary 4.2 [BCGM25] : Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `κ` a -subset of `ℓ`. Then the projected generator over `κ` is an MCA generator with the same error as `G`. - -## References - -* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance -with Mutual Correlated Agreement*][BCGM25]. Full paper : https://eprint.iacr.org/2025/2051} --/ - -namespace LinearTransformations - -open NNReal ENNReal unitInterval LinearCode CoreDefinitions Matrix -open scoped ProbabilityTheory - -variable {ι : Type} [Fintype ι] - {F : Type} [Field F] - {ℓ ℓ' : Type} [Fintype ℓ] [Fintype ℓ'] - {S : Type} [Fintype S] - -/-- Let `G : S → 𝔽^ℓ` be a generator and let `A` be an `ℓ × ℓ'` matrix. Then `G' : S → 𝔽^ℓ'` is a -generator defined by `x ↦ G(x) · A`. -This is the generator `G'` inside Lemma 4.1 [BCGM25]. -/ -def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F := - fun x ↦ Matrix.vecMul (G x) A - -/-- Let `G : S → 𝔽^ℓ` be a generator and `κ` a subset of `ℓ`. Define a new generator -`G' : S → 𝔽^κ`, which we call a projected generator, by restricting the output of `G` to the indices -given by `κ`. -This is the generator `G'` inside Corollary 4.2 [BCGM25] -/ -def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F := - fun x ↦ Set.restrict κ (G x) - -/-- Let `U : ℓ' → (ι → F)` be a family of `ℓ'` codewords over `𝔽^ι`. Obtain a family of `ℓ` -codewords by acting on `U` by left multiplication with an `ℓ × ℓ'` matrix `A`. -/ -def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F) := - fun i k => ∑ j : ℓ', A i j * U j k - -/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `A` a matrix -with a left pseudoinverse. Then the generator `G'` obtained from `G` by right multiplication by `A` -is an MCA generator with the same error `ε_mca` as `G`. -Lemma 4.1 [BCGM25]. -/ -lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I) - (LC : LinearCode ι F) (hGMCA : IsMCAGenerator G ε_mca LC) - (A : Matrix ℓ ℓ' F) (hA : HasLeftPseudoInverse A) : - IsMCAGenerator (generatorByRightMul G A) ε_mca LC := by - intro U γ - have isMCA_generatorByRightMul_of_isMCA (x : S) : -IsMCA (generatorByRightMul G A) LC x U γ → IsMCA G LC x (matrixMulCodewords A U) γ := by - obtain ⟨B, hB⟩ := hA - rintro ⟨T, hT_card, hT_proj, j, hj⟩ - refine ⟨T, hT_card, ?_, ?_⟩ - · convert hT_proj using 1 - ext i - simp only [generatorByRightMul, Matrix.vecMul_vecMul] - congr! 2 - · contrapose! hj - convert LinearCode.projectedCode_linearCombination LC T (fun i => matrixMulCodewords A U i) - (fun i => B j i) (fun i => hj i) using 1 - · rfl - · apply congrArg (fun f : ι → F => f|[T]) - funext k - change U j k = B.mulVec (A.mulVec (fun j_2 => U j_2 k)) j - rw [Matrix.mulVec_mulVec (fun j_2 => U j_2 k) B A, hB, Matrix.one_mulVec] - exact le_trans (Pr_le_Pr_of_implies ($ᵖ S) _ _ fun x h => isMCA_generatorByRightMul_of_isMCA x h) - (hGMCA (matrixMulCodewords A U) γ) - -open Classical in -/-- Extend a collection of words `U : κ → (ι → F)` to `ℓ → (ι → F)` by filling in the extra -positions with zeros. -/ -noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F) := -fun i => if h : i ∈ κ then U ⟨i, h⟩ else 0 - -/-- If the MCA condition `IsMCA` holds for a projected generator, then `IsMCA` holds for the -original generator `G` with the zero-extension defined above. -/ -lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F) - (κ : Set ℓ) [Fintype κ] (U : κ → (ι → F)) (γ : I) (x : S) : - IsMCA (projectedGenerator G κ) LC x U γ → IsMCA G LC x (zeroExtend κ U) γ := by - have vecMul_projectedGenerator : - Matrix.vecMul (projectedGenerator G κ x) U = Matrix.vecMul (G x) (zeroExtend κ U) := by - ext i - simp only [Matrix.vecMul, dotProduct] - rw [← Finset.sum_subset (Finset.subset_univ (Set.toFinset κ))] - · refine Finset.sum_bij (fun j _ => j) ?_ ?_ ?_ ?_ <;> - simp [projectedGenerator, zeroExtend] - · intro x _ hx; simp [zeroExtend]; aesop - have zeroExtend_val (j : κ) : zeroExtend κ U j.val = U j := by - simp [zeroExtend, j.property] - rintro ⟨T, hT₁, hT₂, j, hT₃⟩ - exact ⟨T, hT₁, - by convert hT₂ using 1; exact funext fun _ => by simp [vecMul_projectedGenerator], - ⟨j, by rw [zeroExtend_val] ; assumption⟩⟩ - -/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `κ` a -subset of `ℓ`. Then the projected generator over `κ` is an MCA generator with the same error as `G`. -Corollary 4.2 [BCGM25]. -/ -lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → I) (LC : LinearCode ι F) -(hGMCA : IsMCAGenerator G ε_mca LC) (κ : Set ℓ) [Fintype κ] : - IsMCAGenerator (projectedGenerator G κ) ε_mca LC := by - intro U γ - exact le_trans (Pr_le_Pr_of_implies ($ᵖ S) _ _ - fun x h => isMCA_projectedGenerator_of_isMCA LC G κ U γ x h) - (hGMCA (zeroExtend κ U) γ) - -end LinearTransformations diff --git a/ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean b/ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean new file mode 100644 index 0000000000..f316f9c317 --- /dev/null +++ b/ArkLib/Data/CodingTheory/ProximityGenerator/AffineGenerator.lean @@ -0,0 +1,319 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova +-/ + +import ArkLib.Data.CodingTheory.ProximityGenerator.Basic +import ArkLib.Data.CodingTheory.ProximityGenerator.MCAGenerator +import ArkLib.Data.Probability.Notation +import ArkLib.Data.Probability.Instances +import ArkLib.Data.CodingTheory.Prelims +import Mathlib.Algebra.Azumaya.Basic +import Mathlib.Algebra.Ring.IsFormallyReal +import Mathlib.AlgebraicTopology.SimplexCategory.Basic +import Mathlib.Data.Int.Star +import Mathlib.FieldTheory.Finiteness +import Mathlib.RingTheory.Flat.TorsionFree + + +/-! +## Main Results + +- Lemma 7.1. [BCGM25]: Mutual correlated agreement (MCA) for the affine line generator implies +MCA for the affine space generator. + +## References + +* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance +with Mutual Correlated Agreement*][BCGM25]. Full paper : https://eprint.iacr.org/2025/2051} +-/ + +namespace AffineMCALemmas + +open unitInterval NNReal ENNReal CoreDefinitions LinearTransformations LinearCode Affine +open scoped ProbabilityTheory NNReal ENNReal BigOperators + + +variable {ι : Type} + {F : Type} [Field F] + +/-- The affine line combination `vecMul (1, t) W = W 0 + t • W 1`. -/ +lemma line_vecMul (W : Fin 2 → (ι → F)) (t : F) : + Matrix.vecMul (AffineLineGenerator F t) W = W 0 + t • W 1 := by + ext k + simp [AffineLineGenerator, Matrix.vecMul, dotProduct, Fin.sum_univ_two] + +/-- If the affine combination restricted to `T` is in a linear code, but +some `U j` restricted to `T` does not lie in the code, then there is a codeword `U (i + 1)` which is +not a codeword in the `T`-projected code. -/ +lemma exists_succ_not_mem [Fintype ι] {s : ℕ} (LC : LinearCode ι F) (T : Finset ι) + (U : Fin (s + 1) → (ι → F)) (x : Fin s → F) + (hv : projectedWord (affineComb U x) T ∈ projectedCode_submod LC T) + (hj : ∃ j : Fin (s + 1), projectedWord (U j) T ∉ projectedCode_submod LC T) : + ∃ i : Fin s, projectedWord (U i.succ) T ∉ projectedCode_submod LC T := by + contrapose! hj + intro j + induction j using Fin.inductionOn + · have h_aff : affineComb U x = U 0 + linComb U x := by + ext k; simp [affineComb, linComb, Matrix.vecMul, dotProduct, Fin.sum_univ_succ] + have hj' : ∀ i : Fin s, projectedWord (U i.succ) T ∈ projectedCode LC.carrier T := hj + have h_linComb : projectedWord (linComb U x) T ∈ projectedCode_submod LC T := by + change projectedWord (fun k => ∑ i, x i * U i.succ k) T ∈ projectedCode LC.carrier T + exact LinearCode.projectedCode_linearCombination LC T (fun i => U i.succ) x hj' + have h_split : projectedWord (affineComb U x) T = + projectedWord (U 0) T + projectedWord (linComb U x) T := by + rw [h_aff] + rfl + have hmem := Submodule.sub_mem _ (h_split ▸ hv) h_linComb + rwa [add_sub_cancel_right] at hmem + · exact hj _ + +/-- The quotient of the projected word space `T → F` by the projected code on `T`, used in the +kernel/rank-nullity argument of Step 2. -/ +abbrev projectedQuotient [Fintype ι] (LC : LinearCode ι F) (T : Finset ι) : Type := + (T → F) ⧸ LC.projectedCode_submod T + +open Classical in +/-- If some direction codeword `w i` does not project into the code on `T`, then the set of +coefficient vectors `l` whose combination `∑ i, l i • w i` projects into the code has cardinality +at most `|F| ^ (s-1)`. -/ +lemma proj_lincomb_ker_card_le [Fintype F] [Fintype ι] {s : ℕ} + (LC : LinearCode ι F) (T : Finset ι) (w : Fin s → (ι → F)) + (hne : ∃ i, projectedWord (w i) T ∉ projectedCode_submod LC T) : + (Finset.univ.filter (fun l : Fin s → F => + projectedWord (fun k => ∑ i, l i * w i k) T ∈ projectedCode_submod LC T)).card + ≤ (Fintype.card F) ^ (s - 1) := by + set g : (Fin s → F) →ₗ[F] projectedQuotient LC T := + Submodule.mkQ (LC.projectedCode_submod T) ∘ₗ + LinearMap.funLeft F F (Subtype.val : T → ι) ∘ₗ Fintype.linearCombination F w with hg_def + have hker : Module.finrank F (LinearMap.ker g) ≤ s - 1 := by + obtain ⟨i, hi⟩ := hne + have h_range : LinearMap.range g ≠ ⊥ := by + simp_all only [ne_eq, Submodule.eq_bot_iff, LinearMap.mem_range, LinearMap.coe_comp, + Function.comp_apply, Submodule.mkQ_apply, forall_exists_index, forall_apply_eq_imp_iff, + Submodule.Quotient.mk_eq_zero, not_forall] + exact ⟨Pi.single i 1, by + simp_all only [Fintype.linearCombination_apply_single, one_smul, g] + exact hi⟩ + have hrank_null := LinearMap.finrank_range_add_finrank_ker g + simp_all only [ne_eq, Module.finrank_fintype_fun_eq_card, Fintype.card_fin, ge_iff_le] + exact Nat.le_sub_one_of_lt + (lt_of_lt_of_le (Nat.lt_add_of_pos_left (Nat.pos_of_ne_zero (by aesop))) hrank_null.le) + have hcard : Fintype.card (LinearMap.ker g) ≤ (Fintype.card F) ^ (s - 1) := by + rw [Module.card_eq_pow_finrank (K := F)] + exact pow_le_pow_right₀ (Fintype.card_pos) hker + convert hcard using 1 + simp only [LinearMap.mem_ker, hg_def, LinearMap.coe_comp, Function.comp_apply, + Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] + rw [Fintype.card_subtype] + congr + ext + simp only [projectedWord, Fintype.linearCombination_apply, map_sum, map_smul] + congr! 1 + ext + simp [Finset.sum_apply, LinearMap.funLeft_apply] + +/-- If a sum of nonnegative integer counts over all `|F|^s` coefficient vectors is bounded by +`|F|^(s-1) * m`, then some coefficient vector achieves a count whose `|F|`-fold is at most `m`. -/ +lemma exists_avg_le [Fintype F] {s : ℕ} (hs : 1 ≤ s) (f : (Fin s → F) → ℕ) (m : ℕ) + (hsum : ∑ l, f l ≤ (Fintype.card F) ^ (s - 1) * m) : + ∃ l, (Fintype.card F : ℝ) * f l ≤ m := by + by_contra h_contra + push Not at h_contra + norm_cast at * + have hsum_lt := Finset.sum_lt_sum_of_nonempty (Finset.univ_nonempty) fun l _ => h_contra l + simp_all only [Finset.sum_const, Finset.card_univ, Fintype.card_pi, Finset.prod_const, + Fintype.card_fin, smul_eq_mul, ← Finset.mul_sum _ _ _] + cases s <;> simp_all [pow_succ', mul_assoc] + nlinarith + +open Classical in +/-- For a fixed direction `d`, some base point `v` makes the line `t ↦ v + t • d` hit the set `B'` +with (normalized) frequency at least the density of `B'`. -/ +lemma exists_dir_line_ge [Fintype F] [Nonempty F] {s : ℕ} + (d : Fin s → F) (B' : Finset (Fin s → F)) : + ∃ v : Fin s → F, + ((B'.card : ℝ) / (Fintype.card F) ^ s) ≤ + ((Finset.univ.filter (fun t : F => v + t • d ∈ B')).card : ℝ) / (Fintype.card F) := by + set q := Fintype.card F + have h_card_eq : ∀ t : F, Finset.card (Finset.filter (fun v => v + t • d ∈ B') Finset.univ) = + Finset.card B' := by + intro t + have hinj : Function.Injective (fun v : Fin s → F => v + t • d) := fun v w h => by simpa using h + rw [← Finset.card_image_of_injective _ hinj] + congr + ext + aesop + have h_inner : ∀ t : F, ∑ v : Fin s → F, (if v + t • d ∈ B' then 1 else 0) = B'.card := by + intro t + have := h_card_eq t + aesop + have h_swap : ∑ v : Fin s → F, (Finset.univ.filter (fun t : F => v + t • d ∈ B')).card = + ∑ t : F, ∑ v : Fin s → F, (if v + t • d ∈ B' then 1 else 0) := by + rw [Finset.sum_comm, Finset.sum_congr rfl] + aesop + have h_sum : + ∑ v : Fin s → F, (Finset.univ.filter (fun t : F => v + t • d ∈ B')).card = q * B'.card := by + rw [h_swap] + simp only [h_inner, Finset.sum_const, Finset.card_univ, smul_eq_mul] + rfl + contrapose! h_sum + have hsum_lt := Finset.sum_lt_sum_of_nonempty (Finset.univ_nonempty) fun v _ => h_sum v + simp_all only [Finset.sum_const, Finset.card_univ, Fintype.card_pi, Finset.prod_const, + Fintype.card_fin, nsmul_eq_mul, Nat.cast_pow, ne_eq] + rw [mul_div_cancel₀] at hsum_lt <;> simp_all only [← Finset.sum_div _ _ _, ne_eq, + pow_eq_zero_iff', Nat.cast_eq_zero, Fintype.card_ne_zero, false_and, not_false_eq_true] + rw [div_lt_iff₀] at hsum_lt <;> norm_cast at * <;> nlinarith [show q > 0 from Fintype.card_pos] + + +open Classical in +/-- There is a choice of two line-codewords `W` so that `(1 - 1/|F|)` times the density of +affine-space bad seeds is at most the density of affine-line bad seeds for `W`. -/ +lemma exists_line_bound [Fintype F] [Fintype ι] {s : ℕ} (hs : 1 ≤ s) + (LC : LinearCode ι F) (U : Fin (s + 1) → (ι → F)) (γ : unitInterval) : + ∃ W : Fin 2 → (ι → F), + (1 - 1 / (Fintype.card F : ℝ)) * + (((Finset.univ.filter (fun x : Fin s → F => + IsMCA (AffineSpaceGenerator F s) LC x U γ)).card : ℝ) / (Fintype.card F) ^ s) + ≤ ((Finset.univ.filter (fun t : F => + IsMCA (AffineLineGenerator F) LC t W γ)).card : ℝ) / (Fintype.card F) := by + set isB := fun x => IsMCA (AffineSpaceGenerator F s) LC x U γ + set Bset := Finset.univ.filter isB + set m := Bset.card + obtain ⟨T, hT⟩ : + ∃ T : (Fin s → F) → (Finset ι), ∀ x, isB x → (T x).card ≥ (Fintype.card ι) * (1 - (γ : ℝ)) ∧ + projectedWord (affineComb U x) (T x) ∈ projectedCode_submod LC (T x) ∧ + ∃ j, projectedWord (U j) (T x) ∉ projectedCode_submod LC (T x) := by + choose! T hT using fun x (hx : isB x) => hx + use T + obtain ⟨lam, hlam⟩ : ∃ lam : Fin s → F, (Bset.filter (fun x => projectedWord (linComb U lam) (T x) + ∈ projectedCode_submod LC (T x))).card ≤ m / (Fintype.card F : ℝ) := by + have h_per_seed_le : ∀ x ∈ Bset, ∑ lam : Fin s → F, (if projectedWord (linComb U lam) (T x) ∈ + projectedCode_submod LC (T x) then 1 else 0) ≤ (Fintype.card F) ^ (s - 1) := by + intro x hx + have h_ker : ∃ i : Fin s, projectedWord (U i.succ) (T x) ∉ projectedCode_submod LC (T x) := + exists_succ_not_mem LC (T x) U x (hT x (Finset.mem_filter.mp hx |>.2) |>.2.1) + (hT x (Finset.mem_filter.mp hx |>.2) |>.2.2) + have h_proj_bound := proj_lincomb_ker_card_le LC (T x) (fun i => U i.succ) h_ker + aesop + have h_sum : ∑ lam : Fin s → F, (Bset.filter (fun x => projectedWord (linComb U lam) (T x) ∈ + projectedCode_submod LC (T x))).card ≤ m * (Fintype.card F) ^ (s - 1) := by + convert Finset.sum_le_sum h_per_seed_le using 1 + · rfl + · rw [Finset.sum_comm, Finset.sum_congr rfl] + aesop + · simp +zetaDelta + have havg := exists_avg_le hs (fun lam => (Bset.filter (fun x => projectedWord (linComb U lam) + (T x) ∈ LC.projectedCode_submod (T x) ) |> Finset.card)) m ?_ + · exact havg.imp fun x hx => by rwa [le_div_iff₀' (Nat.cast_pos.mpr <| Fintype.card_pos)] + · linarith + obtain ⟨v, hv⟩ : ∃ v : Fin s → F, ((Bset.filter (fun x => ¬projectedWord (linComb U lam) (T x) ∈ + projectedCode_submod LC (T x))).card : ℝ) / (Fintype.card F) ^ s ≤ + ((Finset.univ.filter (fun t : F => v + t • lam ∈ Bset ∧ + ¬projectedWord (linComb U lam) (T (v + t • lam)) ∈ + projectedCode_submod LC (T (v + t • lam)))).card : ℝ) / (Fintype.card F) := by + have hdir := exists_dir_line_ge lam (Bset.filter fun x => ¬projectedWord (linComb U lam) (T x) ∈ + LC.projectedCode_submod (T x)) + aesop + refine ⟨![affineComb U v, linComb U lam], le_trans ?_ (hv.trans ?_ )⟩ + · convert mul_le_mul_of_nonneg_right + (show (1 - 1 / (Fintype.card F : ℝ)) * m ≤ ( + Finset.filter (fun x => ¬projectedWord (linComb U lam ) ( T x ) ∈ + LC.projectedCode_submod (T x)) Bset |> Finset.card : ℝ) from ?_) + (by positivity : 0 ≤ (Fintype.card F : ℝ) ⁻¹ ^ s) using 1 + · ring + · ring + · rw [one_sub_div, div_mul_eq_mul_div, div_le_iff₀] <;> norm_cast <;> norm_num + · rw [le_div_iff₀ (Nat.cast_pos.mpr <| Fintype.card_pos)] at hlam + norm_cast at * + rw [Int.subNatNat_eq_coe] + push_cast + have hcard_gt_one : Fintype.card F > 1 := Fintype.one_lt_card + have hpartition : Finset.card (Finset.filter + (fun x => projectedWord (linComb U lam) (T x) ∈ + projectedCode_submod LC (T x)) Bset) + + Finset.card (Finset.filter + (fun x => ¬projectedWord (linComb U lam) (T x) ∈ + projectedCode_submod LC (T x)) Bset) = m := by + rw [Finset.card_filter_add_card_filter_not] + nlinarith [hcard_gt_one, hpartition] + · gcongr + intro h + use T (v + ‹_› • lam) + simp_all only [ge_iff_le, Finset.mem_univ, line_vecMul, Fin.isValue, Matrix.cons_val_zero, + Matrix.cons_val_one, Matrix.cons_val_fin_one, Fin.exists_fin_two, not_false_eq_true, or_true, + and_true] + exact ⟨hT _ (Finset.mem_filter.mp h.1 |>.2 ) |>.1, + by simpa only [affineComb_line] using hT _ (Finset.mem_filter.mp h.1 |>.2 ) |>.2.1⟩ + +end AffineMCALemmas + +namespace AffineMCAMain + +open unitInterval NNReal ENNReal CoreDefinitions LinearTransformations LinearCode AffineMCALemmas +open scoped ProbabilityTheory NNReal ENNReal BigOperators + + +variable {ι : Type} [Fintype ι] + {F : Type} [Field F] [Fintype F] + +/-- Lemma 7.1. [BCGM25]. +The affine line generator `F → F²`, `x ↦ (1, x)`, having MCA error `ε_mca` for `LC` implies that +the affine space generator `Fˡ → Fˡ⁺¹`, `x ↦ (1, x)`, has MCA for `LC` with error +`(1 - 1/|F|)⁻¹ • ε_mca`. -/ +theorem AffineLine_MCA_AffineSpaceMCA {ℓ : ℕ} (hℓ : ℓ ≥ 2) (ε_mca : I → ℝ) (LC : LinearCode ι F) + (hGMCA : IsMCAGenerator (AffineLineGenerator F) ε_mca LC) : + letI a := (1 - 1 / Fintype.card F : ℝ) + letI ε_mca' := a⁻¹ • ε_mca + IsMCAGenerator (AffineSpaceGenerator F ℓ) ε_mca' LC := by + classical + intro U γ + set a : ℝ := (1 - 1 / (Fintype.card F : ℝ)) + have ha : 0 < a := by + have hq1 : (1 : ℝ) < (Fintype.card F : ℝ) := by exact_mod_cast Fintype.one_lt_card + rw [sub_pos, div_lt_one (by linarith)] + linarith + have hs : 1 ≤ ℓ := by omega + rw [prob_uniform_eq_ofReal] + have hcard : (Fintype.card (Fin ℓ → F) : ℝ) = (Fintype.card F : ℝ) ^ ℓ := by + norm_cast + rw [Fintype.card_fun, Fintype.card_fin] + rw [hcard] + simp only [Pi.smul_apply, smul_eq_mul] + obtain ⟨W, hW⟩ := AffineMCALemmas.exists_line_bound hs LC U γ + have hline := hGMCA W γ + rw [prob_uniform_eq_ofReal] at hline + set sp : ℝ := + ((Finset.univ.filter (fun x : Fin ℓ → F => + IsMCA (AffineSpaceGenerator F ℓ) LC x U γ)).card : ℝ) with hsp + set ln : ℝ := + ((Finset.univ.filter (fun t : F => + IsMCA (AffineLineGenerator F) LC t W γ)).card : ℝ) with hln + have hsp0 : 0 ≤ sp / (Fintype.card F : ℝ) ^ ℓ := by positivity + have hln0 : 0 ≤ ln / (Fintype.card F : ℝ) := by positivity + by_cases hε : 0 ≤ ε_mca γ + · have hlre : ln / (Fintype.card F : ℝ) ≤ ε_mca γ := + (ENNReal.ofReal_le_ofReal_iff hε).mp hline + have hchain : a * (sp / (Fintype.card F : ℝ) ^ ℓ) ≤ ε_mca γ := le_trans hW hlre + have hfin : sp / (Fintype.card F : ℝ) ^ ℓ ≤ a⁻¹ * ε_mca γ := by + rw [inv_mul_eq_div, le_div_iff₀ ha, mul_comm] + exact hchain + exact ENNReal.ofReal_le_ofReal hfin + · push Not at hε + have h0 : ENNReal.ofReal (ε_mca γ) = 0 := ENNReal.ofReal_of_nonpos (le_of_lt hε) + rw [h0] at hline + have hln_le : ln / (Fintype.card F : ℝ) ≤ 0 := + ENNReal.ofReal_eq_zero.mp (le_antisymm hline zero_le) + have hln_eq : ln / (Fintype.card F : ℝ) = 0 := le_antisymm hln_le hln0 + have hchain : a * (sp / (Fintype.card F : ℝ) ^ ℓ) ≤ 0 := by + rw [← hln_eq]; exact hW + have hsp_eq : sp / (Fintype.card F : ℝ) ^ ℓ = 0 := by + by_contra h + have hpos : 0 < sp / (Fintype.card F : ℝ) ^ ℓ := lt_of_le_of_ne hsp0 (Ne.symm h) + have : 0 < a * (sp / (Fintype.card F : ℝ) ^ ℓ) := mul_pos ha hpos + linarith + rw [hsp_eq] + simp + +end AffineMCAMain diff --git a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean b/ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean similarity index 73% rename from ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean rename to ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean index 3d2439ec2a..8a003c7b3a 100644 --- a/ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean +++ b/ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean @@ -26,6 +26,9 @@ function is a generator matrix for an MDS code probability that the generator satisfies the MCA condition is bounded above by `ε_mca`. - `tensor product of generators`: given two generators over a field `F` of output sizes `ℓ` and `ℓ'` respectively, we can define their tensor product componentwise. This is a generator on `F^ℓ ⊗ 𝔽^ℓ'` +- `affine line generator`: A generator of the form `G : F → F²` such that `x ↦ (1,x)`. +- `affine space generator`: A generator a generator of the form `G : F^ℓ → F^(ℓ + 1)` such that + `x ↦ (1,x)`. ## References @@ -54,11 +57,11 @@ abbrev Generator (S ℓ F : Type) : Type := S → (ℓ → F) a zero output from a non-zero vector is bounded above by `ε_ze`. Definition 3.11 [BCGM25]. -/ def IsZeroEvadingGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_ze : I) : - Prop := + Prop := (sSup {y | ∃ v : ℓ → F, v ≠ 0 ∧ y = Pr_{let x ←$ᵖ S}[dotProduct (G x) v = 0]}) ≤ ENNReal.ofReal ε_ze -/-- Let the set `S` be a product of `ℓ` subsets of `F`. A polynomial generator is a generator if +/-- Let the set `S` be a product of `s` subsets of `F`. A polynomial generator is a generator if there exist `ℓ` linearly independent multivariate polynomials, such that the output is an evaluation of the seed at each of these polynomials. Definition 3.19 [BCGM25]. -/ @@ -70,6 +73,11 @@ def IsPolynomialGeneratorOf {s : ℕ} (S : Fin s → Set F) (G : Generator (∀ (P : ℓ → MvPolynomial (Fin s) F) : Prop := LinearIndependent F P ∧ ∀ x : (∀ i, S i), G x = MvPolynomial.eval (fun i ↦ (x i : F)) ∘ P +/-- A polynomial generator where each `S i` is the whole field `F`. -/ +def IsPolynomialGeneratorOfFull {s : ℕ} (G : Generator (Fin s → F) ℓ F) + (P : ℓ → MvPolynomial (Fin s) F) : Prop := + LinearIndependent F P ∧ ∀ x : Fin s → F, G x = MvPolynomial.eval x ∘ P + /-- A matrix whose rows are the outputs of the generator function. Defined inside Definition 3.12 [BCGM25]. -/ def M_G {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) : Matrix S ℓ F := @@ -89,19 +97,19 @@ def IsMCA {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (LC : Line (x : S) (U : ℓ → (ι → F)) (γ : I) : Prop := let v := Matrix.vecMul (G x) (U) ∃ (T : Finset ι), (T.card : ℝ) ≥ (Fintype.card ι) * (1 - γ) ∧ - projectedWord v T ∈ projectedCode LC T ∧ - ∃ j : ℓ, projectedWord (U j) T ∉ projectedCode LC T + projectedWord v T ∈ projectedCode_submod LC T ∧ + ∃ j : ℓ, projectedWord (U j) T ∉ projectedCode_submod LC T /-- A generator has mutual correlated agreement (MCA) with error `ε_mca` if the probability that the generator satisfies the MCA condition is bounded above by `ε_mca`. Definition 3.14 [BCGM25]. -/ -def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → I) +def IsMCAGenerator {S : Type} [Nonempty S] [Fintype S] (G : Generator S ℓ F) (ε_mca : I → ℝ) (LC : LinearCode ι F) : Prop := ∀ U : ℓ → (ι → F), ∀ γ : I, Pr_{let x ←$ᵖ S}[(IsMCA G LC x U γ)] ≤ ENNReal.ofReal (ε_mca γ) -/-- Let `G : S →F^ℓ` and `G′: S′→F^ℓ` be two generators. Their tensor product is the generator -`G ⊗ G′: S × S′→ F^ℓ ⊗ F^ℓ′` defined by `(x,x′) ↦ G(x) ⊗ G′(x′)`. +/-- Let `G : S → F^ℓ` and `G′: S′ → F^ℓ` be two generators. Their tensor product is the generator +`G ⊗ G′: S × S′→ F^ℓ ⊗ F^ℓ′` defined by `(x , x′) ↦ G(x) ⊗ G′(x′)`. Definition 4.3 [BCGM25]. -/ def TensorGenerator {ℓ' : Type} [Fintype ℓ'] {S S' : Type} (G : Generator S ℓ F) (G' : Generator S' ℓ' F) : @@ -116,6 +124,18 @@ def TensorGenerator_Explicit {ℓ' : Type} [Fintype ℓ'] {S S' : Type} Generator (S × S') (ℓ × ℓ') F | (x, x'), (i, j) => G x i * G' x' j +omit [Fintype ι] in +/-- The tensor generator combination of a family `U : ℓ × ℓ' → (ι → F)` factors: it is the +`G x`-combination of the rows `i ↦ Matrix.vecMul (G' x') (U (i, ·))`, each of which is the +`G' x'`-combination of the `i`-th row of `U`. -/ +lemma vecMul_tensorGenerator_explicit {ℓ' : Type} [Fintype ℓ'] {S S' : Type} + (G : Generator S ℓ F) (G' : Generator S' ℓ' F) (U : ℓ × ℓ' → (ι → F)) (x : S) (x' : S') : + Matrix.vecMul (TensorGenerator_Explicit G G' (x, x')) U + = Matrix.vecMul (G x) (fun i => Matrix.vecMul (G' x') (fun j => U (i, j))) := by + funext k + simp [Matrix.vecMul, dotProduct, TensorGenerator_Explicit, Fintype.sum_prod_type, + Finset.mul_sum, mul_assoc] + /-- The canonical linear isomorphism between the tensor product of function spaces and the function space on the product type. -/ noncomputable def tensorProductPiFunEquiv (F : Type) [Field F] (ℓ ℓ' : Type) @@ -124,18 +144,34 @@ noncomputable def tensorProductPiFunEquiv (F : Type) [Field F] (ℓ ℓ' : Type) ((Pi.basisFun F ℓ).tensorProduct (Pi.basisFun F ℓ')).equivFun /-- The tensor product generator `TensorGenerator` and the explicit componentwise generator -`TensorGenerator_Explicit` agree under the canonical isomorphism between -`F^ℓ ⊗ F^ℓ′` and `(ℓ × ℓ') → F`. -/ +`TensorGenerator_Explicit` agree under the canonical isomorphism between `F^ℓ ⊗ F^ℓ′` and +`(ℓ × ℓ') → F`. -/ theorem TensorGenerator_eq_TensorGenerator_Explicit {ℓ' : Type} [Fintype ℓ'] [DecidableEq ℓ] [DecidableEq ℓ'] {S S' : Type} (G : Generator S ℓ F) (G' : Generator S' ℓ' F) (p : S × S') : tensorProductPiFunEquiv F ℓ ℓ' (TensorGenerator G G' p) = TensorGenerator_Explicit G G' p := by unfold tensorProductPiFunEquiv TensorGenerator TensorGenerator_Explicit convert (Pi.basisFun F ℓ).tensorProduct (Pi.basisFun F ℓ') |> fun b => - b.equivFun_apply ( G p.1 ⊗ₜ[F] G' p.2 ) using 1 + b.equivFun_apply (G p.1 ⊗ₜ[F] G' p.2) using 1 ext ⟨i, j⟩ simp only [Module.Basis.tensorProduct_repr_tmul_apply, Pi.basisFun_repr, smul_eq_mul] ring +/-- Let `F` be a field. +The affine line generator is a generator of the form `G : F → F²` such that `x ↦ (1,x)`. -/ +abbrev AffineLineGenerator (F : Type) [Field F] : Generator F (Fin 2) F := + fun x => ![1, x] + +/-- Let `F` be a field. +The affine space generator is a generator of the form `G : F^ℓ → F^(ℓ + 1) ` such that +`x ↦ (1,x)`. -/ +abbrev AffineSpaceGenerator (F : Type) [Field F] (ℓ : ℕ) : Generator (Fin ℓ → F) (Fin (ℓ + 1)) F := + fun x => Fin.cons 1 x + +/-- Let `F` be a field. The univariate powers generator `G : F → F ^ (d + 1)` is defined by +`x ↦ (1, x, x², … , x^d)`. -/ +def UnivariatePowers (d : ℕ) : Generator F (Fin (d + 1)) F := + fun x i => x ^ (i : ℕ) + end CoreDefinitions namespace PolynomialGenerator @@ -143,6 +179,7 @@ namespace PolynomialGenerator open NNReal ENNReal unitInterval MvPolynomial LinearCombination CoreDefinitions open scoped ProbabilityTheory ENNReal NNReal BigOperators +/-- Auxiliary lemma to prove that an error is in the unit interval. -/ lemma error_in_unit_interval (d : ℕ) (m : ℕ) (hm_pos : 0 < m) (hdm : d ≤ m) : (d / m : ℝ) ∈ I := by constructor · exact div_nonneg (Nat.cast_nonneg d) (le_of_lt (Nat.cast_pos.mpr hm_pos)) @@ -150,8 +187,8 @@ lemma error_in_unit_interval (d : ℕ) (m : ℕ) (hm_pos : 0 < m) (hdm : d ≤ m have hm_pos' : (0 : ℝ) < m := by exact_mod_cast hm_pos exact (div_le_one hm_pos').mpr hdm' -/-- The minimum of the cardinality of a family of sets nonempty sets, indexed by a possibly empty -set. Returns 1 if the indexing set is empty. -/ +/-- The minimum of the cardinality of a family of nonempty sets, indexed by a possibly empty set. +Returns `1` if the indexing set is empty. -/ def minSeedCard {F : Type} {s : ℕ} (S : Fin s → Set F) [∀ i, Fintype ↥(S i)] : ℕ := if h : 0 < s then Finset.inf' Finset.univ (Finset.univ_nonempty_iff.mpr (Fin.pos_iff_nonempty.mp h)) @@ -171,6 +208,7 @@ lemma minSeedCard_pos {F : Type} {s : ℕ} (S : Fin s → Set F) exact Fintype.card_pos_iff.mpr (Set.nonempty_coe_sort.2 (hne i)) · norm_num + /-- The minimum of the cardinality of a family of nonempty sets is smaller than the cardinality of each set in the family. -/ lemma minSeedCard_le {F : Type} {s : ℕ} (S : Fin s → Set F) @@ -205,20 +243,20 @@ theorem poly_gen_is_zero_evading and_imp] intros b x hx hb rw [hb] - change ((fun a => G a ⬝ᵥ x = 0) <$> $ᵖ ((i : Fin s) → ↥(S i))) True ≤ _ - rw [show (fun a => G a ⬝ᵥ x = 0) = fun a => - MvPolynomial.eval (fun i => (a i : F)) (∑ j, x j • P j) = 0 by - funext a - simp +decide [MvPolynomial.dotProduct_eq_eval_linearCombination, hG.2]] - refine (prob_eval_zero_le_div (∑ j, x j • P j) - (LinearCombination.linearCombination_ne_zero hG.1 hx) - (maxTotalDegree P) (minSeedCard S) - (MvPolynomial.totalDegree_linearCombination_le _ _ _ fun j => - Finset.le_sup (f := fun j => (P j |> MvPolynomial.totalDegree)) (Finset.mem_univ j)) - (minSeedCard_pos S) - (fun i => minSeedCard_le S (Fin.pos_iff_nonempty.mpr ⟨i⟩) i)).trans_eq ?_ - rw [ENNReal.ofReal_div_of_pos] <;> norm_cast - exact minSeedCard_pos S + convert prob_eval_zero_le_div (∑ j, x j • P j) _ (maxTotalDegree P) (minSeedCard S) _ _ _ using 1 + any_goals intro i; exact minSeedCard_le S (Fin.pos_iff_nonempty.mpr ⟨i⟩) i + any_goals assumption + · rfl + · convert rfl + ext + simp [MvPolynomial.dotProduct_eq_eval_linearCombination, hG.2] + · have := @ENNReal.ofReal_div_of_pos + rw [ENNReal.ofReal_div_of_pos] <;> norm_cast + exact minSeedCard_pos S + · exact LinearCombination.linearCombination_ne_zero hG.1 hx + · exact MvPolynomial.totalDegree_linearCombination_le _ _ _ fun j => + Finset.le_sup (f := fun j => (P j |> MvPolynomial.totalDegree)) (Finset.mem_univ j) + · exact minSeedCard_pos S end PolynomialGenerator diff --git a/ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean b/ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean new file mode 100644 index 0000000000..6056a78e35 --- /dev/null +++ b/ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean @@ -0,0 +1,254 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova +-/ + +import ArkLib.Data.CodingTheory.ProximityGenerator.Basic +import ArkLib.Data.Matrix.Basic +import ArkLib.Data.Probability.Instances + +/-! +## Main Results + +- Lemma 4.1 [BCGM25] : Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `A` a matrix +with a left pseudoinverse. Then the generator `G'` obtained from `G` by right multiplication by `A` +is an MCA generator with the same error `ε_mca` as `G`. +- Corollary 4.2 [BCGM25] : Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `κ` a +subset of `ℓ`. Then the projected generator over `κ` is an MCA generator with the same error as `G`. +- `isMCAGenerator_reindex` : MCA is invariant under bijective relabellings of the seed space and +of the output coordinates of a generator. +- Lemma 4.4 [BCGM25] : the tensor product of two MCA generators is an MCA generator, with the +weaker error `ε_mca + |ℓ| • ε_mca'` (`tensor_of_MCA_is_MCA`, fully proved) and with the tight +error `ε_mca + ε_mca'` of the paper (`tensor_of_MCA_is_MCA_tight`, currently `sorry`ed pending a +generalisation of `IsMCAGenerator` to module alphabets). + +## References + +* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance +with Mutual Correlated Agreement*][BCGM25]. Full paper : https://eprint.iacr.org/2025/2051} +-/ + +namespace LinearTransformations + +open NNReal ENNReal unitInterval LinearCode CoreDefinitions Matrix +open scoped ProbabilityTheory + +variable {ι : Type} [Fintype ι] + {F : Type} [Field F] + {ℓ ℓ' : Type} [Fintype ℓ] [Fintype ℓ'] + {S : Type} [Fintype S] + +/-- Let `G : S → 𝔽^ℓ` be a generator and let `A` be an `ℓ × ℓ'` matrix. Then `G' : S → 𝔽^ℓ'` is a +generator defined by `x ↦ G(x) · A`. +This is the generator `G'` inside Lemma 4.1 [BCGM25]. -/ +def generatorByRightMul (G : Generator S ℓ F) (A : Matrix ℓ ℓ' F) : Generator S ℓ' F := + fun x ↦ Matrix.vecMul (G x) A + +/-- Let `G : S → 𝔽^ℓ` be a generator and `κ` a subset of `ℓ`. Define a new generator +`G' : S → 𝔽^κ`, which we call a projected generator, by restricting the output of `G` to the indices +given by `κ`. +This is the generator `G'` inside Corollary 4.2 [BCGM25] -/ +def projectedGenerator (G : Generator S ℓ F) (κ : Set ℓ) : Generator S κ F := + fun x ↦ Set.restrict κ (G x) + +/-- Let `U : ℓ' → (ι → F)` be a family of `ℓ'` codewords over `𝔽^ι`. Obtain a family of `ℓ` +codewords by acting on `U` by left multiplication with an `ℓ × ℓ'` matrix `A`. -/ +def matrixMulCodewords (A : Matrix ℓ ℓ' F) (U : ℓ' → (ι → F)) : ℓ → (ι → F) := + fun i k => ∑ j : ℓ', A i j * U j k + +/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `A` a matrix +with a left pseudoinverse. Then the generator `G'` obtained from `G` by right multiplication by `A` +is an MCA generator with the same error `ε_mca` as `G`. +Lemma 4.1 [BCGM25]. -/ +lemma pseudoinverseGen [DecidableEq ℓ'] [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) + (LC : LinearCode ι F) (hGMCA : IsMCAGenerator G ε_mca LC) + (A : Matrix ℓ ℓ' F) (hA : HasLeftPseudoInverse A) : + IsMCAGenerator (generatorByRightMul G A) ε_mca LC := by + intro U γ + have isMCA_generatorByRightMul_of_isMCA (x : S) : +IsMCA (generatorByRightMul G A) LC x U γ → IsMCA G LC x (matrixMulCodewords A U) γ := by + obtain ⟨B, hB⟩ := hA + rintro ⟨T, hT_card, hT_proj, j, hj⟩ + refine ⟨T, hT_card, ?_, ?_⟩ + · convert hT_proj using 1 + ext i + simp only [generatorByRightMul, Matrix.vecMul_vecMul] + congr! 2 + · contrapose! hj + convert LinearCode.projectedCode_linearCombination LC T (fun i => matrixMulCodewords A U i) + (fun i => B j i) (fun i => hj i) using 1 + · rfl + · ext k + simp [matrixMulCodewords, ← Matrix.mul_apply, ← Matrix.mul_assoc, hB] + exact le_trans (Pr_le_Pr_of_implies ($ᵖ S) _ _ fun x h => isMCA_generatorByRightMul_of_isMCA x h) + (hGMCA (matrixMulCodewords A U) γ) + +open Classical in +/-- Extend a collection of words `U : κ → (ι → F)` to `ℓ → (ι → F)` by filling in the extra +positions with zeros. -/ +noncomputable def zeroExtend (κ : Set ℓ) (U : κ → (ι → F)) : ℓ → (ι → F) := +fun i => if h : i ∈ κ then U ⟨i, h⟩ else 0 + +/-- If the MCA condition `IsMCA` holds for a projected generator, then `IsMCA` holds for the +original generator `G` with the zero-extension defined above. -/ +lemma isMCA_projectedGenerator_of_isMCA (LC : LinearCode ι F) [Nonempty S] (G : Generator S ℓ F) + (κ : Set ℓ) [Fintype κ] (U : κ → (ι → F)) (γ : I) (x : S) : + IsMCA (projectedGenerator G κ) LC x U γ → IsMCA G LC x (zeroExtend κ U) γ := by + have vecMul_projectedGenerator : + Matrix.vecMul (projectedGenerator G κ x) U = Matrix.vecMul (G x) (zeroExtend κ U) := by + ext i + simp only [Matrix.vecMul, dotProduct] + rw [← Finset.sum_subset (Finset.subset_univ (Set.toFinset κ))] + · refine Finset.sum_bij (fun j _ => j) ?_ ?_ ?_ ?_ <;> + simp [projectedGenerator, zeroExtend] + · intro x _ hx; simp [zeroExtend]; aesop + have zeroExtend_val (j : κ) : zeroExtend κ U j.val = U j := by + simp [zeroExtend, j.property] + rintro ⟨T, hT₁, hT₂, j, hT₃⟩ + exact ⟨T, hT₁, + by convert hT₂ using 1; exact funext fun _ => by simp [vecMul_projectedGenerator], + ⟨j, by rw [zeroExtend_val] ; assumption⟩⟩ + +/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca`, and `κ` a +subset of `ℓ`. Then the projected generator over `κ` is an MCA generator with the same error as `G`. +Corollary 4.2 [BCGM25]. -/ +lemma generatorSubset [Nonempty S] (G : Generator S ℓ F) (ε_mca : I → ℝ) (LC : LinearCode ι F) +(hGMCA : IsMCAGenerator G ε_mca LC) (κ : Set ℓ) [Fintype κ] : + IsMCAGenerator (projectedGenerator G κ) ε_mca LC := by + intro U γ + exact le_trans (Pr_le_Pr_of_implies ($ᵖ S) _ _ + fun x h => isMCA_projectedGenerator_of_isMCA LC G κ U γ x h) + (hGMCA (zeroExtend κ U) γ) + +/-- Mutual correlated agreement is invariant under bijective relabellings of the seed space and of +the output coordinates of a generator. This lets us transport MCA statements along the canonical +equivalences (such as `Fin.consEquiv`) that arise when iterating tensor products of generators. -/ +lemma isMCAGenerator_reindex {S' : Type} [Fintype S'] [Nonempty S'] [Nonempty S] + (LC : LinearCode ι F) (G : Generator S ℓ F) (ε_mca : I → ℝ) + (hGMCA : IsMCAGenerator G ε_mca LC) (eS : S' ≃ S) (eL : ℓ ≃ ℓ') : + IsMCAGenerator (fun x' j' => G (eS x') (eL.symm j')) ε_mca LC := by + classical + intro U γ + -- The reindexed combination is the original combination of the relabelled words `U ∘ eL`. + have hvec : ∀ x' : S', Matrix.vecMul (fun j' => G (eS x') (eL.symm j')) U + = Matrix.vecMul (G (eS x')) (fun j => U (eL j)) := by + intro x' + funext kk + simp only [Matrix.vecMul, dotProduct] + rw [← Equiv.sum_comp eL fun j' => G (eS x') (eL.symm j') * U j' kk] + simp + have hiff : ∀ x' : S', + IsMCA (fun x' j' => G (eS x') (eL.symm j')) LC x' U γ + ↔ IsMCA G LC (eS x') (fun j => U (eL j)) γ := by + intro x' + constructor + · rintro ⟨T, hT, hmem, j', hj'⟩ + refine ⟨T, hT, ?_, eL.symm j', by simpa using hj'⟩ + rw [← hvec x'] + exact hmem + · rintro ⟨T, hT, hmem, j, hj⟩ + refine ⟨T, hT, ?_, eL j, hj⟩ + rw [hvec x'] + exact hmem + have hcard : (Finset.univ.filter fun x' : S' => + IsMCA G LC (eS x') (fun j => U (eL j)) γ).card + = (Finset.univ.filter fun x : S => IsMCA G LC x (fun j => U (eL j)) γ).card := + Finset.card_equiv eS fun x' => by simp + calc Pr_{let x' ←$ᵖ S'}[IsMCA (fun x' j' => G (eS x') (eL.symm j')) LC x' U γ] + = Pr_{let x' ←$ᵖ S'}[IsMCA G LC (eS x') (fun j => U (eL j)) γ] := Pr_congr hiff + _ = Pr_{let x ←$ᵖ S}[IsMCA G LC x (fun j => U (eL j)) γ] := by + rw [prob_uniform_eq_ofReal, prob_uniform_eq_ofReal, hcard, Fintype.card_congr eS] + _ ≤ ENNReal.ofReal (ε_mca γ) := hGMCA _ γ + +/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca` and `G' : S' → 𝔽^ℓ'` be an MCA +generator with error `ε_mca'`. Then the (explicit) tensor generator `G ⊗ G' : S × S' → 𝔽^(ℓ × ℓ')` +is an MCA generator. -/ +lemma tensor_of_MCA_is_MCA [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] (LC : LinearCode ι F) + (G : Generator S ℓ F) (ε_mca : I → ℝ) (hε_mca : ∀ γ, 0 ≤ ε_mca γ) + (hGMCA : IsMCAGenerator G ε_mca LC) + (G' : Generator S' ℓ' F) (ε_mca' : I → ℝ) (hε_mca' : ∀ γ, 0 ≤ ε_mca' γ) + (hG'MCA : IsMCAGenerator G' ε_mca' LC) : + IsMCAGenerator (TensorGenerator_Explicit G G') + (ε_mca + (Fintype.card ℓ : ℝ) • ε_mca') LC := by + intro U γ + -- `W x' i` is the `G'`-combination of the `i`-th "row" `(U (i, ·))` of the word matrix. + set W : S' → (ℓ → (ι → F)) := fun x' i => Matrix.vecMul (G' x') (fun j => U (i, j)) + -- Pointwise: an MCA violation of the tensor generator forces an MCA violation of `G` (on the + -- `W`-rows) or of `G'` (on some individual row). + have himp : ∀ p : S × S', IsMCA (TensorGenerator_Explicit G G') LC p U γ → + IsMCA G LC p.1 (W p.2) γ ∨ ∃ i, IsMCA G' LC p.2 (fun j => U (i, j)) γ := by + rintro ⟨x, x'⟩ ⟨T, hTcard, hTproj, ⟨i₀, j₀⟩, hij⟩ + rw [vecMul_tensorGenerator_explicit G G' U x x'] at hTproj + by_cases hcase : ∃ i, projectedWord (W x' i) T ∉ projectedCode_submod LC T + · exact Or.inl ⟨T, hTcard, hTproj, hcase⟩ + · simp only [not_exists, not_not] at hcase + exact Or.inr ⟨i₀, T, hTcard, hcase i₀, j₀, hij⟩ + -- Rewrite the target error as the matching sum of `ENNReal.ofReal`s. + have hEq : ENNReal.ofReal (ε_mca γ) + (Fintype.card ℓ : ℝ≥0∞) * ENNReal.ofReal (ε_mca' γ) + = ENNReal.ofReal ((ε_mca + (Fintype.card ℓ : ℝ) • ε_mca') γ) := by + rw [Pi.add_apply, Pi.smul_apply, smul_eq_mul, + ENNReal.ofReal_add (hε_mca γ) (mul_nonneg (by positivity) (hε_mca' γ)), + ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_natCast] + -- `G`-term: reorder so `S'` is sampled first, then apply `hGMCA` for each `x'`. + have hA : Pr_{ let p ←$ᵖ (S × S') }[ IsMCA G LC p.1 (W p.2) γ ] + ≤ ENNReal.ofReal (ε_mca γ) := by + rw [prob_split_uniform_sampling_of_equiv_prod (Equiv.prodComm S S')] + simp only [Equiv.prodComm_symm, Equiv.prodComm_apply, Prod.swap_prod_mk] + exact Pr_seq_le_of_forall_le ($ᵖ S) ($ᵖ S') + (fun x x' => IsMCA G LC x (W x') γ) (fun x' => hGMCA (W x') γ) + -- `G'`-term: the event is independent of `x ∈ S`; union bound over the `ℓ` rows. + have hB : Pr_{ let p ←$ᵖ (S × S') }[ ∃ i, IsMCA G' LC p.2 (fun j => U (i, j)) γ ] + ≤ (Fintype.card ℓ : ℝ≥0∞) * ENNReal.ofReal (ε_mca' γ) := by + rw [prob_split_uniform_sampling_of_prod] + refine Pr_seq_le_of_forall_le ($ᵖ S') ($ᵖ S) + (fun x' _ => ∃ i, IsMCA G' LC x' (fun j => U (i, j)) γ) (fun _ => ?_) + refine (Pr_exists_le _ _).trans ?_ + refine (Finset.sum_le_card_nsmul _ _ _ fun i _ => hG'MCA (fun j => U (i, j)) γ).trans ?_ + simp [Finset.card_univ, nsmul_eq_mul] + -- Combine: the tensor MCA event implies one of the two, then union + additivity. + refine le_trans (Pr_le_Pr_of_implies ($ᵖ (S × S')) _ _ himp) ?_ + refine le_trans (Pr_or_le ($ᵖ (S × S')) _ _) ?_ + rw [← hEq] + exact add_le_add hA hB + +/-- Let `G : S → 𝔽^ℓ` be an MCA generator with error `ε_mca` and `G' : S' → 𝔽^ℓ'` be an MCA +generator with error `ε_mca'`. Then the (explicit) tensor generator `G ⊗ G' : S × S' → 𝔽^(ℓ × ℓ')` +is an MCA generator with error `ε_mca + ε_mca'`. -/ +lemma tensor_of_MCA_is_MCA_tight [Nonempty S] {S' : Type} [Fintype S'] [Nonempty S'] + (LC : LinearCode ι F) + (G : Generator S ℓ F) (ε_mca : I → ℝ) (hGMCA : IsMCAGenerator G ε_mca LC) + (G' : Generator S' ℓ' F) (ε_mca' : I → ℝ) (hG'MCA : IsMCAGenerator G' ε_mca' LC) : + IsMCAGenerator (TensorGenerator_Explicit G G') (ε_mca + ε_mca') LC := by + sorry + +/-- The MCA error function for MDS codes, as defined in Theorem 6.1 [BCGM25]. -/ +noncomputable def ε_MCA_MDS [DecidableEq F] [Nonempty ι] (LC : LinearCode ι F) (ℓ s : ℕ) (η : ℝ) : + I → ℝ := + letI n : ℝ := Fintype.card ι + letI δ_C : ℝ := (Code.minRelHammingDistCode (LC.carrier) : ℝ) + letI ρ_C : ℝ := 1 - δ_C + letI γ_ℓ : ℝ := 1 - (ρ_C + η) ^ (1 / ℓ : ℝ) + fun γ => + if γ < (δ_C / (ℓ + 1) : ℝ) then + letI m' : ℝ := max (n * γ) 1 + m' * ((ℓ - 1) / s : ℝ) + else + if γ ≤ 1 - (ρ_C + η) ^ (1 / (ℓ + 1) : ℝ) then + (n * γ_ℓ / η) * ((ℓ - 1) / s) + + max (2 * (ℓ - 1) / (η * ((ρ_C + η) ^ (1 / ((ℓ + 1) : ℝ)) - (ρ_C + η) ^ (1 / ℓ : ℝ)) * s)) + (ℓ * (ℓ + 1) / (η * s) : ℝ) + else + 1 + +/-- Theorem 6.1 (MCA for MDS generators) [BCGM25]. -/ +theorem isMCAGenerator_of_isMDSGenerator {S : Type} [Nonempty S] [Fintype S] [DecidableEq F] + [Nonempty ι] + (G : Generator S ℓ F) + (hG : IsMDSGenerator G) + (hdim : LinearCode.dim (LinearCode.fromColGenMat (M_G G)) = Fintype.card ℓ) + (η : ℝ) (hη : 0 < η ∧ η < 1) (hℓ : 2 ≤ Fintype.card ℓ) + (LC : LinearCode ι F) : + IsMCAGenerator G (ε_MCA_MDS LC (Fintype.card ℓ) (Fintype.card S) η) LC := by sorry + +end LinearTransformations diff --git a/ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean b/ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean new file mode 100644 index 0000000000..55c814cba3 --- /dev/null +++ b/ArkLib/Data/CodingTheory/ProximityGenerator/PolynomialGenerator.lean @@ -0,0 +1,452 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova +-/ + +import ArkLib.Data.CodingTheory.ProximityGenerator.MCAGenerator +import ArkLib.Data.CodingTheory.ReedSolomon +import Mathlib.AlgebraicTopology.SimplexCategory.Basic +import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic + +/-! +## Main Results + +- Definition 8.1 (MCA error for univariate powers) [BCGM25]. +- Theorem 8.2 (MCA for polynomial generators) [BCGM25]. +- Statement of Lemma 9.3 [BCGM25] - sorried out. It depends on the Guruswami-Sudan part of Proximity +Gaps. +- Definition 9.1 MCA error function for Reed-Solomon codes [BCGM25]. +- Theorem 9.2 (Polynomial Generators have MCA for Reed-Solomon codes up to the Johnson bound) +(statement and proof assuming Lemma 9.3) [BCGM25]. + +## References + +* [Bordage, S., Chiesa, A., Guan, Z., Manzur, I., *All Polynomial Generators Preserve Distance +with Mutual Correlated Agreement*][BCGM25]. Full paper : https://eprint.iacr.org/2025/2051} +-/ + +namespace PolynomialGenIsMCA + +open unitInterval CoreDefinitions LinearTransformations + +variable {F : Type} [Field F] + {ι : Type} [Fintype ι] [Nonempty ι] + +/-- A function assinging the maximum degree in the `i`-the variable of the collection of +polynomials `P`. -/ +noncomputable def deg_max {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) : + Fin s → ℕ := fun i => Finset.sup Fintype.elems (fun j => (P j).degreeOf i) + +/-- Definition 8.1 (MCA error for univariate powers) [BCGM25]. +Note: In the paper, there is a hypothesis `η ∈ (0,1)`. This is omitted in the definition of `ξ` +since the hypothesis is not required to define `ξ`. However, we include it in statement that rely on +or utilise `ξ`. -/ +noncomputable def ξ [DecidableEq F] (LC : LinearCode ι F) (d m : ℕ) (η : ℝ) : + I → ℝ := + letI n : ℝ := Fintype.card ι + letI δ_C : ℝ := (Code.minRelHammingDistCode (LC.carrier) : ℝ) + letI ρ_C : ℝ := 1 - δ_C + letI γ_d : ℝ := 1 - (ρ_C + η) ^ (1 / (d + 1) : ℝ) + fun γ => + if γ < (δ_C / (d + 2) : ℝ) then + letI m' : ℝ := max (n * γ) 1 + m' * (d / m : ℝ) + else + if γ ≤ 1 - (ρ_C + η) ^ (1 / (d + 2) : ℝ) then + (n * γ_d / η) * (d / m) + + max (2 * d / (η * ((ρ_C + η) ^ (1 / (d + 2) : ℝ) - (ρ_C + η) ^ (1 / (d + 1) : ℝ)) * m)) + ((d + 1) * (d + 2) / (η * m) : ℝ) + else + 1 + +/-- The MDS error bound `ε_MCA_MDS` for output size `d + 1` (the univariate powers generator of +degree `d`, whose code has dimension `d + 1`) coincides with the univariate-powers error `ξ` of +degree `d`. -/ +lemma ε_MCA_MDS_eq_ξ [DecidableEq F] (LC : LinearCode ι F) (d m : ℕ) (η : ℝ) : + LinearTransformations.ε_MCA_MDS LC (d + 1) m η = ξ LC d m η := by + funext γ + simp only [LinearTransformations.ε_MCA_MDS, ξ, Nat.cast_add, Nat.cast_one] + rw [show (↑d + 1 + 1 : ℝ) = ↑d + 2 from by ring, + show (↑d + 1 - 1 : ℝ) = ↑d from by ring] + +/-- The iterated tensor product of a finite family of generators `Gᵢ : αᵢ → 𝔽^{ℓᵢ}`, over the +product seed space `∏ᵢ αᵢ`: `(x₁, ..., xₛ) ↦ ⊗ᵢ Gᵢ(xᵢ)`. Both the full-field tensor +`RSCode.tensorGeneratorPiUnivariate` and the subset tensor `tensorGeneratorPiUnivariateOn` are +instances of this construction. -/ +def tensorGeneratorPi {s : ℕ} {α : Fin s → Type} {ℓ : Fin s → Type} + (G : ∀ i, Generator (α i) (ℓ i) F) : Generator (∀ i, α i) (∀ i, ℓ i) F := + fun x j => ∏ i, G i (x i) (j i) + +omit [Nonempty ι] in +/-- The iterated tensor of a family of MCA generators has MCA for any linear code `LC`, with error +the sum `∑ᵢ εᵢ` of the factors' errors. This is the `s`-fold iteration of Lemma 4.4 +(`tensor_of_MCA_is_MCA_tight`) [BCGM25]. -/ +lemma tensorGeneratorPi_isMCAGenerator (LC : LinearCode ι F) : + ∀ {s : ℕ} {α : Fin s → Type} {ℓ : Fin s → Type} + [∀ i, Fintype (α i)] [∀ i, Nonempty (α i)] [∀ i, Fintype (ℓ i)] + (G : ∀ i, Generator (α i) (ℓ i) F) (ε : Fin s → I → ℝ), + (∀ i, IsMCAGenerator (G i) (ε i) LC) → + IsMCAGenerator (tensorGeneratorPi G) (fun γ => ∑ i, ε i γ) LC := by + intro s + induction s with + | zero => + intro α ℓ _ _ _ G ε _ U γ + classical + have hfalse : ∀ x : (∀ i : Fin 0, α i), ¬ IsMCA (tensorGeneratorPi G) LC x U γ := by + rintro x ⟨T, hT, hmem, j, hj⟩ + apply hj + have hvec : Matrix.vecMul (tensorGeneratorPi G x) U = U j := by + funext w + simp only [Matrix.vecMul, dotProduct] + rw [Fintype.sum_subsingleton _ j] + simp [tensorGeneratorPi] + rwa [hvec] at hmem + rw [prob_uniform_eq_ofReal, Finset.filter_false_of_mem fun x _ => hfalse x] + simp + | succ s ih => + intro α ℓ _ _ _ G ε hmca + letI : ∀ i : Fin s, Fintype (Fin.tail α i) := fun i => inferInstanceAs (Fintype (α i.succ)) + letI : ∀ i : Fin s, Nonempty (Fin.tail α i) := fun i => inferInstanceAs (Nonempty (α i.succ)) + letI : ∀ i : Fin s, Fintype (Fin.tail ℓ i) := fun i => inferInstanceAs (Fintype (ℓ i.succ)) + set eS : (∀ i : Fin (s + 1), α i) ≃ (α 0 × (∀ i : Fin s, Fin.tail α i)) := + (Fin.consEquiv α).symm with heS + set eL : (ℓ 0 × (∀ i : Fin s, Fin.tail ℓ i)) ≃ (∀ i : Fin (s + 1), ℓ i) := + Fin.consEquiv ℓ with heL + have hBin := tensor_of_MCA_is_MCA_tight LC + (G 0) (ε 0) (hmca 0) + (tensorGeneratorPi (α := Fin.tail α) (ℓ := Fin.tail ℓ) (Fin.tail G)) + (fun γ => ∑ i, Fin.tail ε i γ) + (ih (α := Fin.tail α) (ℓ := Fin.tail ℓ) (Fin.tail G) (Fin.tail ε) + (fun i => hmca (Fin.succ i))) + have hR := isMCAGenerator_reindex LC + (TensorGenerator_Explicit (G 0) + (tensorGeneratorPi (α := Fin.tail α) (ℓ := Fin.tail ℓ) (Fin.tail G))) + _ hBin eS eL + have hgen : (fun (x' : ∀ i : Fin (s + 1), α i) (j' : ∀ i : Fin (s + 1), ℓ i) => + TensorGenerator_Explicit (G 0) + (tensorGeneratorPi (α := Fin.tail α) (ℓ := Fin.tail ℓ) (Fin.tail G)) (eS x') (eL.symm j')) + = tensorGeneratorPi G := by + funext x' j' + rw [heS, heL] + simp only [TensorGenerator_Explicit, tensorGeneratorPi, Fin.tail, Fin.prod_univ_succ] + simp_all only [eS, eL] + rfl + have herr : ((ε 0) + fun γ => ∑ i, Fin.tail ε i γ) = (fun γ => ∑ i, ε i γ) := by + funext γ + simp only [Pi.add_apply, Fin.sum_univ_succ] + rfl + rw [hgen, herr] at hR + exact hR + +end PolynomialGenIsMCA + +namespace RSCode + +open unitInterval CoreDefinitions PolynomialGenIsMCA LinearTransformations MvPolynomial + Matrix + +variable {F : Type} [Field F] + {ι : Type} [Fintype ι] + (k : ℕ) -- degree of the polynomials + (D : ι ↪ F) -- the domain of evaluation + + +/-- Definition 9.1 MCA error function for Reed-Solomon codes [BCGM25]. -/ +noncomputable def ε_mca_RS [Fintype F] (n d m : ℕ) : I → ℝ := + let ρ_sqrt := ReedSolomon.sqrtRate k D + fun γ => + if γ ≤ 1 - (1 + (1 / (2 * m : ℝ))) * ρ_sqrt then + (|Fintype.card F| : ℝ)⁻¹ * (m + 1 / 2) ^ 7 * (3 * (ρ_sqrt) ^ 3)⁻¹.toReal * d * n ^ 2 + else + 1 + +/-- Let `F` be a field and `k, n, d, m ∈ ℕ` with `m ≥ 3`. Then the univariate powers generator has +MCA for a Reed-Solomon code over a domain `D` and degree `k` with error `ε_mca_RS` as defined +above. +Lemma 9.3 [BCGM25]. -/ +lemma univariate_powers_MCA [Fintype F] (n d m : ℕ) (hm : 3 ≤ m) : + IsMCAGenerator (UnivariatePowers d) (ε_mca_RS k D n d m) (ReedSolomon.code D k) := by + sorry + +/-- The multi-index (as a finitely supported function) associated to a bounded exponent vector. -/ +noncomputable def exponentFinsupp {s : ℕ} {d : Fin s → ℕ} (e : (i : Fin s) → Fin (d i + 1)) : + Fin s →₀ ℕ := Finsupp.equivFunOnFinite.symm (fun i => (e i : ℕ)) + +/-- Distinct bounded exponent vectors give distinct monomials. This lets a sum over the monomials +in the box `d` be rewritten as a sum over the finite index type `(i : Fin s) → Fin (d i + 1)`, +via `Finset.sum_image`. -/ +lemma exponentFinsupp_injective {s : ℕ} {d : Fin s → ℕ} : + Function.Injective (exponentFinsupp (d := d)) := by + intro e₁ e₂ h + funext i + have := congrArg (fun f => (f i : ℕ)) h + simpa using Fin.val_injective (by simpa [exponentFinsupp] using this) + +/-- Conversely, every monomial lying inside the box `d` is `exponentFinsupp` of some bounded +exponent vector. Together with `exponentFinsupp_injective` this identifies the box index type with +the set of monomials of individual degree at most `d`. -/ +lemma exists_exponentFinsupp_eq {s : ℕ} {d : Fin s → ℕ} {mo : Fin s →₀ ℕ} (h : ∀ i, mo i ≤ d i) : + ∃ e, exponentFinsupp (d := d) e = mo := + ⟨fun i => ⟨mo i, Nat.lt_succ_of_le (h i)⟩, by ext i; simp [exponentFinsupp]⟩ + + +/-- The `s`-fold tensor product of univariate powers generators. This is the generator defined in +the proof of Theorem 9.2 [BCGM25]. +`tilde{G} : (x_1, ..., x_s) ↦ ⊗_{i ∈ [s]} (1, x_i, ..., x_i^{d_i})`. -/ +def tensorGeneratorPiUnivariate {s : ℕ} (d : Fin s → ℕ) : + Generator (Fin s → F) ((i : Fin s) → Fin (d i + 1)) F := + fun x j => ∏ i, x i ^ (j i : ℕ) + +/-- The `s`-fold tensor product of univariate powers generators has MCA for any linear code +`LC`, with error the sum `∑ i, ε (d i)` of the factors' errors, provided each univariate powers +generator has MCA for `LC` with error `ε e`. +This is the `s`-fold iteration of Lemma 4.4 (tensor products preserve MCA) [BCGM25]. -/ +lemma tensorGeneratorPiUnivariate_isMCAGenerator [Fintype F] (LC : LinearCode ι F) + (ε : ℕ → I → ℝ) (huniv : ∀ e : ℕ, IsMCAGenerator (UnivariatePowers e) (ε e) LC) : + ∀ {s : ℕ} (d : Fin s → ℕ), + IsMCAGenerator (tensorGeneratorPiUnivariate d) (fun γ => ∑ i, ε (d i) γ) LC := by + intro s d + exact tensorGeneratorPi_isMCAGenerator LC (fun i => UnivariatePowers (d i)) (fun i => ε (d i)) + (fun i => huniv (d i)) + +/-- The coefficient matrix expressing the polynomial generator `G` as a right multiplication of the +tensor generator: the entry at `(e, j)` is the coefficient of the monomial `exponentFinsupp e` in +the polynomial `P j`. + +This is the matrix `A ∈ F^{k×ℓ}` of [BCGM25, Section 2.2], with `k = ∏ᵢ (dᵢ + 1)`. Equivalently, it +is `Aᵀ` for the `A ∈ F^{ℓ×k}` used in the proof of Theorem 9.2 [BCGM25]. -/ +noncomputable def coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ] (P : ℓ → MvPolynomial (Fin s) F) + (d : Fin s → ℕ) : Matrix ((i : Fin s) → Fin (d i + 1)) ℓ F := + fun e j => (P j).coeff (exponentFinsupp e) + +/-- The polynomial generator `G` is the right multiplication of the tensor generator by the +coefficient matrix (`G = G̃ · Aᵀ` in the proof of Theorem 9.2 [BCGM25]). -/ +lemma generatorByRightMul_coeffMatrix {s : ℕ} {ℓ : Type} [Fintype ℓ] + (P : ℓ → MvPolynomial (Fin s) F) (d : Fin s → ℕ) + (hdeg : ∀ (j : ℓ) (i : Fin s), (P j).degreeOf i ≤ d i) + (G : Generator (Fin s → F) ℓ F) (hG : ∀ x, G x = MvPolynomial.eval x ∘ P) : + generatorByRightMul (tensorGeneratorPiUnivariate d) (coeffMatrix P d) = G := by + funext x j + rw [hG] + simp only [Function.comp_apply, generatorByRightMul, Matrix.vecMul, dotProduct, + tensorGeneratorPiUnivariate, coeffMatrix] + have hsub : (P j).support ⊆ Finset.univ.image (exponentFinsupp (d := d)) := by + intro mo hmo + obtain ⟨e, he⟩ := + exists_exponentFinsupp_eq fun i => le_trans (monomial_le_degreeOf i hmo) (hdeg j i) + exact Finset.mem_image.mpr ⟨e, Finset.mem_univ _, he⟩ + rw [eval_eq', Finset.sum_subset hsub + (fun mo _ hmo => by simp [MvPolynomial.notMem_support_iff.mp hmo]), + Finset.sum_image (fun a _ b _ h => exponentFinsupp_injective h)] + exact Finset.sum_congr rfl fun e _ => by simp [mul_comm, exponentFinsupp] + +/-- The coefficient matrix expressing the polynomial generator `G` as a right multiplication of +the tensor generatorhas a left inverse. -/ +lemma coeffMatrix_hasLeftPseudoInverse {s : ℕ} {ℓ : Type} [Fintype ℓ] [DecidableEq ℓ] + (P : ℓ → MvPolynomial (Fin s) F) (d : Fin s → ℕ) + (hdeg : ∀ (j : ℓ) (i : Fin s), (P j).degreeOf i ≤ d i) (hP : LinearIndependent F P) : + HasLeftPseudoInverse (coeffMatrix P d) := by + set A := coeffMatrix P d with hA + have hinj : LinearMap.ker A.mulVecLin = ⊥ := by + rw [LinearMap.ker_eq_bot'] + intro v hv + set Q : MvPolynomial (Fin s) F := ∑ j, v j • P j with hQ + have hcoeff : ∀ e : (i : Fin s) → Fin (d i + 1), Q.coeff (exponentFinsupp e) = 0 := by + intro e + have hve := congrFun hv e + simpa [hA, coeffMatrix, Matrix.mulVecLin, Matrix.mulVec, dotProduct, hQ, + MvPolynomial.coeff_sum, MvPolynomial.coeff_smul, mul_comm] using hve + have hQ0 : Q = 0 := by + ext mo + rw [MvPolynomial.coeff_zero] + by_cases hmem : ∀ i, mo i ≤ d i + · obtain ⟨e, he⟩ := exists_exponentFinsupp_eq hmem + exact he ▸ hcoeff e + · simp only [not_forall, not_le] at hmem + obtain ⟨i, hi⟩ := hmem + apply MvPolynomial.notMem_support_iff.mp + intro hmo + rw [hQ] at hmo + obtain ⟨j, _, hj⟩ := Finset.mem_biUnion.mp (MvPolynomial.support_sum hmo) + have hj' : mo ∈ (P j).support := MvPolynomial.support_smul hj + exact absurd (le_trans (monomial_le_degreeOf i hj') (hdeg j i)) (by omega) + exact funext fun j => Fintype.linearIndependent_iff.mp hP v (hQ.symm.trans hQ0) j + obtain ⟨g, hg⟩ := LinearMap.exists_leftInverse_of_injective A.mulVecLin hinj + refine ⟨LinearMap.toMatrix' g, ?_⟩ + have hcomp : LinearMap.toMatrix' (g.comp A.mulVecLin) = LinearMap.toMatrix' g * A := by + rw [LinearMap.toMatrix'_comp] + congr 1 + rw [← Matrix.toLin'_apply', LinearMap.toMatrix'_toLin'] + rw [hg, LinearMap.toMatrix'_id] at hcomp + exact hcomp.symm + +/-- Take a Reed–Solomon code of polynomials of degree less than `k` over an evaluation domain +`D`. Let `G` be a polynomial generator where each `S` is the whole field `F`. +Then, for every `m ≥ 3`, `G` has MCA for with error `∑ i, ε_mca_RS`. +Theorem 9.2 [BCGM25]. -/ +lemma polynomial_gen_MCA_RScode [Fintype F] (n m : ℕ) (hm : 3 ≤ m) {ℓ : Type} [Fintype ℓ] {s : ℕ} + {P : ℓ → MvPolynomial (Fin s) F} (G : Generator ((Fin s) → F) ℓ F) + (hG : IsPolynomialGeneratorOfFull G P) : + letI ε := ∑ i : Fin s, ε_mca_RS k D n (deg_max P i) m + IsMCAGenerator G ε (ReedSolomon.code D k) := by + classical + show IsMCAGenerator G (∑ i : Fin s, ε_mca_RS k D n (deg_max P i) m) (ReedSolomon.code D k) + have hdeg : ∀ (j : ℓ) (i : Fin s), (P j).degreeOf i ≤ deg_max P i := by + intro j i + simpa [deg_max] using + Finset.le_sup (f := fun j => (P j).degreeOf i) (Fintype.complete j) + have htensor := tensorGeneratorPiUnivariate_isMCAGenerator (ReedSolomon.code D k) + (fun e => ε_mca_RS k D n e m) (fun e => univariate_powers_MCA k D n e m hm) (deg_max P) + have hmul := pseudoinverseGen (tensorGeneratorPiUnivariate (deg_max P)) + (fun γ => ∑ i, ε_mca_RS k D n (deg_max P i) m γ) (ReedSolomon.code D k) htensor + (coeffMatrix P (deg_max P)) + (coeffMatrix_hasLeftPseudoInverse P (deg_max P) hdeg hG.1) + rw [generatorByRightMul_coeffMatrix P (deg_max P) hdeg G hG.2] at hmul + rwa [_root_.funext fun γ => (Finset.sum_apply γ Finset.univ _).symm] at hmul + +end RSCode + +namespace PolynomialGenIsMCA + +open CoreDefinitions LinearTransformations LinearCode RSCode ReedSolomon +open unitInterval + +variable {F : Type} [Field F] + +/-- The univariate powers generator of degree `d` restricted to a subset `s ⊆ F` as its seed +space: `x ↦ (1, x, …, x^d)`. This is the univariate factor used in the proof of Theorem 8.2 +[BCGM25], now over the seed space `s` rather than the whole field. -/ +def UnivariatePowersOn (s : Set F) (d : ℕ) : Generator s (Fin (d + 1)) F := + fun x j => (x : F) ^ (j : ℕ) + +/-- The code `C_G` of the restricted univariate powers generator is the Reed–Solomon code of +degree less than `d + 1` over `s`: its `M_G` matrix is the non-square Vandermonde matrix. -/ +lemma UnivariatePowersOn.code_eq_reedSolomon (s : Set F) [Fintype s] [Nonempty s] (d : ℕ) : + fromColGenMat (M_G (UnivariatePowersOn s d)) + = ReedSolomon.code (Function.Embedding.subtype (· ∈ s)) (d + 1) := by + have hMG : M_G (UnivariatePowersOn s d) + = Vandermonde.nonsquare (d + 1) ((Function.Embedding.subtype (· ∈ s)) : s → F) := by + ext x j + simp [M_G, UnivariatePowersOn, Vandermonde.nonsquare] + rw [hMG, genMatIsVandermonde] + +/-- The restricted univariate powers generator is an MDS generator (its code is Reed–Solomon, +hence MDS). -/ +lemma UnivariatePowersOn.isMDSGenerator [DecidableEq F] (s : Set F) [Fintype s] [Nonempty s] + (d : ℕ) (h : d + 1 ≤ Fintype.card ↥s) : IsMDSGenerator (UnivariatePowersOn s d) := by + unfold IsMDSGenerator + rw [UnivariatePowersOn.code_eq_reedSolomon] + exact ReedSolomon.isMDS_code h + +/-- The restricted univariate powers generator has MCA for every linear code with error `ξ`. +For `d ≥ 1` this is Theorem 6.1 (`IsMDSGenerator.isMCAGenerator`) together with the identification +`ε_MCA_MDS = ξ` (`ε_MCA_MDS_eq_ξ`); for `d = 0` the MCA event is vacuous, so the error `0 ≤ ξ` +suffices. -/ +lemma UnivariatePowersOn.isMCAGenerator {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq F] + (s : Set F) [Fintype s] [Nonempty s] + (LC : LinearCode ι F) (d : ℕ) (η : ℝ) (hη : 0 < η ∧ η < 1) + (h : d + 1 ≤ Fintype.card ↥s) : + IsMCAGenerator (UnivariatePowersOn s d) (ξ LC d (Fintype.card ↥s) η) LC := by + rcases Nat.eq_zero_or_pos d with hd | hd + · subst hd + classical + haveI : Subsingleton (Fin (0 + 1)) := inferInstanceAs (Subsingleton (Fin 1)) + intro U γ + have hfalse : ∀ x : ↥s, ¬ IsMCA (UnivariatePowersOn s 0) LC x U γ := by + rintro x ⟨T, hT, hmem, j, hj⟩ + apply hj + have hvec : Matrix.vecMul (UnivariatePowersOn s 0 x) U = U j := by + funext w + simp only [Matrix.vecMul, dotProduct] + rw [Fintype.sum_subsingleton _ j] + simp [UnivariatePowersOn] + rwa [hvec] at hmem + rw [prob_uniform_eq_ofReal, Finset.filter_false_of_mem fun x _ => hfalse x] + simp + · have hℓ : 2 ≤ Fintype.card (Fin (d + 1)) := by rw [Fintype.card_fin]; omega + have hdim : LinearCode.dim (fromColGenMat (M_G (UnivariatePowersOn s d))) + = Fintype.card (Fin (d + 1)) := by + rw [UnivariatePowersOn.code_eq_reedSolomon, ReedSolomon.dim_eq_deg_of_le' h, Fintype.card_fin] + have hmca := isMCAGenerator_of_isMDSGenerator (UnivariatePowersOn s d) + (UnivariatePowersOn.isMDSGenerator s d h) hdim η hη hℓ LC + rwa [Fintype.card_fin, ε_MCA_MDS_eq_ξ] at hmca + +/-- The `s`-fold tensor product of restricted univariate powers generators, over the product seed +space `∏ᵢ Sᵢ`: `(x₁, …, xₛ) ↦ ⊗ᵢ (1, xᵢ, …, xᵢ^{dᵢ})`. -/ +def tensorGeneratorPiUnivariateOn {s : ℕ} (S : Fin s → Set F) (d : Fin s → ℕ) : + Generator (∀ i, (S i)) ((i : Fin s) → Fin (d i + 1)) F := + fun x j => ∏ i, ((x i) : F) ^ (j i : ℕ) + +/-- The tensor product of the restricted univariate powers generators has MCA for any linear code +`LC`, with error the sum `∑ᵢ ξ (dᵢ)` of the factors' errors. This is the `s`-fold iteration of +Lemma 4.4 (`tensor_of_MCA_is_MCA_tight`) [BCGM25], with each factor's MCA supplied by +`UnivariatePowersOn.isMCAGenerator`. -/ +lemma tensorGeneratorPiUnivariateOn_isMCAGenerator {ι : Type} [Fintype ι] [Nonempty ι] + [DecidableEq F] (LC : LinearCode ι F) (η : ℝ) (hη : 0 < η ∧ η < 1) + {s : ℕ} (S : Fin s → Set F) [∀ i, Fintype ↥(S i)] [∀ i, Nonempty ↥(S i)] + (d : Fin s → ℕ) (hcard : ∀ i, d i + 1 ≤ Fintype.card ↥(S i)) : + IsMCAGenerator (tensorGeneratorPiUnivariateOn S d) + (fun γ => ∑ i, ξ LC (d i) (Fintype.card ↥(S i)) η γ) LC := + tensorGeneratorPi_isMCAGenerator LC (fun i => UnivariatePowersOn (S i) (d i)) + (fun i => ξ LC (d i) (Fintype.card ↥(S i)) η) + (fun i => UnivariatePowersOn.isMCAGenerator (S i) LC (d i) η hη (hcard i)) + +/-- The polynomial generator `G` is the right multiplication of the restricted tensor generator by +the coefficient matrix (`G = G̃ · Aᵀ` in the proof of Theorem 8.2 [BCGM25]). -/ +lemma generatorByRightMul_coeffMatrix_sub {s : ℕ} {ℓ : Type} [Fintype ℓ] + (S : Fin s → Set F) (P : ℓ → MvPolynomial (Fin s) F) (d : Fin s → ℕ) + (hdeg : ∀ (j : ℓ) (i : Fin s), (P j).degreeOf i ≤ d i) + (G : Generator (∀ i, ↥(S i)) ℓ F) + (hG : ∀ x, G x = MvPolynomial.eval (fun i => (↑(x i) : F)) ∘ P) : + generatorByRightMul (tensorGeneratorPiUnivariateOn S d) (coeffMatrix P d) = G := by + funext x + set xc : Fin s → F := fun i => (↑(x i) : F) with hxc + have hsub : tensorGeneratorPiUnivariateOn S d x = tensorGeneratorPiUnivariate d xc := by + funext e; simp [tensorGeneratorPiUnivariateOn, tensorGeneratorPiUnivariate, hxc] + have hgbm := generatorByRightMul_coeffMatrix P d hdeg + (fun y => MvPolynomial.eval y ∘ P) (fun _ => rfl) + calc generatorByRightMul (tensorGeneratorPiUnivariateOn S d) (coeffMatrix P d) x + = Matrix.vecMul (tensorGeneratorPiUnivariateOn S d x) (coeffMatrix P d) := rfl + _ = Matrix.vecMul (tensorGeneratorPiUnivariate d xc) (coeffMatrix P d) := by rw [hsub] + _ = generatorByRightMul (tensorGeneratorPiUnivariate d) (coeffMatrix P d) xc := rfl + _ = (MvPolynomial.eval xc ∘ P) := congrFun hgbm _ + _ = G x := (hG x).symm + +/-- Theorem 8.2 (MCA for polynomial generators) [BCGM25]. -/ +theorem polynomial_gen_MCA {ι : Type} [Fintype ι] [Nonempty ι] [DecidableEq F] + {ℓ : Type} [Fintype ℓ] (LC : LinearCode ι F) + (η : ℝ) (hη : 0 < η ∧ η < 1) + {s : ℕ} (S : Fin s → Set F) [∀ i, Fintype (S i)] [∀ i, Nonempty (S i)] + (G : Generator (∀ i, S i) ℓ F) + (P : ℓ → MvPolynomial (Fin s) F) (hG : IsPolynomialGeneratorOf S G P) + (hS : ∀ i : Fin s, (deg_max P i + 1) ≤ (Set.ncard (S i))) : + letI ε : I → ℝ := ∑ i : Fin s, (ξ LC (deg_max P i) (Set.ncard (S i)) η) + IsMCAGenerator G ε LC := by + classical + show IsMCAGenerator G (∑ i : Fin s, ξ LC (deg_max P i) (Set.ncard (S i)) η) LC + have hcard : ∀ i : Fin s, Set.ncard (S i) = Fintype.card (S i) := by + intro i + rw [Set.ncard_eq_toFinset_card', Set.toFinset_card] + have hdeg : ∀ (j : ℓ) (i : Fin s), (P j).degreeOf i ≤ deg_max P i := by + intro j i + simpa [deg_max] using + Finset.le_sup (f := fun j => (P j).degreeOf i) (Fintype.complete j) + have hcard_deg : ∀ i : Fin s, deg_max P i + 1 ≤ Fintype.card (S i) := by + intro i + rw [← hcard i] + exact hS i + have htensor := tensorGeneratorPiUnivariateOn_isMCAGenerator LC η hη S (deg_max P) hcard_deg + have hmul := pseudoinverseGen (tensorGeneratorPiUnivariateOn S (deg_max P)) + (fun γ => ∑ i, ξ LC (deg_max P i) (Fintype.card ↥(S i)) η γ) LC htensor + (coeffMatrix P (deg_max P)) + (coeffMatrix_hasLeftPseudoInverse P (deg_max P) hdeg hG.1) + rw [generatorByRightMul_coeffMatrix_sub S P (deg_max P) hdeg G hG.2] at hmul + have herr : (∑ i : Fin s, ξ LC (deg_max P i) (Set.ncard (S i)) η) + = (fun γ => ∑ i, ξ LC (deg_max P i) (Fintype.card ↥(S i)) η γ) := by + funext γ + rw [Finset.sum_apply] + exact Finset.sum_congr rfl (fun i _ => by rw [hcard i]) + rwa [herr] + +end PolynomialGenIsMCA diff --git a/ArkLib/Data/Probability/Instances.lean b/ArkLib/Data/Probability/Instances.lean index 3f5ca96fd4..10537fd87a 100644 --- a/ArkLib/Data/Probability/Instances.lean +++ b/ArkLib/Data/Probability/Instances.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Quang Dao, Chung Thai Nguyen +Authors: Quang Dao, Chung Thai Nguyen, Katerina Hristova -/ import Mathlib.Probability.ProbabilityMassFunction.Monad @@ -9,13 +9,13 @@ import ArkLib.Data.Probability.Notation import CompPoly.Data.Fin.BigOperators import CompPoly.Data.Nat.Bitwise import Mathlib.Algebra.MvPolynomial.SchwartzZippel + /-! # Probability Instances -/ -open ProbabilityTheory Filter -open NNReal Finset Function +open ProbabilityTheory Filter NNReal Finset Function Real open scoped BigOperators ProbabilityTheory -open Real + -- TODO(dtumad): Move most of the stuff in this file to VCV and generalize as possible @@ -41,6 +41,7 @@ instance [IsEmpty α] : IsEmpty (PMF α) := by end section ProbabilityTools + /-- Unrolls `Pr_{ let x ← D }[P x]` into a sum of the form `∑' x, Pr[x] * (if P x then 1 else 0)`. -/ theorem prob_tsum_form_singleton {α : Type} (D : PMF α) (P : α → Prop) [DecidablePred P] : @@ -221,6 +222,22 @@ theorem do_two_uniform_sampling_eq_uniform_prod {α β : Type} [Fintype α] [Fin simp only [ite_eq_right_iff, one_ne_zero, imp_false] exact id (Ne.symm h_ne) +section + +/-- The probability that a property `P` holds for a uniformly random `r : F` equals +`ENNReal.ofReal` of the real-valued density `|{x : F // P x}| / |F|`. This is the +`ENNReal.ofReal`-of-a-real-number form of `prob_uniform_eq_card_filter_div_card`, useful when the +surrounding goal is stated over `ℝ` rather than `ℝ≥0`. -/ +theorem prob_uniform_eq_ofReal {F : Type} [Fintype F] [Nonempty F] + (P : F → Prop) [DecidablePred P] : + Pr_{let r ←$ᵖ F}[P r] = ENNReal.ofReal + (((Finset.filter (α := F) P Finset.univ).card : ℝ) / (Fintype.card F : ℝ)) := by + convert prob_uniform_eq_card_filter_div_card P using 1 + rw [ENNReal.ofReal_div_of_pos] <;> norm_num + exact Fintype.card_pos + +end + /-- **Generic Probability Splitting Lemma (via Equivalence)** @@ -451,6 +468,81 @@ lemma Pr_congr {α : Type} {D : PMF α} {P Q : α → Prop} congr 2; funext x; congr 1; exact propext (h x) +/-- +**Union Bound (binary form)** + +The probability of a disjunction of two events is at most the sum of their individual +probabilities. +-/ +theorem Pr_or_le {α : Type} (D : PMF α) (f g : α → Prop) : + Pr_{ let r ← D }[ f r ∨ g r ] ≤ Pr_{ let r ← D }[ f r ] + Pr_{ let r ← D }[ g r ] := by + classical + rw [prob_tsum_form_singleton, prob_tsum_form_singleton, prob_tsum_form_singleton, + ← ENNReal.tsum_add] + apply ENNReal.tsum_le_tsum + intro r + rw [← mul_add] + refine mul_le_mul_of_nonneg_left ?_ zero_le' + by_cases hf : f r <;> by_cases hg : g r <;> simp [hf, hg] + +/-- +**Union Bound (over a finite index set)** + +The probability that `∃ i, f i r` holds is at most the sum, over `i`, of the probabilities that +`f i r` holds. +-/ +theorem Pr_exists_le {α ι : Type} [Fintype ι] (D : PMF α) (f : ι → α → Prop) : + Pr_{ let r ← D }[ ∃ i, f i r ] ≤ ∑ i, Pr_{ let r ← D }[ f i r ] := by + classical + have key : ∀ (s : Finset ι), + Pr_{ let r ← D }[ ∃ i ∈ s, f i r ] ≤ ∑ i ∈ s, Pr_{ let r ← D }[ f i r ] := by + intro s + induction s using Finset.induction with + | empty => + have h0 : Pr_{ let r ← D }[ ∃ i ∈ (∅ : Finset ι), f i r ] + = Pr_{ let r ← D }[ (False : Prop) ] := + Pr_congr (fun r => by simp) + rw [Finset.sum_empty, h0, prob_tsum_form_singleton] + simp + | insert a s ha ih => + have hcongr : Pr_{ let r ← D }[ ∃ i ∈ insert a s, f i r ] = + Pr_{ let r ← D }[ f a r ∨ ∃ i ∈ s, f i r ] := + Pr_congr (fun r => by + constructor + · rintro ⟨i, hi, hfi⟩ + rcases Finset.mem_insert.mp hi with rfl | hi + · exact Or.inl hfi + · exact Or.inr ⟨i, hi, hfi⟩ + · rintro (hfa | ⟨i, hi, hfi⟩) + · exact ⟨a, Finset.mem_insert_self a s, hfa⟩ + · exact ⟨i, Finset.mem_insert_of_mem hi, hfi⟩) + rw [hcongr] + calc Pr_{ let r ← D }[ f a r ∨ ∃ i ∈ s, f i r ] + ≤ Pr_{ let r ← D }[ f a r ] + Pr_{ let r ← D }[ ∃ i ∈ s, f i r ] := Pr_or_le D _ _ + _ ≤ Pr_{ let r ← D }[ f a r ] + ∑ i ∈ s, Pr_{ let r ← D }[ f i r ] := by gcongr + _ = ∑ i ∈ insert a s, Pr_{ let r ← D }[ f i r ] := by rw [Finset.sum_insert ha] + simpa using key Finset.univ + +/-- +**Marginal Bound for Sequential Sampling** + +If, for every fixed outcome `b` of the second sample, the probability over the first sample is +bounded by a constant `c` (not depending on `b`), then the same bound holds for the probability +over the full sequential sample. +-/ +theorem Pr_seq_le_of_forall_le {α β : Type} (Da : PMF α) (Db : PMF β) (Q : α → β → Prop) + {c : ENNReal} (h : ∀ b, Pr_{ let a ← Da}[Q a b] ≤ c) : + Pr_{ let b ← Db; let a ← Da }[ Q a b ] ≤ c := by + classical + let D_rest : β → PMF Prop := fun b => (do let a ← Da; return (Q a b)) + calc Pr_{ let b ← Db; let a ← Da }[ Q a b ] + = ∑' b, Db b * (D_rest b) True := prob_tsum_form_split_first Db D_rest + _ ≤ ∑' b, Db b * c := by + apply ENNReal.tsum_le_tsum + intro b + exact mul_le_mul_of_nonneg_left (h b) zero_le' + _ = c := by rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + /-- **Schwartz-Zippel Lemma** (Probability Form): For a non-zero multivariate polynomial `P` of total degree at most `d` over a finite field `L`, the probability that `P(r)` evaluates to 0 for a uniformly random `r` is at most `d / |L|`. -/ diff --git a/docs/kb/concepts/reed-solomon-proximity.md b/docs/kb/concepts/reed-solomon-proximity.md index 6fef153a1b..5048dc60ee 100644 --- a/docs/kb/concepts/reed-solomon-proximity.md +++ b/docs/kb/concepts/reed-solomon-proximity.md @@ -20,8 +20,8 @@ coding-theory machinery as formalized in ArkLib. - [`../../../ArkLib/Data/CodingTheory/ProximityGap/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/Basic.lean) - [`../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20`](../../../ArkLib/Data/CodingTheory/ProximityGap/BCIKS20) - [`../../../ArkLib/Data/CodingTheory/ProximityGap/DG25`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25) -- [`../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean) -- [`../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean) +- [`../../../ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean) +- [`../../../ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean) - [`../../../ArkLib/Data/CodingTheory/ReedSolomon.lean`](../../../ArkLib/Data/CodingTheory/ReedSolomon.lean) - [`../../../ArkLib/ProofSystem/Stir/ProximityGap.lean`](../../../ArkLib/ProofSystem/Stir/ProximityGap.lean) diff --git a/docs/kb/papers/BCGM25.md b/docs/kb/papers/BCGM25.md index bf3231a2e8..8f1ba21cbb 100644 --- a/docs/kb/papers/BCGM25.md +++ b/docs/kb/papers/BCGM25.md @@ -10,8 +10,8 @@ status: seeded related_concepts: - reed-solomon-proximity related_modules: - - ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean - - ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean + - ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean + - ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean --- # BCGM25 @@ -26,16 +26,17 @@ with Reed-Solomon refinements up to the Johnson bound. ## What ArkLib Uses From This Paper - Generator definitions and zero-evading/MDS/polynomial-generator interfaces in - [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean). + [`ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean). - MCA generator definitions and linear-transformation closure statements in - [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean). + [`ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean). - The broader formalization target that polynomial-generator MCA bounds should become reusable coding-theory infrastructure rather than WHIR-only assumptions. ## Main ArkLib Touchpoints -- [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean) -- [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean) +- [`ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean) +- [`ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean) +- [`ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean`](../../../ArkLib/ProofSystem/Whir/MutualCorrAgreement.lean) ## Version Notes diff --git a/docs/kb/papers/Jo26.md b/docs/kb/papers/Jo26.md index 62bd7086db..090a3cc8d1 100644 --- a/docs/kb/papers/Jo26.md +++ b/docs/kb/papers/Jo26.md @@ -11,8 +11,8 @@ related_concepts: - reed-solomon-proximity related_modules: - ArkLib/Data/CodingTheory/InterleavedCode.lean - - ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean - - ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean + - ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean + - ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean - ArkLib/Data/CodingTheory/ProximityGap/DG25 --- @@ -40,9 +40,9 @@ linear interleaving-width loss for generator MCA. - [`ArkLib/Data/CodingTheory/InterleavedCode.lean`](../../../ArkLib/Data/CodingTheory/InterleavedCode.lean) provides row-wise/interleaved-code representations. -- [`ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/ProximityGenerators.lean) +- [`ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/Basic.lean) and - [`ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGap/MCAGenerator.lean) + [`ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean`](../../../ArkLib/Data/CodingTheory/ProximityGenerator/MCAGenerator.lean) provide the general generator and MCA-generator layer. - [`ArkLib/Data/CodingTheory/ProximityGap/DG25`](../../../ArkLib/Data/CodingTheory/ProximityGap/DG25) contains adjacent interleaved-code proximity-gap transfer results.