Hamming support, and Hamming data under coordinate decompositions and reindexing #
This file builds on hammingNorm, hammingDist, and hammingDist_eq_hammingNorm from
Mathlib.InformationTheory.Hamming.
The Hamming support of a word x : ι → A is Function.support x, the set of its nonzero
coordinates, and its Hamming weight is the number of elements of that support. The first part of
this file relates Function.support, its finset version, hammingNorm and hammingDist: the
distance from x to y is the weight of y - x, and the weight of a sum is governed by
wt(x + y) + #(supp x ∩ supp y) + #(supp x \ supp (x + y)) = wt x + wt y,
where the last set consists of the coordinates at which y cancels x. It follows that weight is
additive on words with disjoint supports; weight is also subadditive. Scaling coordinatewise by c
intersects the support with supp c.
The file also records that Hamming weight and distance on a function whose domain is a disjoint union split as sums over the two coordinate types. Weight also splits over a retained coordinate set and its complement. These identities let constructions assembled from independent coordinate blocks reduce their Hamming data to the data of the blocks.
It also proves that Hamming distance and Hamming weight are invariant under relabelling a finite
coordinate type along an equivalence, and evaluates a product over the coordinates of a word which
only depends on which coordinates vanish; this is how weight monomials X^(n - wt x) Y^(wt x)
factor over the coordinates.
Hamming support #
The Hamming weight of a word is the number of elements of its support.
The Hamming weight of a word is the cardinality of its support, viewed as a finset.
A word whose support is contained in the support of another word has at most its weight.
Two words with the same support have the same Hamming weight.
The Hamming distance between two words is the number of coordinates at which they differ.
Negation preserves Hamming weight.
The Hamming distance from x to y is the Hamming weight of x - y.
The Hamming distance from x to y is the Hamming weight of y - x.
The Hamming distance from x to y is the number of elements of the support of y - x.
Hamming weight is subadditive.
The weight of a sum. Coordinates in the support of both words are counted twice on the
right, and the coordinates at which y cancels x are lost from the support of x + y.
Words with disjoint supports have additive Hamming weight.
The weight of a coordinatewise scaling c • x is the number of coordinates at which both
c and x are nonzero.
A constant word has full weight unless its constant value is zero.
The Hamming distance between two pairs of words combined on a disjoint union is the sum of the distances between the respective words.
The Hamming weight of two words combined on a disjoint union is the sum of their weights.
The Hamming distance between two pairs of words over a common alphabet, combined on a disjoint union, is the sum of the distances between the respective words.
The Hamming weight of two words over a common alphabet, combined on a disjoint union, is the sum of their weights.
Hamming weight splits over a retained coordinate set and its complement.
A product over the coordinates which takes the value a at the zero coordinates of a word
and b elsewhere is a ^ (n - wt x) * b ^ (wt x), where n is the length and wt is the
Hamming weight.
Relabelling coordinates along an equivalence preserves the Hamming distance.
Relabelling coordinates along an equivalence preserves the Hamming weight.
Relabelling a word along an equivalence of finite coordinate types preserves its Hamming weight, when the relabelling is expressed as a linear map between function spaces.
Relabelling two words along an equivalence of finite coordinate types preserves their Hamming distance, when the relabelling is expressed as a linear map between function spaces.