Coding-Theory Preliminaries

def multilinearWeight {F : Type u_1} [CommRing F] {ϑ : ℕ} (r : Fin ϑ → F) (i : Fin (2 ^ ϑ)) : F

The tensor product weight ⊗_{i=0}^{ϑ-1}(1 - rᵢ, rᵢ) for a specific index i given randomness r. Corresponds to eq(i, r) in multilinear polynomial literature.

def multilinearCombine {F : Type u_1} [CommRing F] {A : Type u_2} [AddCommMonoid A] [Module F A] {ϑ : ℕ} {ι : Type u_3} (u : Fin (2 ^ ϑ) → ι → A) (r : Fin ϑ → F) : ι → A

Linear combination of the rows of u according to the tensor product of r: [tensor_product r i] ·|u₀| |u₁| |⋮| |u_{2^ϑ-1}| = ∑_{i=0}^{2^ϑ-1} (multilinearWeight r i) • u_i

def «term_|⨂|_» : Lean.TrailingParserDescr

def Matrix.neqCols {F : Type u_1} {ι : Type u_2} [Fintype ι] {ι' : Type u_3} [Fintype ι'] [DecidableEq F] (U V : Matrix ι ι' F) : Finset ι'

The set of column indices where two matrices differ.

def Matrix.rowSpan {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Semiring F] (U : Matrix ι ι' F) : Submodule F (ι' → F)

The submodule spanned by the rows of a matrix.

noncomputable def Matrix.rowRank {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Semiring F] (U : Matrix ι ι' F) : ℕ

The row rank of a matrix (dimension of the row span).

def Matrix.colSpan {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Semiring F] (U : Matrix ι ι' F) : Submodule F (ι → F)

The submodule spanned by the columns of a matrix.

noncomputable def Matrix.colRank {F : Type u_1} {ι : Type u_2} {ι' : Type u_3} [Semiring F] (U : Matrix ι ι' F) : ℕ

The column rank of a matrix (dimension of the column span).

def Matrix.subUpFull {F : Type u_1} {m n : ℕ} (U : Matrix (Fin m) (Fin n) F) (r_reindex : Fin n → Fin m) : Matrix (Fin n) (Fin n) F

Extract an n×n submatrix from an m×n matrix by selecting n rows.

def Matrix.subLeftFull {F : Type u_1} {m n : ℕ} (U : Matrix (Fin m) (Fin n) F) (c_reindex : Fin m → Fin n) : Matrix (Fin m) (Fin m) F

Extract an m×m submatrix from an m×n matrix by selecting m columns.

theorem Matrix.rank_eq_if_subUpFull_eq {F : Type u_1} {m n : ℕ} [CommRing F] [Nontrivial F] {U : Matrix (Fin m) (Fin n) F} (h : n ≤ m) : (U.subUpFull (Fin.castLE h)).rank = n → U.rank = n

An m×n matrix has full rank if the submatrix consisting of rows 1 through n has rank n.

theorem Matrix.cRank_rank_conversion {F : Type u_1} {m n : ℕ} [CommRing F] [Nontrivial F] {U : Matrix (Fin m) (Fin n) F} : ↑U.rank = U.cRank

cRank and Rank agree for a finite matirx

theorem Matrix.full_row_rank_via_rank_subLeftFull {F : Type u_1} {m n : ℕ} [CommRing F] [Nontrivial F] {U : Matrix (Fin m) (Fin n) F} (h : m ≤ n) : (U.subLeftFull (Fin.castLE h)).rank = m → U.rank = m

An m×n matrix has full rank if the submatrix consisting of columns 1 through m has rank m.

theorem Matrix.rank_eq_if_det_ne_zero {F : Type u_1} {n : ℕ} [CommRing F] [Nontrivial F] {U : Matrix (Fin n) (Fin n) F} [IsDomain F] : U.det ≠ 0 → U.rank = n

A square matrix over an integral domain has full rank if its determinant is nonzero.

theorem Matrix.rank_eq_iff_det_ne_zero {F : Type u_1} {n : ℕ} [Field F] {U : Matrix (Fin n) (Fin n) F} : U.rank = n ↔ U.det ≠ 0

A square matrix has full rank iff the determinant is nonzero.

theorem Matrix.rank_eq_colRank {F : Type u_1} {m n : ℕ} [Field F] {U : Matrix (Fin m) (Fin n) F} : U.rank = U.colRank

The rank of a matrix equals the column rank.

theorem Matrix.rowRank_eq_colRank {F : Type u_1} {m n : ℕ} [Field F] {U : Matrix (Fin m) (Fin n) F} : U.rowRank = U.colRank

The row rank of a matrix equals the column rank.

theorem Matrix.rank_eq_rowRank {F : Type u_1} {m n : ℕ} [Field F] {U : Matrix (Fin m) (Fin n) F} : U.rank = U.rowRank

The rank of a matrix equals the row rank.

theorem Matrix.rank_eq_min_row_col_rank {F : Type u_1} {m n : ℕ} [Field F] {U : Matrix (Fin m) (Fin n) F} : U.rank = min U.rowRank U.colRank

The rank of a matrix equals the minimum of its row rank and column rank.

@[reducible]

def Affine.affineLineAtOrigin {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Ring F] [AddCommGroup A] [Module F A] (origin direction : ι → A) : AffineSubspace F (ι → A)

Affine line at origin u: {u + α • v : α ∈ F}, the line through u with direction v. This definition is used in Theorems 1.4, 4.1, 5.1, [BCIKS20] and Lemma 4.4, [AHIV22].

theorem Affine.mem_affineLineAtOrigin_iff {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Ring F] [AddCommGroup A] [Module F A] (origin direction x : ι → A) : x ∈ affineLineAtOrigin origin direction ↔ ∃ (α : F), x = origin + α • direction

@[reducible]

def Affine.affineSubspaceAtOrigin {ι : Type u_1} [Fintype ι] {F : Type u_2} {A : Type u_3} {k : ℕ} [Ring F] [AddCommGroup A] [DecidableEq A] [Module F A] (origin : ι → A) (directions : Fin k → ι → A) : AffineSubspace F (ι → A)

Affine subspace from base origin and direction generators. Constructs the affine subspace {origin + span{directions}}. Used in Theorem 1.6, [BCIKS20].

theorem Affine.mem_affineSubspaceFrom_iff {ι : Type u_1} [Fintype ι] {F : Type u_2} {A : Type u_3} {k : ℕ} [Ring F] [AddCommGroup A] [DecidableEq A] [Module F A] (origin : ι → A) (directions : Fin k → ι → A) (x : ι → A) : x ∈ affineSubspaceAtOrigin origin directions ↔ ∃ (β : Fin k → F), x = origin + ∑ i : Fin k, β i • directions i

@[implicit_reducible]

instance Affine.instVAddForallAffineSubspace_starlib {ι : Type u_1} {F : Type u_2} [Ring F] : VAdd (ι → F) (AffineSubspace F (ι → F))

Vector addition action on affine subspaces.

@[implicit_reducible]

noncomputable instance Affine.instFintypeSubtypeForallMemAffineSubspaceHVAdd_starlib {ι : Type u_1} [Fintype ι] {F : Type u_2} [Ring F] [Fintype F] {v : ι → F} {s : AffineSubspace F (ι → F)} [Fintype ↥s] : Fintype ↥(v +ᵥ s)

A translate of a finite affine subspace is finite.

@[implicit_reducible]

noncomputable instance Affine.instFintypeSubtypeForallMemAffineSubspaceAffineSpan_starlib {ι : Type u_1} [Fintype ι] {F : Type u_2} [Ring F] [Fintype F] {s : Set (ι → F)} : Fintype ↥(affineSpan F s)

The affine span of a set is finite over a finite field.

instance Affine.instNonemptySubtypeForallMemFinsetImageFinUniv_starlib {ι : Type u_1} [Fintype ι] {F : Type u_2} {k : ℕ} [DecidableEq F] [NeZero k] {f : Fin k → ι → F} : Nonempty ↥(Finset.image f Finset.univ)

The image of a function Fin k → α over Finset.univ is nonempty when k ≠ 0.

instance Affine.instNonemptySubtypeForallMemAffineSubspaceHVAdd_starlib {ι : Type u_1} {F : Type u_2} [Ring F] {v : ι → F} {s : AffineSubspace F (ι → F)} [inst : Nonempty ↥s] : Nonempty ↥(v +ᵥ s)

A translate of a nonempty affine subspace is nonempty.

@[reducible, inline]

abbrev Affine.AffSpanSet {ι : Type u_1} [Fintype ι] {F : Type u_2} {k : ℕ} [DecidableEq F] [Ring F] [NeZero k] (U : Fin k → ι → F) : Set (ι → F)

The carrier set of the affine span of the image of a function U : Fin k → ι → F. This is the set of all affine combinations of U 0, U 1, ..., U (k-1).

noncomputable def Affine.AffSpanFinset {ι : Type u_1} [Fintype ι] {F : Type u_2} {k : ℕ} [DecidableEq F] [Ring F] [Fintype F] [NeZero k] (U : Fin k → ι → F) : Finset (ι → F)

The affine span as a Finset, using AffSpanFinite to convert from the set.

noncomputable def Affine.AffSpanFinsetCollection {ι : Type u_1} [Fintype ι] {F : Type u_2} {k : ℕ} [DecidableEq F] [Ring F] [Fintype F] {t : ℕ} [NeZero k] [NeZero t] (C : Fin t → Fin k → ι → F) : Set (Finset (ι → F))

A collection of affine subspaces in F^ι.

instance Affine.instNonemptyElemCoeFinsetOfSubtypeMem_starlib {α : Type u_4} {s : Finset α} [inst : Nonempty ↥s] : Nonempty ↑↑s

The carrier set of a nonempty finset is nonempty.

@[implicit_reducible]

noncomputable instance Affine.instFintypeAffineSubspace {F : Type u_2} [Ring F] {V : Type u_4} [AddCommGroup V] [Module F V] [Fintype V] (S : AffineSubspace F V) : Fintype ↥S

Affine subspace carriers are Fintype when the ambient space is Fintype

instance Affine.instNonemptyAffineSubspace_mk' {F : Type u_2} [Ring F] {V : Type u_4} [AddCommGroup V] [Module F V] (p : V) (direction : Submodule F V) : Nonempty ↥(AffineSubspace.mk' p direction)

Affine subspaces constructed with mk' are always nonempty

@[reducible]

def Curve.polynomialCurveEval {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Semiring F] [AddCommMonoid A] [Module F A] {k : ℕ} (u : Fin k → ι → A) (r : F) : ι → A

Evaluate the polynomial curve generated by u at parameter r.

@[reducible]

def Curve.polynomialCurve {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Semiring F] [AddCommMonoid A] [Module F A] {k : ℕ} (u : Fin k → ι → A) : Set (ι → A)

(Parameterised) polynomial curve, Thm 1.5, [BCIKS20]: Let u := {u₀, ..., u_{k-1}} be a collection of vectors with coefficients in a semiring. The polynomial curve of degree k-1 generated by u is the set of linear combinations of the form {∑ i ∈ k, r ^ i • u_i | r ∈ F}.

def Curve.polynomialCurveFinite {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F : Type u_2} {A : Type u_3} [Semiring F] [Fintype F] [AddCommMonoid A] [Module F A] [Fintype A] [DecidableEq A] {k : ℕ} (u : Fin k → ι → A) : Finset (ι → A)

A polynomial curve over a finite field, as a Finset. Requires DecidableEq ι and DecidableEq F to be able to construct the Finset.

instance Curve.instNonemptySubtypeForallMemFinsetPolynomialCurveFinite {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F : Type u_2} {A : Type u_3} [Semiring F] [Fintype F] [AddCommMonoid A] [Module F A] [Fintype A] [DecidableEq A] [Nonempty F] {k : ℕ} (u : Fin k → ι → A) : Nonempty ↥(polynomialCurveFinite u)

A polynomial curve over a nonempty finite field contains at least one point.

instance Curve.instNonemptySubtypeForallMemFinsetPolynomialCurveFinite_1 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F : Type u_2} {A : Type u_3} [Semiring F] [Fintype F] [AddCommMonoid A] [Module F A] [Fintype A] [DecidableEq A] {k : ℕ} {u : Fin k → ι → A} : Nonempty ↥(polynomialCurveFinite u)

theorem sInf.sInf_UB_of_le_UB {S : Set ℕ} {i : ℕ} : (∀ s ∈ S, s ≤ i) → sInf S ≤ i

If every element of a set is bounded above by i, then the infimum is also bounded by i.

theorem sInf.le_sInf_of_LB {S : Set ℕ} (hne : S.Nonempty) {i : ℕ} (hLB : ∀ s ∈ S, i ≤ s) : i ≤ sInf S

If i is a lower bound for all elements in a nonempty set, then i is at most the infimum.

@[simp]

theorem Fintype.zero_lt_card {ι : Type u_1} [Fintype ι] [Nonempty ι] : 0 < card ι

A nonempty fintype has positive cardinality.

@[simp]

theorem Finset.card_filter_prod_self_eq {α : Type u_1} [DecidableEq α] {s : Finset α} : {x ∈ s ×ˢ s | x.1 = x.2}.card = s.card

The diagonal of s × s has the same cardinality as s.

@[simp]

theorem Finset.card_univ_filter_eq {α : Type u_1} [DecidableEq α] [Fintype α] {e : α} : {x : α | x ≠ e}.card = univ.card - 1

The number of elements different from a fixed element e is one less than the total.

@[simp]

theorem Finset.card_prod_self_eq {α : Type u_1} [DecidableEq α] {s : Finset α} [Fintype α] : (s ×ˢ s ∩ {x : α × α | x.1 = x.2}).card = s.card

The diagonal of s × s (intersection form) has the same cardinality as s.