Documentation

Starlib.Data.CodingTheory.Basic.DecodingRadius

Decoding Radius for Codes #

This module contains absolute and relative unique decoding radius definitions and the standard lemmas relating decoding-radius bounds to code distance.

source
noncomputable def Code.uniqueDecodingRadius {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) :
ℕ

The unique decoding radius: ≤ ⌊(d-1)/2⌋ for any code C.

Instances For
    source
    def Code.UDR {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) :
    ℕ

    Alias of Code.uniqueDecodingRadius.

    The unique decoding radius: ≤ ⌊(d-1)/2⌋ for any code C.

    Instances For
      source
      noncomputable def Code.relativeUniqueDecodingRadius {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) :
      NNReal

      The relative unique decoding radius, obtained from the absolute radius by normalizing with the block length. This also works with ≤.

      Instances For
        source
        def Code.relUDR {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) :
        NNReal

        Alias of Code.relativeUniqueDecodingRadius.

        The relative unique decoding radius, obtained from the absolute radius by normalizing with the block length. This also works with ≤.

        Instances For
          source
          @[simp]
          theorem Code.uniqueDecodingRadius_eq_floor_div_2 {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) :
          uniqueDecodingRadius C = ⌊(↑‖C‖₀ - 1) / 2⌋₊
          source
          theorem Code.UDRClose_iff_two_mul_proximity_lt_d_UDR {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) [NeZero ‖C‖₀] {e : ℕ} :
          e ≤ uniqueDecodingRadius C ↔ 2 * e < ‖C‖₀

          Given an error/proximity parameter e within the unique decoding radius of a code C where ‖C‖₀ > 0, this lemma proves the standard bound 2 * e < d (i.e. condition of Code.eq_of_lt_dist).

          source
          theorem Code.eq_of_le_uniqueDecodingRadius {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) (u : ι → F) {v w : ι → F} (hv : v ∈ C) (hw : w ∈ C) (huv : Δ₀(u, v) ≤ uniqueDecodingRadius C) (huw : Δ₀(u, w) ≤ uniqueDecodingRadius C) :
          v = w

          A stronger version of distFromCode_eq_of_lt_half_dist: If two codewords v and w are both within the uniqueDecodingRadius of u (i.e. 2 * Δ₀(u, v) < ‖C‖₀ and 2 * Δ₀(u, w) < ‖C‖₀), then they must be equal.

          source
          theorem Code.UDR_close_iff_exists_unique_close_codeword {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] (C : Set (ι → F)) [Nonempty ↑C] (u : ι → F) :
          Δ₀(u, C) ≤ ↑(uniqueDecodingRadius C) ↔ ∃! v : ι → F, v ∈ C ∧ Δ₀(u, v) ≤ uniqueDecodingRadius C

          A word u is within the uniqueDecodingRadius of a code C if and only if there exists exactly one codeword v in C that is that close.

          source
          theorem Code.UDR_close_iff_relURD_close {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) (u : ι → F) :
          Δ₀(u, C) ≤ ↑(uniqueDecodingRadius C) ↔ δᵣ(u, C) ≤ ↑(relativeUniqueDecodingRadius C)

          A word u is close to a code C within the absolute unique decoding radius if and only if it is close within the relative unique decoding radius.

          source
          @[simp]
          theorem Code.dist_le_UDR_iff_relDist_le_relUDR {ι : Type u_1} [Fintype ι] {F : Type u_2} [DecidableEq F] [Nonempty ι] (C : Set (ι → F)) (e : ℕ) :
          e ≤ uniqueDecodingRadius C ↔ ↑e / ↑(Fintype.card ι) ≤ relativeUniqueDecodingRadius C