# 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 between x and y, the number of entries which differ.
• hammingNorm x: the Hamming norm of x, the number of non-zero entries.
• Hamming β: a type synonym for Π i, β i with dist and norm provided by the above.
• Hamming.toHamming, Hamming.ofHamming: functions for casting between Hamming β and Π i, β i.
• the Hamming norm forms a normed group on Hamming β.
def hammingDist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) :

The Hamming distance function to the naturals.

Equations
Instances For
@[simp]
theorem hammingDist_self {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) :
= 0

Corresponds to dist_self.

theorem hammingDist_nonneg {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
0

Corresponds to dist_nonneg.

theorem hammingDist_comm {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) :
=

Corresponds to dist_comm.

theorem hammingDist_triangle {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) (z : (i : ι) → β i) :
+

Corresponds to dist_triangle.

theorem hammingDist_triangle_left {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) (z : (i : ι) → β i) :
+

Corresponds to dist_triangle_left.

theorem hammingDist_triangle_right {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) (z : (i : ι) → β i) :
+

Corresponds to dist_triangle_right.

theorem swap_hammingDist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] :
Function.swap hammingDist = hammingDist

Corresponds to swap_dist.

theorem eq_of_hammingDist_eq_zero {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
= 0x = y

Corresponds to eq_of_dist_eq_zero.

@[simp]
theorem hammingDist_eq_zero {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
= 0 x = y

Corresponds to dist_eq_zero.

@[simp]
theorem hamming_zero_eq_dist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
0 = x = y

Corresponds to zero_eq_dist.

theorem hammingDist_ne_zero {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
0 x y

Corresponds to dist_ne_zero.

@[simp]
theorem hammingDist_pos {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
0 < x y

Corresponds to dist_pos.

theorem hammingDist_lt_one {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
< 1 x = y
theorem hammingDist_le_card_fintype {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
theorem hammingDist_comp_le_hammingDist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {γ : ιType u_4} [(i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ iβ i) {x : (i : ι) → γ i} {y : (i : ι) → γ i} :
(hammingDist (fun (i : ι) => f i (x i)) fun (i : ι) => f i (y i))
theorem hammingDist_comp {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {γ : ιType u_4} [(i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ iβ i) {x : (i : ι) → γ i} {y : (i : ι) → γ i} (hf : ∀ (i : ι), Function.Injective (f i)) :
(hammingDist (fun (i : ι) => f i (x i)) fun (i : ι) => f i (y i)) =
theorem hammingDist_smul_le_hammingDist {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul α (β i)] {k : α} {x : (i : ι) → β i} {y : (i : ι) → β i} :
hammingDist (k x) (k y)
theorem hammingDist_smul {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul α (β i)] {k : α} {x : (i : ι) → β i} {y : (i : ι) → β i} (hk : ∀ (i : ι), IsSMulRegular (β i) k) :
hammingDist (k x) (k y) =

Corresponds to dist_smul with the discrete norm on α.

def hammingNorm {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : (i : ι) → β i) :

The Hamming weight function to the naturals.

Equations
Instances For
@[simp]
theorem hammingDist_zero_right {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : (i : ι) → β i) :
=

Corresponds to dist_zero_right.

@[simp]
theorem hammingDist_zero_left {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] :
= hammingNorm

Corresponds to dist_zero_left.

theorem hammingNorm_nonneg {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
0

Corresponds to norm_nonneg.

@[simp]
theorem hammingNorm_zero {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] :
= 0

Corresponds to norm_zero.

@[simp]
theorem hammingNorm_eq_zero {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
= 0 x = 0

Corresponds to norm_eq_zero.

theorem hammingNorm_ne_zero_iff {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
0 x 0

Corresponds to norm_ne_zero_iff.

@[simp]
theorem hammingNorm_pos_iff {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
0 < x 0

Corresponds to norm_pos_iff.

theorem hammingNorm_lt_one {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
< 1 x = 0
theorem hammingNorm_le_card_fintype {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} :
theorem hammingNorm_comp_le_hammingNorm {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {γ : ιType u_4} [(i : ι) → DecidableEq (γ i)] [(i : ι) → Zero (β i)] [(i : ι) → Zero (γ i)] (f : (i : ι) → γ iβ i) {x : (i : ι) → γ i} (hf : ∀ (i : ι), f i 0 = 0) :
(hammingNorm fun (i : ι) => f i (x i))
theorem hammingNorm_comp {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] {γ : ιType u_4} [(i : ι) → DecidableEq (γ i)] [(i : ι) → Zero (β i)] [(i : ι) → Zero (γ i)] (f : (i : ι) → γ iβ i) {x : (i : ι) → γ i} (hf₁ : ∀ (i : ι), Function.Injective (f i)) (hf₂ : ∀ (i : ι), f i 0 = 0) :
(hammingNorm fun (i : ι) => f i (x i)) =
theorem hammingNorm_smul_le_hammingNorm {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] [Zero α] [(i : ι) → SMulWithZero α (β i)] {k : α} {x : (i : ι) → β i} :
theorem hammingNorm_smul {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] [Zero α] [(i : ι) → SMulWithZero α (β i)] {k : α} (hk : ∀ (i : ι), IsSMulRegular (β i) k) (x : (i : ι) → β i) :
theorem hammingDist_eq_hammingNorm {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) :
= hammingNorm (x - y)

Corresponds to dist_eq_norm.

### The Hamming type synonym #

def Hamming {ι : Type u_1} (β : ιType u_2) :
Type (max u_1 u_2)

Type synonym for a Pi type which inherits the usual algebraic instances, but is equipped with the Hamming metric and norm, instead of Pi.normedAddCommGroup which uses the sup norm.

Equations
• = ((i : ι) → β i)
Instances For

Instances inherited from normal Pi types.

instance Hamming.instInhabitedHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → Inhabited (β i)] :
Equations
• Hamming.instInhabitedHamming = { default := fun (x : ι) => default }
instance Hamming.instFintypeHamming {ι : Type u_2} {β : ιType u_3} [] [] [(i : ι) → Fintype (β i)] :
Equations
• Hamming.instFintypeHamming = Pi.fintype
instance Hamming.instNontrivialHamming {ι : Type u_2} {β : ιType u_3} [] [∀ (i : ι), Nonempty (β i)] [Nontrivial (β default)] :
Equations
instance Hamming.instDecidableEqHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] :
Equations
• Hamming.instDecidableEqHamming = Fintype.decidablePiFintype
instance Hamming.instZeroHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → Zero (β i)] :
Zero ()
Equations
• Hamming.instZeroHamming = Pi.instZero
instance Hamming.instNegHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → Neg (β i)] :
Neg ()
Equations
• Hamming.instNegHamming = Pi.instNeg
instance Hamming.instAddHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → Add (β i)] :
Equations
instance Hamming.instSubHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → Sub (β i)] :
Sub ()
Equations
• Hamming.instSubHamming = Pi.instSub
instance Hamming.instSMulHamming {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [(i : ι) → SMul α (β i)] :
SMul α ()
Equations
• Hamming.instSMulHamming = Pi.instSMul
instance Hamming.instSMulWithZeroHammingInstZeroHamming {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [Zero α] [(i : ι) → Zero (β i)] [(i : ι) → SMulWithZero α (β i)] :
Equations
• Hamming.instSMulWithZeroHammingInstZeroHamming =
instance Hamming.instAddMonoidHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddMonoid (β i)] :
Equations
instance Hamming.instAddCommMonoidHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddCommMonoid (β i)] :
Equations
instance Hamming.instAddCommGroupHamming {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddCommGroup (β i)] :
Equations
instance Hamming.instModuleHammingInstAddCommMonoidHamming {ι : Type u_2} (α : Type u_5) [] (β : ιType u_4) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module α (β i)] :
Module α ()
Equations

API to/from the type synonym.

@[match_pattern]
def Hamming.toHamming {ι : Type u_2} {β : ιType u_3} :
((i : ι) → β i)

Hamming.toHamming is the identity function to the Hamming of a type.

Equations
Instances For
@[match_pattern]
def Hamming.ofHamming {ι : Type u_2} {β : ιType u_3} :
((i : ι) → β i)

Hamming.ofHamming is the identity function from the Hamming of a type.

Equations
• Hamming.ofHamming =
Instances For
@[simp]
theorem Hamming.toHamming_symm_eq {ι : Type u_2} {β : ιType u_3} :
Hamming.toHamming.symm = Hamming.ofHamming
@[simp]
theorem Hamming.ofHamming_symm_eq {ι : Type u_2} {β : ιType u_3} :
Hamming.ofHamming.symm = Hamming.toHamming
@[simp]
theorem Hamming.toHamming_ofHamming {ι : Type u_2} {β : ιType u_3} (x : ) :
Hamming.toHamming (Hamming.ofHamming x) = x
@[simp]
theorem Hamming.ofHamming_toHamming {ι : Type u_2} {β : ιType u_3} (x : (i : ι) → β i) :
Hamming.ofHamming (Hamming.toHamming x) = x
theorem Hamming.toHamming_inj {ι : Type u_2} {β : ιType u_3} {x : (i : ι) → β i} {y : (i : ι) → β i} :
Hamming.toHamming x = Hamming.toHamming y x = y
theorem Hamming.ofHamming_inj {ι : Type u_2} {β : ιType u_3} {x : } {y : } :
Hamming.ofHamming x = Hamming.ofHamming y x = y
@[simp]
theorem Hamming.toHamming_zero {ι : Type u_2} {β : ιType u_3} [(i : ι) → Zero (β i)] :
Hamming.toHamming 0 = 0
@[simp]
theorem Hamming.ofHamming_zero {ι : Type u_2} {β : ιType u_3} [(i : ι) → Zero (β i)] :
Hamming.ofHamming 0 = 0
@[simp]
theorem Hamming.toHamming_neg {ι : Type u_2} {β : ιType u_3} [(i : ι) → Neg (β i)] {x : (i : ι) → β i} :
Hamming.toHamming (-x) = -Hamming.toHamming x
@[simp]
theorem Hamming.ofHamming_neg {ι : Type u_2} {β : ιType u_3} [(i : ι) → Neg (β i)] {x : } :
Hamming.ofHamming (-x) = -Hamming.ofHamming x
@[simp]
theorem Hamming.toHamming_add {ι : Type u_2} {β : ιType u_3} [(i : ι) → Add (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
Hamming.toHamming (x + y) = Hamming.toHamming x + Hamming.toHamming y
@[simp]
theorem Hamming.ofHamming_add {ι : Type u_2} {β : ιType u_3} [(i : ι) → Add (β i)] {x : } {y : } :
Hamming.ofHamming (x + y) = Hamming.ofHamming x + Hamming.ofHamming y
@[simp]
theorem Hamming.toHamming_sub {ι : Type u_2} {β : ιType u_3} [(i : ι) → Sub (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :
Hamming.toHamming (x - y) = Hamming.toHamming x - Hamming.toHamming y
@[simp]
theorem Hamming.ofHamming_sub {ι : Type u_2} {β : ιType u_3} [(i : ι) → Sub (β i)] {x : } {y : } :
Hamming.ofHamming (x - y) = Hamming.ofHamming x - Hamming.ofHamming y
@[simp]
theorem Hamming.toHamming_smul {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [(i : ι) → SMul α (β i)] {r : α} {x : (i : ι) → β i} :
Hamming.toHamming (r x) = r Hamming.toHamming x
@[simp]
theorem Hamming.ofHamming_smul {α : Type u_1} {ι : Type u_2} {β : ιType u_3} [(i : ι) → SMul α (β i)] {r : α} {x : } :
Hamming.ofHamming (r x) = r Hamming.ofHamming x

Instances equipping Hamming with hammingNorm and hammingDist.

instance Hamming.instDistHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] :
Dist ()
Equations
• Hamming.instDistHamming = { dist := fun (x y : ) => (hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y)) }
@[simp]
theorem Hamming.dist_eq_hammingDist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : ) (y : ) :
dist x y = (hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
instance Hamming.instPseudoMetricSpaceHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Hamming.nndist_eq_hammingDist {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] (x : ) (y : ) :
nndist x y = (hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y))
Equations
• (_ : ) = (_ : )
instance Hamming.instMetricSpaceHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] :
Equations
• Hamming.instMetricSpaceHamming =
instance Hamming.instNormHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] :
Norm ()
Equations
• Hamming.instNormHamming = { norm := fun (x : ) => (hammingNorm (Hamming.ofHamming x)) }
@[simp]
theorem Hamming.norm_eq_hammingNorm {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : ) :
x = (hammingNorm (Hamming.ofHamming x))
instance Hamming.instNormedAddCommGroupHamming {ι : Type u_2} {β : ιType u_3} [] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddCommGroup (β i)] :
Equations