diff --git a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean b/ArkLib/Data/CodingTheory/DivergenceOfSets.lean index b252e8836..b6ede0714 100644 --- a/ArkLib/Data/CodingTheory/DivergenceOfSets.lean +++ b/ArkLib/Data/CodingTheory/DivergenceOfSets.lean @@ -1,5 +1,15 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import ArkLib.Data.CodingTheory.RelativeHammingDistance +/- +Proved definiton for divergence of an arbitrary set `U` from an arbitrary set `V`. +-/ + namespace DivergenceOfSets noncomputable section @@ -11,7 +21,7 @@ variable {ι : Type*} [Fintype ι] {U V C : Set (ι → F)} /-- -`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V` +`d_U` is the set of achievable relative Hamming distances between elements `u ∈ U` and `V`. -/ def d_U [Nonempty ι] (U V : Set (ι → F)) : Set ℚ := { d : ℚ | ∃ u ∈ U, δᵣ(u,V) = d } @@ -26,7 +36,7 @@ lemma finite_d_U [Nonempty ι] : (d_U U V).Finite := Set.Finite.subset RelativeHamming.finite_relHammingDistRange d_U_subset_relHammingDistRange /-- -divergence of the arbitrary set `U` to the arbitrary set `V` +divergence of an arbitrary set `U` from an arbitrary set `V`. -/ def div_U_from_V [Nonempty ι] (U : Set (ι → F)) (V : Set (ι → F)) : ℚ := have : Fintype (d_U U V) := @Fintype.ofFinite _ finite_d_U diff --git a/ArkLib/Data/CodingTheory/InterleavedCodes.lean b/ArkLib/Data/CodingTheory/InterleavedCodes.lean index c0dde66cc..38d6329db 100644 --- a/ArkLib/Data/CodingTheory/InterleavedCodes.lean +++ b/ArkLib/Data/CodingTheory/InterleavedCodes.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši +-/ + import Mathlib.Algebra.Module.Submodule.Defs import Mathlib.Data.Matrix.Defs import Mathlib.Data.Matrix.RowCol @@ -9,30 +15,39 @@ import ArkLib.Data.CodingTheory.LinearCodes import ArkLib.Data.CodingTheory.ReedSolomon import ArkLib.Data.CodingTheory.Prelims + open Classical LinearCodes noncomputable section +/- +Definition of a `κ`-interleaved code `IC` of a linear code `LC` over a semiring `F`. +Definition of distances for interleaved codes and statement for the relation between the minimal +distance of an interleaved code and its underlying linear code. +Statements of proximity results for Reed Solomon codes +(`Lemma 4.3`, `Lemma 4.4` and `Lemma 4.5` from Ligero) with proximity parameter less than +the minimal code distance divided by `3`. +-/ + variable {F : Type*} [Semiring F] {κ ι: ℕ} {LC : LinearCode ι F} namespace InterleavedCodes --- Question: in the abbrev, do we need to add the condition which makes a submodule of --- the given type an interleaved code? (it's in the def below) - -/-- - @KATY: Probably a bad name, I just followed the 'Submodule F (Fin ι → F)' for 'LinearCode' exmpl. - Feel free to either remove this altogether or name this better :). --/ abbrev MatrixSubmodule.{u} (κ ι : ℕ) (F : Type u) [Semiring F] : Type u := Submodule F (Matrix (Fin κ) (Fin ι) F) +/-- +The data needed to construct an interleaved code +-/ structure InterleavedCode (κ ι : ℕ) (F : Type*) [Semiring F] where MF : MatrixSubmodule κ ι F LC : LinearCode ι F +/-- +The condition making the InterleavedCode structure an interleaved code. +-/ def InterleavedCode.isInterleaved (IC : InterleavedCode κ ι F) := ∀ V ∈ IC.MF, ∀ i, V i ∈ IC.LC @@ -46,10 +61,13 @@ def codeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : InterleavedCode κ ι F { MF := matrixSubmoduleOfLinearCode κ LC, LC := LC } lemma isInterleaved_codeOfLinearCode : (codeOfLinearCode κ LC).isInterleaved := by sorry - + def lawfulInterleavedCodeOfLinearCode (κ : ℕ) (LC : LinearCode ι F) : LawfulInterleavedCode κ ι F := ⟨codeOfLinearCode κ LC, isInterleaved_codeOfLinearCode⟩ +/-- +distance between codewords `U` and `V` in a `κ`-interleaved code. + -/ def distCodewords (U V : Matrix (Fin κ) (Fin ι) F) : ℕ := (Matrix.neqCols U V).card @@ -62,7 +80,7 @@ def minDist (IC : MatrixSubmodule κ ι F) : ℕ := sInf { d : ℕ | ∃ U ∈ IC, ∃ V ∈ IC, distCodewords U V = d } /-- -`Δ IC` is the min distance of an interleaved code `IC` +`Δ IC` is the min distance of an interleaved code `IC`. -/ notation "Δ" IC => minDist IC diff --git a/ArkLib/Data/CodingTheory/LinearCodes.lean b/ArkLib/Data/CodingTheory/LinearCodes.lean index 4376c47fd..2f8f7a2f4 100644 --- a/ArkLib/Data/CodingTheory/LinearCodes.lean +++ b/ArkLib/Data/CodingTheory/LinearCodes.lean @@ -1,9 +1,22 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import Mathlib.Data.Matrix.Rank import Mathlib.InformationTheory.Hamming import Mathlib.LinearAlgebra.Matrix.ToLin import Mathlib.Algebra.Module.Submodule.Range import Mathlib.Algebra.Module.Submodule.Defs +/-! + Definition of a linear code, minimal distance of a linear code, length, dimension and rate. + Linear codes defined by a generator matrices and rephrase of dimension in this framework. + Definition of the weight of a vector, statement and proof of the fact that the minimal + distance of a linear code equals the minimal weight taken over the set of codewords. +-/ + open Classical open Finset @@ -76,6 +89,9 @@ lemma minDist_eq_minWtCodewords {LC : LinearCode ι F} : minDist LC = minWtCodew refine congrArg _ (Set.ext fun _ ↦ ⟨fun ⟨u, _, v, _⟩ ↦ ⟨u - v, ?p₁⟩, fun _ ↦ ⟨0, ?p₂⟩⟩) <;> aesop (add simp [hammingDist_eq_wt_sub, sub_eq_zero]) +/-- +Singleton Bound Theorem. +-/ theorem singletonBound (LC : LinearCode ι F) : dim LC ≤ length LC - minDist LC + 1 := by sorry diff --git a/ArkLib/Data/CodingTheory/Prelims.lean b/ArkLib/Data/CodingTheory/Prelims.lean index 0fec94527..569ca764b 100644 --- a/ArkLib/Data/CodingTheory/Prelims.lean +++ b/ArkLib/Data/CodingTheory/Prelims.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši +-/ + import Mathlib.Algebra.Module.Submodule.Defs import Mathlib.Data.Matrix.Defs import Mathlib.Data.Matrix.RowCol @@ -79,11 +85,9 @@ end Embedding namespace Affine /-- -Affine line between two vectors with coefficients in a semiring. +affine line between vectors `u` and `v`. -/ def line [Ring F] (u v : Fin ι → F) : Set (Fin ι → F) := {x | ∃ γ : F, x = γ • u + (1 - γ) • v} end Affine - -end diff --git a/ArkLib/Data/CodingTheory/ReedSolomon.lean b/ArkLib/Data/CodingTheory/ReedSolomon.lean index 62f781e3a..22fe9d2db 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomon.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomon.lean @@ -17,7 +17,6 @@ import Mathlib.Data.FinEnum list-decoding. -/ - namespace ReedSolomon open Polynomial diff --git a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean index 20df0a691..08aff9394 100644 --- a/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean +++ b/ArkLib/Data/CodingTheory/ReedSolomonCodes.lean @@ -13,11 +13,17 @@ variable {ι : ℕ} noncomputable section namespace Vandermonde + /-- A non-square Vandermonde matrix. -/ def nonsquare [Semiring F] (deg : ℕ) (α : Fin ι ↪ F) : Matrix (Fin ι) (Fin deg) F := - Matrix.of (fun i j => (α i) ^ j.1) + Matrix.of fun i j => (α i) ^ j.1 + +lemma nonsquare_mulVecLin [CommSemiring F] + {deg : ℕ} {α₁ : Fin ι ↪ F} {α₂ : Fin deg → F} {i : Fin ι} : + (nonsquare deg α₁).mulVecLin α₂ i = ∑ x, α₂ x * α₁ i ^ (↑x : ℕ) := by + simp [nonsquare, Matrix.mulVecLin_apply, Matrix.mulVec_eq_sum] /-- The transpose of a non-square Vandermonde matrix. @@ -79,186 +85,130 @@ lemma rank_nonsquare_rows_eq_min [CommRing F] [IsDomain F] {deg : ℕ} {α : Fin aesop (add simp [rank_nonsquare_eq_deg_of_ι_le, rank_nonsquare_eq_deg_of_deg_le]) (add safe forward le_of_lt) -theorem eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials - {deg : ℕ} [CommRing F] {v : Fin ι ↪ F} - {p : F[X]} (h_deg : p.natDegree ≤ deg) : - (Vandermonde.nonsquare (deg + 1) v).mulVecLin (p.coeff ∘ Fin.val) = - (fun i => (p.eval (v i))) := by - rw [Matrix.mulVecLin_apply] - unfold Matrix.mulVec Vandermonde.nonsquare dotProduct - simp only [Matrix.of_apply, Function.comp_apply] - funext i - rw [Polynomial.eval_eq_sum, sum_def] - apply Eq.symm - apply Finset.sum_of_injOn (Fin.ofNat' (deg + 1)) - · unfold Set.InjOn - intro x₁ h₁ x₂ h₂ h - have h₁' : x₁ < deg + 1 := by - have := Polynomial.le_natDegree_of_mem_supp _ h₁ - linarith - have h₂' : x₂ < deg + 1 := by - have := Polynomial.le_natDegree_of_mem_supp _ h₂ - linarith - have : (Fin.ofNat' (deg + 1) x₁ : ℕ) = (Fin.ofNat' (deg + 1) x₁ : ℕ) := by rfl - rw (occs := .pos [2]) [h] at this - rw [Fin.val_ofNat', Fin.val_ofNat', Nat.mod_eq_of_lt h₁', Nat.mod_eq_of_lt h₂'] at this - exact this - · unfold Set.MapsTo - intros x h - simp - · intros i _ h - simp only [Fin.ofNat'_eq_cast, Set.mem_image, Finset.mem_coe, mem_support_iff, ne_eq, - not_exists, not_and] at h - specialize h i.val - simp only [Fin.cast_val_eq_self, not_true_eq_false, imp_false, Decidable.not_not] at h - rw [h, mul_zero] - · intros i h - rw [Fin.val_ofNat'] - have : i < deg + 1 := by - apply lt_of_le_of_lt (Polynomial.le_natDegree_of_mem_supp i h) - linarith - rw [Nat.mod_eq_of_lt this] - ring +theorem mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials + {deg : ℕ} [NeZero deg] [CommRing F] {v : Fin ι ↪ F} + {p : F[X]} (h_deg : p.natDegree < deg) : + (Vandermonde.nonsquare deg v).mulVecLin (p.coeff ∘ Fin.val) = -- NOTE: Use `liftF`. + fun i => p.eval (v i) := by + ext i + simp only [ + nonsquare_mulVecLin, Finset.sum_fin_eq_sum_range, eval_eq_sum + ] + refine Eq.symm (Finset.sum_of_injOn (·%deg) ?p₁ ?p₂ (fun i _ h ↦ ?p₃) (fun i _ ↦ ?p₄)) + · aesop (add simp [Set.InjOn]) + (add safe forward [le_natDegree_of_mem_supp, lt_of_le_of_lt, Nat.lt_add_one_of_le]) + (add 10% apply (show ∀ {a b c : ℕ}, a < c → b < c → a % c = b % c → a = b from + fun h₁ h₂ ↦ by aesop (add simp Nat.mod_eq_of_lt))) + (erase simp mem_support_iff) + · aesop (add simp Set.MapsTo) (add safe apply Nat.mod_lt) (add 1% cases Nat) + · aesop (add safe (by specialize h i)) (add simp Nat.mod_eq_of_lt) + · have : i < deg := by aesop (add safe forward le_natDegree_of_mem_supp) + (erase simp mem_support_iff) + (add safe (by omega)) + aesop (add simp Nat.mod_eq_of_lt) (add safe (by ring)) end Vandermonde namespace ReedSolomonCode -lemma degree_lt [Semiring F] {p : F[X]} {deg : ℕ} [NeZero deg] : - (∀ i, i ≥ deg → p.coeff i = 0) → p.natDegree < deg := by - intro h - by_contra! h' - specialize h p.natDegree h' - simp_all only - [ - coeff_natDegree, leadingCoeff_eq_zero, natDegree_zero, - nonpos_iff_eq_zero, neZero_zero_iff_false - ] +section + +variable [Semiring F] {p : F[X]} + {deg : ℕ} [NeZero deg] + {coeffs : Fin deg → F} + +lemma natDegree_lt_of_lbounded_zero_coeff + (h : ∀ i, deg ≤ i → p.coeff i = 0) : p.natDegree < deg := by + aesop (add unsafe [(by by_contra), (by specialize h p.natDegree)]) + +def polynomialOfCoeffs (coeffs : Fin deg → F) : F[X] := + ⟨ + Finset.map ⟨Fin.val, Fin.val_injective⟩ {i | coeffs i ≠ 0}, + fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, + fun a ↦ by aesop (add safe (by existsi a)) + (add simp [Fin.natCast_def, Nat.mod_eq_of_lt]) + ⟩ + +@[simp] +lemma natDegree_polynomialOfCoeffs_deg_lt_deg : (polynomialOfCoeffs coeffs).natDegree < deg := by + aesop (add simp polynomialOfCoeffs) + (add safe apply natDegree_lt_of_lbounded_zero_coeff) + +@[simp] +lemma degree_polynomialOfCoeffs_deg_lt_deg : (polynomialOfCoeffs coeffs).degree < deg := by + aesop (add simp [polynomialOfCoeffs, degree_lt_iff_coeff_zero]) + +@[simp] +lemma coeff_polynomialOfCoeffs_eq_coeffs : + (polynomialOfCoeffs coeffs).coeff ∘ Fin.val = coeffs := by -- NOTE TO SELF: `liftF' coeffs`! + aesop (add simp polynomialOfCoeffs) + +@[simp] +lemma polynomialOfCoeffs_mem_degreeLT : polynomialOfCoeffs coeffs ∈ degreeLT F deg := by + aesop (add simp Polynomial.mem_degreeLT) -lemma exists_poly_of_coeffs [Semiring F] (deg : ℕ) [NeZero deg] (coeffs : Fin deg → F) : - ∃ p : F[X], coeffs = p.coeff ∘ Fin.val ∧ p.natDegree < deg := by - have : Function.Injective (Fin.val : Fin deg → ℕ) := by - unfold Function.Injective - aesop - let support := Finset.map ⟨Fin.val, this⟩ (Finset.filter (fun i ↦ coeffs i ≠ 0) Finset.univ) - let p : F[X] := - ⟨ - support, - fun i ↦ if h : i < deg then coeffs ⟨i, h⟩ else 0, - by - dsimp [support] - intros a - simp_all only - [ - Finset.mem_map, Finset.mem_filter, Finset.mem_univ, - true_and, Function.Embedding.coeFn_mk, - dite_eq_right_iff, not_forall, support - ] - apply Iff.intro - · intro a_1 - obtain ⟨w, h⟩ := a_1 - obtain ⟨left, right⟩ := h - subst right - simp_all only [Fin.eta, not_false_eq_true, Fin.is_lt, exists_const, support] - · intro a_1 - obtain ⟨w, h⟩ := a_1 - exists ⟨a, w⟩ - ⟩ - exists p - simp only [coeff_ofFinsupp, Finsupp.coe_mk, support, p] - apply And.intro - · aesop - · apply degree_lt; aesop +lemma natDegree_lt_of_mem_degreeLT (h : p ∈ degreeLT F deg) : p.natDegree < deg := by + by_cases p = 0 + · cases deg <;> aesop + · aesop (add simp [natDegree_lt_iff_degree_lt, mem_degreeLT]) + +end + +section + +variable {deg : ℕ} [Field F] {α : Fin ι ↪ F} /-- The generator matrix of a Reed-Solomon code is a Vandermonde matrix. -/ -lemma genMatIsVandermonde [Field F] {deg : ℕ} [inst : NeZero deg] (α : Fin ι ↪ F) : +lemma genMatIsVandermonde [NeZero deg] : LinearCodes.genMat_mul (Vandermonde.nonsquare deg α) = ReedSolomon.code α deg := by unfold LinearCodes.genMat_mul ReedSolomon.code - apply Submodule.ext - intros x - apply Iff.intro - · intros h - rw [LinearMap.mem_range] at h - rcases h with ⟨coeffs, h⟩ - rcases exists_poly_of_coeffs deg coeffs with ⟨p, h', p_deg⟩ - rw [h'] at h - match deg_def : deg with - | .zero => aesop - | deg + 1 => - rw [Vandermonde.eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials (by linarith)] at h - rw [←h, Submodule.mem_map] - exists p - apply And.intro - · rw [Polynomial.mem_degreeLT] - by_cases p_ne_zero : p ≠ 0 - · rw - [ - Polynomial.degree_eq_natDegree p_ne_zero, - Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe - ] - exact p_deg - · simp only [ne_eq, Decidable.not_not] at p_ne_zero - rw [p_ne_zero, Polynomial.degree_zero, Nat.cast_withBot] - simp - decide - · simp only [ReedSolomon.evalOnPoints, LinearMap.coe_mk, AddHom.coe_mk] - · intros h - rw [Submodule.mem_map] at h - rcases h with ⟨p, h⟩ - rw [LinearMap.mem_range] - exists (p.coeff ∘ Fin.val) - match def_def : deg with - | .zero => aesop - | deg + 1 => - rw [Polynomial.mem_degreeLT] at h - rw [Vandermonde.eval_matrixOfPolynomials_eq_nsvandermonde_mul_matrixOfPolynomials, ←h.2] - unfold ReedSolomon.evalOnPoints - simp only [LinearMap.coe_mk, AddHom.coe_mk] - by_cases p_ne_zero : p ≠ 0 - · rw - [ - Polynomial.degree_eq_natDegree p_ne_zero, - Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe - ] at h - linarith - · aesop + ext x; rw [LinearMap.mem_range, Submodule.mem_map] + refine ⟨ + fun ⟨coeffs, h⟩ ↦ ⟨polynomialOfCoeffs coeffs, h.symm ▸ ?p₁⟩, + fun ⟨p, h⟩ ↦ ⟨p.coeff ∘ Fin.val, ?p₂⟩ + ⟩ + · rw [ + ←coeff_polynomialOfCoeffs_eq_coeffs (coeffs := coeffs), + Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials (by simp) + ] + simp [ReedSolomon.evalOnPoints] + · exact h.2 ▸ Vandermonde.mulVecLin_coeff_vandermondens_eq_eval_matrixOfPolynomials + (natDegree_lt_of_mem_degreeLT h.1) -- for RS codes we know `deg ≤ ι ≤ |F|`. `ι ≤ |F|` is clear from the embedding. -- Check : is `deg ≤ ι` implemented in Quang's defn? Answer: not explicitly. Worth mentioning?? -/-- -The dimension of a Reed-Solomon code is the maximal degree of the polynomials. --/ -lemma dim_eq_deg [Field F] {deg : ℕ} [NeZero deg] {α : Fin ι ↪ F} (h : deg ≤ ι) : +lemma dim_eq_deg [NeZero deg] (h : deg ≤ ι) : LinearCodes.dim (ReedSolomon.code α deg) = deg := by rw [←genMatIsVandermonde, ←LinearCodes.dimEqRankGenMat] - aesop + simpa -/-- -The length of a Reed-Solomon code is the domain size. --/ -lemma length_eq_domain_size [Field F] {deg : ℕ} {α : Fin ι ↪ F} : +@[simp] +lemma length_eq_domain_size : LinearCodes.length (ReedSolomon.code α deg) = ι := by - rw[LinearCodes.length] + rw [LinearCodes.length] simp -/-- -The rate of a Reed-Solomon code. --/ -lemma rate [Field F] {deg : ℕ} [NeZero deg] {α : Fin ι ↪ F} (h : deg ≤ ι) : +lemma rate [NeZero deg] (h : deg ≤ ι) : LinearCodes.rate (ReedSolomon.code α deg) = deg / ι := by - rw[LinearCodes.rate, dim_eq_deg, length_eq_domain_size] - exact h + rwa [LinearCodes.rate, dim_eq_deg, length_eq_domain_size] /-- The minimal code distance of a Reed-Solomon given by the degree and domain size. -/ -lemma minDist [Field F] {deg : ℕ} {α : Fin ι ↪ F} : - LinearCodes.minDist (ReedSolomon.code α deg) = ι - deg + 1 := by sorry - +lemma minDist [NeZero deg] (h : deg ≤ ι) : + LinearCodes.minDist (ReedSolomon.code α deg) = ι - deg + 1 := by + have : NeZero ι := by constructor; aesop + refine le_antisymm ?p₁ ?p₂ + case p₁ => sorry + case p₂ => + choose c hc using show ∃ c, c ∈ ReedSolomon.code α deg by sorry + let p := polynomialOfCoeffs c + sorry +end end ReedSolomonCode end diff --git a/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean b/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean index 084fbabc1..e60648659 100644 --- a/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean +++ b/ArkLib/Data/CodingTheory/RelativeHammingDistance.lean @@ -1,6 +1,16 @@ +/- +Copyright (c) 2024-2025 ArkLib Contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Katerina Hristova, František Silváši, Julian Sutherland +-/ + import Mathlib.InformationTheory.Hamming import Mathlib.Analysis.Normed.Field.Lemmas +/-! +proved definitions of relative Hamming distance and related notions for a linear code `LC`, +including corner cases. +-/ open Classical variable {ι : Type*} [Fintype ι] @@ -23,7 +33,7 @@ section variable [Nonempty ι] /-- - relative Hamming distance between vectors `u` and `v` + relative Hamming distance between vectors `u` and `v`. -/ def dist (u v : ι → F) : ℚ := (hammingDist u v : ℚ) / (Fintype.card ι : ℚ) @@ -43,10 +53,13 @@ lemma zero_le_relHammingDist : 0 ≤ dist u v := by end /-- -`δᵣ(u,v)` denotes the relative Hamming distance between vectors `u` and `v` +`δᵣ(u,v)` denotes the relative Hamming distance between vectors `u` and `v`. -/ notation "δᵣ(" u ", " v ")" => dist u v +/-- +the range of the relative Hamming distance function. +-/ def distRange (ι : Type*) [Fintype ι] : Set ℚ := { d : ℚ | ∃ d' : ℕ, d' ≤ Fintype.card ι ∧ d = d' / Fintype.card ι } @@ -72,7 +85,7 @@ lemma finite_relHammingDistRange [Nonempty ι] : (distRange ι).Finite := by lemma finite_offDiag [Finite F] : C.offDiag.Finite := Set.Finite.offDiag (Set.toFinite _) /-- -The set of possible distances between distinct codewords of `C` +The set of possible distances between distinct codewords of `C`. -/ def d_C (C : Set (ι → F)) : Set ℚ := { d : ℚ | ∃ p ∈ Set.offDiag C, δᵣ(p.1, p.2) = d } @@ -90,7 +103,7 @@ lemma finite_d_C [Nonempty ι] : (d_C C).Finite := end /-- -relative Hamming Distance of a code C over a semiring F +relative Hamming Distance of a code `C`. -/ def minDistCode [Nonempty ι] (C : Set (ι → F)) : ℚ := have : Fintype (d_C C) := @Fintype.ofFinite _ finite_d_C @@ -120,7 +133,7 @@ lemma finite_d_w [Nonempty ι] : (d_w w C).Finite := instance [Nonempty ι] : Fintype (d_w w C) := @Fintype.ofFinite _ finite_d_w /-- -relative Hamming distance between a vector `w` and a code `C` +relative Hamming distance between a vector `w` and a code `C`. -/ def distToCode [Nonempty ι] (w : ι → F) (C : Set (ι → F)) : ℚ := if h : (d_w w C).Nonempty