Relative Distances for Codes

This module contains relative Hamming distance, relative distance-to-code, and the finite-range/computable variants used by the coding-theory development.

def Code.relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u v : ι → F) : ℚ≥0

def Code.«termδᵣ(_,_)» : Lean.ParserDescr

δᵣ(u,v) denotes the relative Hamming distance between vectors u and v.

noncomputable def Code.relDistFromCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u : ι → F) (C : Set (ι → F)) : ENNReal

The relative Hamming distance from a vector to a code, defined as the infimum of all relative distances from u to codewords in C. The type is ENNReal (ℝ≥0∞) to correctly handle the case C = ∅. For case of Nonempty C, we can use relDistFromCode (δᵣ') for smaller value range in ℚ≥0, which is equal to this definition.

def Code.«termδᵣ(_,_)_1» : Lean.ParserDescr

δᵣ(u,C) denotes the relative distance from u to C. This is the main standard definition used in statements. The NNRat version of it is δᵣ'(u, C).

theorem Code.relDistFromCode_le_relDist_to_mem {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (u : ι → F) {C : Set (ι → F)} (v : ι → F) (hv : v ∈ C) : δᵣ(u, C) ≤ ↑δᵣ(u, v)

The relative distance to a code is at most the relative distance to any specific codeword.

@[simp]

theorem Code.relDistFromCode_of_empty {n : Type u_1} [Fintype n] {R : Type u_2} [DecidableEq R] (u : n → R) : δᵣ(u, ∅) = ⊤

theorem Code.exists_relClosest_codeword_of_Nonempty_Code {ι : Type u_5} [Fintype ι] {F : Type u_6} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ∃ M ∈ C, ↑δᵣ(u, M) = δᵣ(u, C)

This follows proof strategy from exists_closest_codeword_of_Nonempty_Code. However, it's NOT used to construct pickRelClosestCodeword_of_Nonempty_Code.

theorem Code.relDistFromCode_eq_distFromCode_div {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (u : ι → F) (C : Set (ι → F)) : δᵣ(u, C) = ↑Δ₀(u, C) / ↑(Fintype.card ι)

theorem Code.pairDist_eq_distFromCode_iff_eq_relDistFromCode_div {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (u v : ι → F) (C : Set (ι → F)) [Nonempty ↑C] : ↑Δ₀(u, v) = Δ₀(u, C) ↔ ↑δᵣ(u, v) = δᵣ(u, C)

noncomputable def Code.pickRelClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : ↑C

Note that this gives the same codeword as pickClosestCodeword_of_Nonempty_Code.

theorem Code.relDistFromPickRelClosestCodeword_of_Nonempty_Code {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) : δᵣ(u, C) = ↑δᵣ(u, ↑(pickRelClosestCodeword_of_Nonempty_Code C u))

theorem Code.relCloseToCode_iff_relCloseToCodeword_of_minDist {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (δ : NNReal) : δᵣ(u, C) ≤ ↑δ ↔ ∃ v ∈ C, ↑δᵣ(u, v) ≤ δ

Relative distance version of closeToCode_iff_closeToCodeword_of_minDist. If the distance to a code is at most δ, then there exists a codeword within distance δ. NOTE: can we make this shorter using relDistFromCode_eq_distFromCode_div?

theorem Code.pairRelDist_le_iff_pairDist_le {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ Δ₀(u, v) ≤ ⌊δ * ↑(Fintype.card ι)⌋₊

Equivalence between relative and natural distance bounds.

theorem Code.distFromCode_le_iff_relDistFromCode_le {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] {C : Set (ι → F)} [Nonempty ι] (u : ι → F) (e : ℕ) : Δ₀(u, C) ≤ ↑e ↔ δᵣ(u, C) ≤ ↑↑e / ↑↑(Fintype.card ι)

A word u is close to a code C within an absolute error bound e if and only if it is close within the equivalent relative error bound e / n.

theorem Code.relDistFromCode_le_iff_distFromCode_le {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (δ : NNReal) : δᵣ(u, C) ≤ ↑δ ↔ Δ₀(u, C) ≤ ↑⌊δ * ↑(Fintype.card ι)⌋₊

A word u is relatively close to a code C within an relative error bound δ if and only if it is relatively close within the equivalent absolute error bound ⌊δ * n⌋.

theorem Code.relDistFromCode_le_iff_distFromCode_toENNReal_le {ι : Type u_3} [Fintype ι] {F : Type u_4} [Nonempty ι] [DecidableEq F] {C : Set (ι → F)} (u : ι → F) (δ : NNReal) : δᵣ(u, C) ≤ ↑δ ↔ ↑Δ₀(u, C) ≤ ↑δ * ↑↑(Fintype.card ι)

theorem Code.relCloseToWord_iff_exists_possibleDisagreeCols {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (u v : ι → F) (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ ∃ (D : Finset ι), D.card ≤ ⌊δ * ↑(Fintype.card ι)⌋₊ ∧ ∀ colIdx ∉ D, u colIdx = v colIdx

theorem Code.relCloseToWord_iff_exists_agreementCols {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (u v : ι → F) (δ : NNReal) : ↑δᵣ(u, v) ≤ δ ↔ ∃ (S : Finset ι), Fintype.card ι - ⌊δ * ↑(Fintype.card ι)⌋₊ ≤ S.card ∧ ∀ (colIdx : ι), (colIdx ∈ S → u colIdx = v colIdx) ∧ (u colIdx ≠ v colIdx → colIdx ∉ S)

theorem Code.NNReal.floor_ge_Nat_of_gt {r : NNReal} {n : ℕ} (h : r > ↑n) : ⌊r⌋₊ ≥ n

theorem Code.NNReal.sub_eq_zero_of_le (x y : NNReal) (h : x ≤ y) : x - y = 0

theorem Code.relDist_floor_bound_iff_complement_bound (n upperBound : ℕ) (δ : NNReal) : n - ⌊δ * ↑n⌋₊ ≤ upperBound ↔ (1 - δ) * ↑n ≤ ↑upperBound

The equivalence between the two lowerbound of upperBound in Nat and NNReal context. In which, upperBound is viewed as the size of an agreement set S (e.g. between two words, or between a word to a code, ...). Specifically, n - ⌊δ * n⌋ ≤ (upperBound : ℕ) ↔ (1 - δ) * n ≤ (upperBound : ℝ≥0). This lemma is useful for jumping back-and-forth between absolute distance and relative distance realms, especially when we work with an agreement set. For example, it can be used after simping with closeToWord_iff_exists_agreementCols and relCloseToWord_iff_exists_agreementCols.

@[simp]

theorem Code.relHammingDist_le_one {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : δᵣ(u, v) ≤ 1

The relative Hamming distance between two vectors is at most 1.

@[simp]

theorem Code.zero_le_relHammingDist {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [Nonempty ι] [DecidableEq F] : 0 ≤ δᵣ(u, v)

The relative Hamming distance between two vectors is non-negative.

def Code.relHammingDistRange (ι : Type u_5) [Fintype ι] : Set ℚ≥0

The range of the relative Hamming distance function.

@[simp]

theorem Code.relHammingDist_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {u v : ι → F} [DecidableEq F] : δᵣ(u, v) ∈ relHammingDistRange ι

The range of the relative Hamming distance is well-defined.

@[simp]

theorem Code.finite_relHammingDistRange {ι : Type u_3} [Fintype ι] [Nonempty ι] : (relHammingDistRange ι).Finite

The range of the relative Hamming distance function is finite.

@[simp]

theorem Code.finite_offDiag {ι : Type u_3} {F : Type u_4} {C : Set (ι → F)} [Finite ι] [Finite F] : C.offDiag.Finite

The set of pairs of distinct elements from a finite set is finite.

def Code.possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] (C : Set (ι → F)) : Set ℚ≥0

The set of possible distances between distinct codewords in a code.

@[simp]

theorem Code.possibleRelHammingDists_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] : possibleRelHammingDists C ⊆ relHammingDistRange ι

The set of possible distances between distinct codewords in a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem Code.finite_possibleRelHammingDists {ι : Type u_3} [Fintype ι] {F : Type u_4} {C : Set (ι → F)} [DecidableEq F] [Nonempty ι] : (possibleRelHammingDists C).Finite

The set of possible distances between distinct codewords in a code is a finite set.

noncomputable def Code.minRelHammingDistCode {ι : Type u_3} [Fintype ι] {F : Type u_4} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) : ℚ≥0

The minimum relative Hamming distance of a code.

def Code.termδᵣ_ : Lean.ParserDescr

δᵣ C denotes the minimum relative Hamming distance of a code C.

@[simp]

theorem Code.possibleRelHammingDistsToC_subset_relHammingDistRange {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [DecidableEq F] : possibleDistsToCode w C relHammingDist ⊆ relHammingDistRange ι

The range set of possible relative Hamming distances from a vector to a code is a subset of the range of the relative Hamming distance function.

@[simp]

theorem Code.finite_possibleRelHammingDistsToCode {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : (possibleDistsToCode w C relHammingDist).Finite

The set of possible relative Hamming distances from a vector to a code is a finite set.

@[implicit_reducible]

noncomputable instance Code.instFintypeElemNNRatPossibleDistsToCodeRelHammingDistOfNonempty {ι : Type u_3} [Fintype ι] {F : Type u_4} {w : ι → F} {C : Set (ι → F)} [Nonempty ι] [DecidableEq F] : Fintype ↑(possibleDistsToCode w C relHammingDist)

def Code.relDistFromCode' {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (w : ι → F) (C : Set (ι → F)) [Fintype ↑C] [Nonempty ↑C] : ℚ≥0

Computable version of the relative Hamming distance from a vector w to a finite non-empty code C. This one is intended to mimic the definition of distFromCode'. However, we don't have ENNRat (ℚ≥0∞) (as counterpart of ENat (ℕ∞) in distFromCode') so we require [Nonempty C]. TODO: define ENNRat (ℚ≥0∞) so we can migrate both relDistFromCode and relDistFromCode' to ℚ≥0∞

def Code.«termδᵣ'(_,_)» : Lean.ParserDescr

δᵣ'(w,C) denotes the relative Hamming distance between a vector w and a code C. This is a different statement of the generic definition δᵣ(w,C).

theorem Code.relDistFromCode'_eq_relDistFromCode {ι : Type u_5} [Fintype ι] [Nonempty ι] {F : Type u_6} [DecidableEq F] (w : ι → F) (C : Set (ι → F)) [Fintype ↑C] [Nonempty ↑C] : δᵣ(w, C) = ↑δᵣ'(w, C)

@[simp]

theorem Code.zero_mem_relHammingDistRange {ι : Type u_3} [Fintype ι] : 0 ∈ relHammingDistRange ι