Binary.lean

1 import ProofPath.Protected
2 import Mathlib.Data.ZMod.Basic
3 import Mathlib.LinearAlgebra.Matrix.ToLin
4 
5 namespace ProofPath
6 open Matrix
7 
8 variable {K : Type*} [Field K] {m n : ℕ}
9 
10 def dualRow (l : (Fin m → K) →ₗ[K] K) (i : Fin m) : K :=
11   l (Pi.single i 1)
12 
13 theorem dual_row_eval (l : (Fin m → K) →ₗ[K] K) (y : Fin m → K) :
14     dotProduct (dualRow l) y = l y := by
15   have h : (∑ i : Fin m, y i • Pi.single i (1 : K)) = y := by
16     ext j
17     simp [Finset.sum_apply, Pi.single_apply, Pi.smul_apply]
18   calc
19     dotProduct (dualRow l) y = l (∑ i : Fin m, y i • Pi.single i (1 : K)) := by
20       simp [dotProduct, dualRow, map_sum, map_smul, smul_eq_mul, mul_comm]
21     _ = l y := congrArg l h
22 
23 theorem row_witness_sound (M : Matrix (Fin m) (Fin n) K)
24     (b l : Fin m → K) (hz : vecMul l M = 0) (h1 : dotProduct l b = 1) :
25     ¬ ∃ y, M.mulVec y = b := by
26   rintro ⟨y, hy⟩
27   have h := dotProduct_mulVec l M y
28   rw [hy, hz, zero_dotProduct, h1] at h
29   exact one_ne_zero h
30 
31 theorem row_alternative (M : Matrix (Fin m) (Fin n) K) (b : Fin m → K) :
32     (¬ ∃ y, M.mulVec y = b) ↔
33       ∃ l, vecMul l M = 0 ∧ dotProduct l b = 1 := by
34   constructor
35   · intro hn
36     have hb : b ∉ M.mulVecLin.range := by
37       rintro ⟨y, hy⟩
38       exact hn ⟨y, hy⟩
39     obtain ⟨l, hl, hz⟩ := Submodule.exists_dual_map_eq_bot_of_notMem hb inferInstance
40     let f := (l b)⁻¹ • l
41     have hf : f b = 1 := by simp [f, hl]
42     have hzero : ∀ y, f (M.mulVec y) = 0 := by
43       intro y
44       have hm : l (M.mulVec y) ∈ M.mulVecLin.range.map l :=
45         ⟨M.mulVec y, ⟨y, rfl⟩, rfl⟩
46       have h : l (M.mulVec y) = 0 := by simpa [hz] using hm
47       simp [f, h]
48     refine ⟨dualRow f, ?_, by rw [dual_row_eval]; exact hf⟩
49     ext j
50     have h := hzero (Pi.single j 1)
51     rw [← dual_row_eval f, dotProduct_mulVec] at h
52     simpa [dotProduct, Pi.single_apply, mul_ite] using h
53   · rintro ⟨l, hz, h1⟩
54     exact row_witness_sound M b l hz h1
55 
56 theorem binary_fiber_card {R : Type*} [AddCommGroup R] [Module (ZMod 2) R]
57     (T : (Fin n → ZMod 2) →ₗ[ZMod 2] R) (x₀ : Fin n → ZMod 2) :
58     Nat.card {y // T y = T x₀} = 2 ^ Module.finrank (ZMod 2) T.ker := by
59   simpa using fiber_card T x₀
60 
61 end ProofPath

Back to source controls