...

Author: Ferinko

.github/workflows/lean_action_ci.yml

@@ -0,0 +1,14 @@
+name: Lean Action CI
+
+on:
+  push:
+  pull_request:
+  workflow_dispatch:
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1

.gitignore

@@ -0,0 +1 @@
+/.lake

Main.lean

@@ -0,0 +1,272 @@
+import Mathlib
+import Auto
+import Smt
+
+import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Real.Sqrt
+import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
+import Mathlib.Data.Finset.BooleanAlgebra
+import Mathlib
+
+/-!
+  # Definitions and Theorems about Proximity Gaps
+
+  We define the proximity gap properties of linear codes over finite fields.
+
+  ## Main Definitions
+
+-/
+
+open NNReal Finset Function
+
+open scoped BigOperators
+
+variable {n : Type*} [Fintype n] [DecidableEq n]
+
+variable {F : Type*} [Field F] [Fintype F] [DecidableEq F]
+
+variable (C : Submodule F (n → F)) [DecidablePred (· ∈ C)]
+
+/-- The proximity measure of two vectors `u` and `v` from a code `C` at distance `d` is the number
+  of vectors at distance at most `d` from the linear combination of `u` and `v` with coefficients
+  `r` in `F`. -/
+def proximityMeasure (u v : n → F) (d : ℕ) : ℕ :=
+  Fintype.card {r : F | Δ₀'(r • u + (1 - r) • v, C) ≤ d}
+
+/-- A code `C` exhibits proximity gap at distance `d` and cardinality bound `bound` if for every
+      pair of vectors `u` and `v`, whenever the proximity measure for `C u v d` is greater than
+      `bound`, then the distance of `[u | v]` from the interleaved code `C ^⊗ 2` is at most `d`. -/
+def proximityGap (d : ℕ) (bound : ℕ) : Prop :=
+  ∀ u v : n → F, (proximityMeasure C u v d > bound)
+    → (Δ₀( u ⋈ v , C ^⋈ Fin 2 ) ≤ d)
+
+/-- A code `C` exhibits `δ`-correlated agreement with respect to a tuple of vectors `W_1, ..., W_k`
+  if there exists a set `S` of coordinates such that the size of `S` is at least `(1 - δ) * |n|`,
+  and there exists a tuple of codewords `v_1, ..., v_k` such that `v_i` agrees with `W_i` on `S`
+  for all `i`. -/
+def correlatedAgreement (C : Set (n → F)) (δ : ℝ≥0) {k : ℕ} (W : Fin k → n → F) : Prop :=
+  ∃ S : Finset n, #(S) ≥ (1 - δ) * (Fintype.card n) ∧
+    ∃ v : Fin k → n → F, ∀ i, v i ∈ C ∧ {j | v i j = W i j} ⊆ S
+
+
+section
+
+variable {α : Type*}[DecidableEq α] [Nonempty α]
+         {ι : Type*} [DecidableEq ι] [Nonempty ι]
+
+
+/--
+Distance from a point to a set of points.
+-/
+noncomputable def distToSet (Δ : (ι → α) → (ι → α) → ℝ≥0) (x : ι → α) (P : Set (ι → α)) : ℝ≥0 :=
+  sInf {d | ∃ y ∈ P, Δ x y = d}
+
+
+/--
+Definition 1.1 in Proximity Gaps paper.
+KATY TO DO: maybe `δ : ℝ≥0` to reflect the rel distances?
+Here, `S` can be empty. Maybe add a condition for every S non-empty, then blah
+-/
+noncomputable def generalProximityGap (P : Finset (ι → α)) (C : Finset (Finset (ι → α)))
+ (Δ : (ι → α) → (ι → α) → ℕ) (δ ε : ℝ≥0) (S : Finset (ι → α)) (h' : S ∈ C) (h : S.Nonempty)
+  : Prop :=
+  (PMF.uniformOfFinset S h).toOuterMeasure {x | distToSet Δ x P ≤ δ} = 1
+  ∨ (PMF.uniformOfFinset S h).toOuterMeasure {x | distToSet Δ x P ≤ δ} ≤ ε
+
+
+-- noncomputable def setOfSubmodules [Field F] : Set (Submodule F (ι → F)) :=
+--{A | ∃ B : Submodule F (ι → F), A = B}
+-- Set.univ
+
+
+lemma setOfSubmodules_nonempty :
+  {A | ∃ B : Submodule F (ι → F), A = B}.Nonempty := by simp only [exists_eq', Set.setOf_true,
+    Set.univ_nonempty]
+
+lemma setOfSubmodules_finite [Fintype F] [Fintype ι] :
+  {A | ∃ B : Submodule F (ι → F), A = B}.Finite := by
+  simp only [exists_eq', Set.setOf_true]
+  exact Set.finite_univ
+
+-- Fintype.ofFinite
+
+#print AffineSubspace
+
+-- noncomputable def setOfAffineSubspaces [Field F] : Set (AffineSubspace F (ι → F)) :=
+-- {A | ∃ B : AffineSubspace F (ι → F), A = B}
+
+
+lemma setOfAffineSubspaces_nonempty :
+  {A | ∃ B : AffineSubspace F (ι → F), A = B}.Nonempty := by simp only [exists_eq', Set.setOf_true,
+    Set.univ_nonempty]
+
+lemma setOfAffineSubspaces_finite [Fintype F] [Fintype ι] :
+  {A | ∃ B : AffineSubspace F (ι → F), A = B}.Finite := by
+  simp only [exists_eq', Set.setOf_true]
+  exact Set.finite_univ
+
+noncomputable def proximityParams [Fintype F] [Fintype ι] (δ : ℝ≥0) (deg : ℕ)
+  (domain : ι ↪ F) : ℝ≥0 :=
+  if UD : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain)/2 then Fintype.card ι / Fintype.card F
+  else if JB : δ ≥ 1 - (ReedSolomonCode.sqrtRate deg domain)/2 ∧ δ ≤ 1 -
+  (ReedSolomonCode.sqrtRate deg domain)
+    then
+    let m := min (1 - (ReedSolomonCode.sqrtRate deg domain) - δ)
+                (ReedSolomonCode.sqrtRate deg domain/ 20)
+    ⟨(deg ^ 2 : ℝ≥0) / ((2 * m) ^ 7 * (Fintype.card F : ℝ)), by positivity⟩
+    else 0
+
+-- /--
+-- Theorem 1.2 (Proximity gap for RS codes)
+-- -/
+-- theorem proximityGapsRSCode [Fintype ι] [Nonempty ι] [Field F] [Fintype F]
+
+/--
+Theorem 1.4 (Main Theorem — Correlated agreement over lines) in Proximity Gaps
+-/
+theorem correlatedAgreement_lines [Fintype ι] [Nonempty ι] [Field F] [Fintype F]
+(u : Fin 2 → ι → F) (δ : ℝ≥0) (deg : ℕ) (domain : ι ↪ F)
+(hδ : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
+(hproximity : (PMF.uniformOfFintype F).toOuterMeasure
+    {z | Code.relHammingDistToCode (u 1 + z • u 2) (ReedSolomon.code domain deg) ≤ δ}
+      > proximityParams δ deg domain) :
+  correlatedAgreement (ReedSolomon.code domain deg) δ u := by sorry
+
+/--
+Let `u := {u_1, ..., u_l}` be a collection of vectors in `F^ι`. The parameterised curve of degree
+`l` generated by `u` is the set of linear combinations of the form `{∑ i ∈ l r ^ i • u_i | r ∈ F}`.
+-/
+def parametrisedCurve {l : ℕ} (u : Fin l → ι → F) : Set (ι → F) :=
+  {v | ∃ r : F, v = ∑ i : Fin l, (r ^ (i : ℕ)) • u i}
+
+/--
+A parametrised curve over a finite field.
+-/
+def parametrisedCurve' [Fintype ι] [Field F] [Fintype F] {l : ℕ} (u : Fin l → ι → F) :
+Finset (ι → F) := {v | ∃ r : F, v = ∑ i : Fin l, (r ^ (i : ℕ)) • u i}
+
+
+instance [Fintype ι] [Field F] [Fintype F] [Nonempty F] {l : ℕ} :
+  ∀ u : Fin l → ι → F, Nonempty {x // x ∈ parametrisedCurve' u } := by
+  intro u
+  unfold parametrisedCurve'
+  simp only [mem_filter, mem_univ, true_and, nonempty_subtype]
+  obtain ⟨r⟩ := ‹Nonempty F›
+  use ∑ i : Fin l, r ^ (i : ℕ) • u i, r
+
+
+/--
+Theorem 1.5 (Correlated agreement for low-degree parameterised curves) in Proximity Gaps
+-/
+theorem correlatedAgreement_affine_curves [Fintype ι] [Nonempty ι] [Field F] [Fintype F]
+[DecidableEq F]
+{l : ℕ} (u : Fin l → ι → F) (δ : ℝ≥0) (deg : ℕ) (domain : ι ↪ F)
+(hδ : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
+(hproximity : (PMF.uniformOfFintype (parametrisedCurve' u)).toOuterMeasure
+    {y | Code.relHammingDistToCode y.1 (ReedSolomon.code domain deg) ≤ δ}
+    > l*(proximityParams δ deg domain)):
+  correlatedAgreement (ReedSolomon.code domain deg) δ u := by sorry
+
+#check Set.range
+#check affineSpan
+/--
+Theorem 1.6 (Correlated agreement over affine spaces) in Proximity Gaps
+--- how do I represent `u` as a set?
+-/
+theorem correlatedAgreement_affine_spaces [Fintype ι] [Nonempty ι] [Field F] [Fintype F]
+{l : ℕ} (u : Fin (l+1) → ι → F) (δ : ℝ≥0) (deg : ℕ) (domain : ι ↪ F)
+(hδ : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
+(hproximity : (PMF.uniformOfFintype (affineSpan F (Set.range u))).toOuterMeasure
+    {y | Code.relHammingDistToCode y (ReedSolomon.code domain deg) ≤ δ}
+    > proximityParams δ deg domain) :
+  correlatedAgreement (ReedSolomon.code domain deg) δ u := by sorry
+
+instance {l : ℕ} [NeZero l] : Nonempty (Fin l) := inferInstance
+
+instance {l : ℕ} [NeZero l] : Fintype (Fin l) := inferInstance
+
+-- instance {l : ℕ} [NeZero l] :
+--   Inhabited (Finset.univ : Finset (Fin l)) := inferInstance
+
+#check Fintype.ofFinite
+
+instance {α : Type} [Fintype α] [Nonempty α] :
+  Nonempty (Finset.univ : Finset α) := by exact Nonempty.to_subtype (univ_nonempty_iff.mpr (by assumption))
+  -- refine Nonempty.to_subtype ?_
+
+
+  -- rw [← Finset.univ_nonempty_iff]
+  -- apply Finset.univ_nonempty
+
+
+  -- haveI := @Finset.univ_nonempty (Fin (l+1)) _ _
+  -- exact this
+
+
+
+  -- apply Nonempty.intro
+  -- exact ⟨0 , by simp⟩
+
+
+
+theorem correlatedAgreement_affine_spaces' [Fintype ι] [Field F] [Fintype F]
+[DecidableEq F]
+{l : ℕ} [NeZero l] (u : Fin l → ι → F) (δ : ℝ≥0) (deg : ℕ) (domain : ι ↪ F)
+-- (hδ : δ ≤ 1 - (ReedSolomonCode.sqrtRate deg domain))
+  (hproximity : (@PMF.uniformOfFintype (@affineSpan F F
+                                          (ι → F) _ _ _ {vsub := sorry, vsub_vadd' := sorry, vadd_vsub' := sorry}
+                                          (Finset.univ.image u))
+                                          (let x : AffineSubspace F (ι → F) := affineSpan F ↑(image u univ)
+                                           let y : Set _ := SetLike.coe x
+                                           by 
+                                           {elems := by have : y = ↑x := by aesop
+                                                        simp [x] at this
+                                                        have : Finite y := by
+                                                          rw [this]
+                                                          exact Subtype.finite
+                                                        simp [y, x] at this
+                                                        have := Fintype.ofFinite ↑(spanPoints F (Set.range u))
+                                                        simp
+                                                        simp_rw [←coe_affineSpan] at this
+                                                        rcases this with ⟨s, hs⟩
+                                                        convert s
+                                                        ext x
+                                                        refine ⟨λ h ↦ ?p₁, λ h ↦ ?p₂⟩
+                                                        sorry
+                                                        
+                                                        
+                                                        done, complete := sorry}) sorry).toOuterMeasure
+      sorry
+      > 42.) : False := by
+  sorry
+  -- correlatedAgreement (ReedSolomon.code domain deg) δ u := by sorry
+
+
+--- { y : affineSpan F (Finset.univ.image u) |
+-- Code.relHammingDistToCode y.1 (ReedSolomon.code domain deg) ≤ δ}
+
+end
+
+-- import Scratch.Basic
+
+-- example {α : Type} {s : Finset α} : Fintype {x | x ∈ s} :=
+--   Set.fintypeMemFinset s
+
+
+
+-- -- set_option trace.auto.smt.printCommands true
+
+-- -- set_option auto.smt true
+
+-- -- -- example {n : ℤ} : n + 1 - 1 = n := by
+-- -- --   -- smt_show
+-- -- --   autoGetHints
+
+-- -- example {x₁ x₂ α₁ : ℤ} (h₁ : 0 ≤ α₁) (h₂ : 0 ≤ 1 - α₁) (h₃ : α₁ + (1 - α₁) = 1) :
+-- --   0 ≤ α₁ * (1 - α₁) * (x₁ - x₂) ^ 2 := by
+-- --   autoGetHints
+
+
+
+-- def main : IO Unit := pure ()

README.md

@@ -0,0 +1 @@
+# scratch

Scratch.lean

@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Scratch` library.
+-- Import modules here that should be built as part of the library.
+import Scratch.Basic

Scratch/Basic.lean

@@ -0,0 +1,5 @@
+namespace X
+
+private def F : Nat := 42
+
+end X