Hamming spaces #
The Hamming metric counts the number of places two members of a (finite) Pi type differ. The Hamming norm is the same as the Hamming metric over additive groups, and counts the number of places a member of a (finite) Pi type differs from zero.
This is a useful notion in various applications, but in particular it is relevant in coding theory, in which it is fundamental for defining the minimum distance of a code.
Main definitions #
hammingDist x y
: the Hamming distance betweenx
andy
, the number of entries which differ.hammingNorm x
: the Hamming norm ofx
, the number of non-zero entries.Hamming β
: a type synonym forΠ i, β i
withdist
andnorm
provided by the above.Hamming.toHamming
,Hamming.ofHamming
: functions for casting betweenHamming β
andΠ i, β i
.- the Hamming norm forms a normed group on
Hamming β
.
The Hamming distance function to the naturals.
Instances For
Corresponds to dist_self
.
Corresponds to dist_nonneg
.
Corresponds to dist_comm
.
Corresponds to dist_triangle
.
Corresponds to dist_triangle_left
.
Corresponds to dist_triangle_right
.
Corresponds to swap_dist
.
Corresponds to eq_of_dist_eq_zero
.
Corresponds to dist_eq_zero
.
Corresponds to zero_eq_dist
.
Corresponds to dist_ne_zero
.
Corresponds to dist_pos
.
Corresponds to dist_smul
with the discrete norm on α
.
The Hamming weight function to the naturals.
Instances For
Corresponds to dist_zero_right
.
Corresponds to dist_zero_left
.
Corresponds to norm_nonneg
.
Corresponds to norm_zero
.
Corresponds to norm_eq_zero
.
Corresponds to norm_ne_zero_iff
.
Corresponds to norm_pos_iff
.
Corresponds to dist_eq_norm
.
Instances inherited from normal Pi types.
API to/from the type synonym.
Hamming.ofHamming
is the identity function from the Hamming
of a type.
Instances For
Instances equipping Hamming
with hammingNorm
and hammingDist
.