Documentation

TauCeti.InformationTheory.Coding.Weight.Euclidean

Euclidean weights of words over ℤ/n #

The Euclidean weight of a residue a modulo n is the square of the distance from a to 0 on the cycle ℤ/n, namely min (a, n - a)² for the representative 0 ≤ a < n; in Mathlib's terms it is the square of the absolute value of ZMod.valMinAbs a. The Euclidean weight of a word is the sum of the Euclidean weights of its coordinates, that is, the squared Euclidean norm of the word's least absolute integer lift.

Euclidean weights are the weights used for codes over ℤ/2k whose Construction A lattices are even: the Type II condition over ℤ/2^r asks that all Euclidean weights be divisible by 2^(r+1). Over ℤ/2 the Euclidean weight is the Hamming weight.

References #

source
def TauCeti.euclideanWeight {ι : Type u_1} [Fintype ι] {n : ℕ} (x : ι → ZMod n) :
ℕ

The Euclidean weight of a word over ℤ/n: the sum over the coordinates of the squares of their least absolute integer representatives.

Instances For
    source
    theorem TauCeti.euclideanWeight_def {ι : Type u_1} [Fintype ι] {n : ℕ} (x : ι → ZMod n) :
    euclideanWeight x = ∑ i : ι, (x i).valMinAbs.natAbs ^ 2
    source
    theorem TauCeti.natCast_euclideanWeight {ι : Type u_1} [Fintype ι] {n : ℕ} (x : ι → ZMod n) :
    ↑(euclideanWeight x) = ∑ i : ι, (x i).valMinAbs ^ 2

    The Euclidean weight of a word is the sum of the squares of the least absolute integer representatives of its coordinates.

    source
    theorem TauCeti.euclideanWeight_eq_sum_min {ι : Type u_1} [Fintype ι] {n : ℕ} [NeZero n] (x : ι → ZMod n) :
    euclideanWeight x = ∑ i : ι, min (x i).val (n - (x i).val) ^ 2

    For a nonzero modulus, the Euclidean weight of a word is the sum over the coordinates of min (a, n - a)², where 0 ≤ a < n is the canonical representative of the coordinate.

    source
    @[simp]
    theorem TauCeti.euclideanWeight_zero {ι : Type u_1} [Fintype ι] {n : ℕ} :
    euclideanWeight 0 = 0

    The zero word has Euclidean weight zero.

    source
    @[simp]
    theorem TauCeti.euclideanWeight_eq_zero {ι : Type u_1} [Fintype ι] {n : ℕ} {x : ι → ZMod n} :
    euclideanWeight x = 0 ↔ x = 0

    Only the zero word has Euclidean weight zero.

    source
    @[simp]
    theorem TauCeti.euclideanWeight_neg {ι : Type u_1} [Fintype ι] {n : ℕ} (x : ι → ZMod n) :
    euclideanWeight (-x) = euclideanWeight x

    Negating a word does not change its Euclidean weight.

    source
    @[simp]
    theorem TauCeti.euclideanWeight_eq_hammingNorm {ι : Type u_1} [Fintype ι] (x : ι → ZMod 2) :
    euclideanWeight x = hammingNorm x

    Over ℤ/2 the Euclidean weight of a word is its Hamming weight.

    source
    theorem TauCeti.hammingNorm_intCast_le_sum_sq {ι : Type u_1} [Fintype ι] (z : ι → ℤ) :
    ↑(hammingNorm fun (i : ι) => ↑(z i)) ≤ ∑ i : ι, z i ^ 2

    The Hamming weight of the binary reduction of an integer vector is bounded by its sum of squares.