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} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i) : ℕ

The Hamming distance function to the naturals.

@[simp]

theorem hammingDist_self {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) : hammingDist x x = 0

Corresponds to dist_self.

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

Corresponds to dist_nonneg.

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

Corresponds to dist_comm.

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

Corresponds to dist_triangle.

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

Corresponds to dist_triangle_left.

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

Corresponds to dist_triangle_right.

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

Corresponds to swap_dist.

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

Corresponds to eq_of_dist_eq_zero.

@[simp]

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

Corresponds to dist_eq_zero.

@[simp]

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

Corresponds to zero_eq_dist.

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

Corresponds to dist_ne_zero.

@[simp]

theorem hammingDist_pos {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i} : 0 < hammingDist x y ↔ x ≠ y

Corresponds to dist_pos.

theorem hammingDist_lt_one {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i} : hammingDist x y < 1 ↔ x = y

theorem hammingDist_le_card_fintype {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i} : hammingDist x y ≤ Fintype.card ι

theorem hammingDist_comp_le_hammingDist {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {γ : ι → Type u_4} [(i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ i → β i) {x y : (i : ι) → γ i} : (hammingDist (fun (i : ι) => f i (x i)) fun (i : ι) => f i (y i)) ≤ hammingDist x y

theorem hammingDist_comp {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {γ : ι → Type u_4} [(i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ i → β i) {x y : (i : ι) → γ i} (hf : ∀ (i : ι), Function.Injective (f i)) : (hammingDist (fun (i : ι) => f i (x i)) fun (i : ι) => f i (y i)) = hammingDist x y

theorem hammingDist_smul_le_hammingDist {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul α (β i)] {k : α} {x y : (i : ι) → β i} : hammingDist (k • x) (k • y) ≤ hammingDist x y

theorem hammingDist_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → SMul α (β i)] {k : α} {x y : (i : ι) → β i} (hk : ∀ (i : ι), IsSMulRegular (β i) k) : hammingDist (k • x) (k • y) = hammingDist x y

Corresponds to dist_smul with the discrete norm on α.

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

The Hamming weight function to the naturals.

@[simp]

theorem hammingDist_zero_right {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : (i : ι) → β i) : hammingDist x 0 = hammingNorm x

Corresponds to dist_zero_right.

@[simp]

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

Corresponds to dist_zero_left.

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

Corresponds to norm_nonneg.

@[simp]

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

Corresponds to norm_zero.

@[simp]

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

Corresponds to norm_eq_zero.

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

Corresponds to norm_ne_zero_iff.

@[simp]

theorem hammingNorm_pos_iff {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} : 0 < hammingNorm x ↔ x ≠ 0

Corresponds to norm_pos_iff.

theorem hammingNorm_lt_one {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} : hammingNorm x < 1 ↔ x = 0

theorem hammingNorm_le_card_fintype {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] {x : (i : ι) → β i} : hammingNorm x ≤ Fintype.card ι

theorem hammingNorm_comp_le_hammingNorm {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(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)) ≤ hammingNorm x

theorem hammingNorm_comp {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(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)) = hammingNorm x

theorem hammingNorm_smul_le_hammingNorm {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] [Zero α] [(i : ι) → SMulWithZero α (β i)] {k : α} {x : (i : ι) → β i} : hammingNorm (k • x) ≤ hammingNorm x

theorem hammingNorm_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] [Zero α] [(i : ι) → SMulWithZero α (β i)] {k : α} (hk : ∀ (i : ι), IsSMulRegular (β i) k) (x : (i : ι) → β i) : hammingNorm (k • x) = hammingNorm x

theorem hammingDist_eq_hammingNorm {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] (x y : (i : ι) → β i) : hammingDist x y = 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.

Instances inherited from normal Pi types.

instance Hamming.instInhabited {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Inhabited (β i)] : Inhabited (Hamming β)

instance Hamming.instFintypeOfDecidableEq {ι : Type u_2} {β : ι → Type u_3} [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (β i)] : Fintype (Hamming β)

instance Hamming.instNontrivialOfNonemptyOfDefault {ι : Type u_2} {β : ι → Type u_3} [Inhabited ι] [∀ (i : ι), Nonempty (β i)] [Nontrivial (β default)] : Nontrivial (Hamming β)

instance Hamming.instDecidableEqOfFintype {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : DecidableEq (Hamming β)

instance Hamming.instZero {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Zero (β i)] : Zero (Hamming β)

instance Hamming.instNeg {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Neg (β i)] : Neg (Hamming β)

instance Hamming.instAdd {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Add (β i)] : Add (Hamming β)

instance Hamming.instSub {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Sub (β i)] : Sub (Hamming β)

instance Hamming.instSMul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → SMul α (β i)] : SMul α (Hamming β)

instance Hamming.instSMulWithZero {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [Zero α] [(i : ι) → Zero (β i)] [(i : ι) → SMulWithZero α (β i)] : SMulWithZero α (Hamming β)

instance Hamming.instAddMonoid {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddMonoid (β i)] : AddMonoid (Hamming β)

instance Hamming.instAddGroup {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddGroup (β i)] : AddGroup (Hamming β)

instance Hamming.instAddCommMonoid {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddCommMonoid (β i)] : AddCommMonoid (Hamming β)

instance Hamming.instAddCommGroup {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → AddCommGroup (β i)] : AddCommGroup (Hamming β)

instance Hamming.instModule {ι : Type u_2} (α : Type u_5) [Semiring α] (β : ι → Type u_4) [(i : ι) → AddCommMonoid (β i)] [(i : ι) → Module α (β i)] : Module α (Hamming β)

API to/from the type synonym.

@[match_pattern]

def Hamming.toHamming {ι : Type u_2} {β : ι → Type u_3} : ((i : ι) → β i) ≃ Hamming β

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

@[match_pattern]

def Hamming.ofHamming {ι : Type u_2} {β : ι → Type u_3} : Hamming β ≃ ((i : ι) → β i)

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

@[simp]

theorem Hamming.toHamming_symm_eq {ι : Type u_2} {β : ι → Type u_3} : toHamming.symm = ofHamming

@[simp]

theorem Hamming.ofHamming_symm_eq {ι : Type u_2} {β : ι → Type u_3} : ofHamming.symm = toHamming

@[simp]

theorem Hamming.toHamming_ofHamming {ι : Type u_2} {β : ι → Type u_3} (x : Hamming β) : toHamming (ofHamming x) = x

@[simp]

theorem Hamming.ofHamming_toHamming {ι : Type u_2} {β : ι → Type u_3} (x : (i : ι) → β i) : ofHamming (toHamming x) = x

theorem Hamming.toHamming_inj {ι : Type u_2} {β : ι → Type u_3} {x y : (i : ι) → β i} : toHamming x = toHamming y ↔ x = y

theorem Hamming.ofHamming_inj {ι : Type u_2} {β : ι → Type u_3} {x y : Hamming β} : ofHamming x = ofHamming y ↔ x = y

@[simp]

theorem Hamming.toHamming_zero {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Zero (β i)] : toHamming 0 = 0

@[simp]

theorem Hamming.ofHamming_zero {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Zero (β i)] : ofHamming 0 = 0

@[simp]

theorem Hamming.toHamming_neg {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Neg (β i)] {x : (i : ι) → β i} : toHamming (-x) = -toHamming x

@[simp]

theorem Hamming.ofHamming_neg {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Neg (β i)] {x : Hamming β} : ofHamming (-x) = -ofHamming x

@[simp]

theorem Hamming.toHamming_add {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Add (β i)] {x y : (i : ι) → β i} : toHamming (x + y) = toHamming x + toHamming y

@[simp]

theorem Hamming.ofHamming_add {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Add (β i)] {x y : Hamming β} : ofHamming (x + y) = ofHamming x + ofHamming y

@[simp]

theorem Hamming.toHamming_sub {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Sub (β i)] {x y : (i : ι) → β i} : toHamming (x - y) = toHamming x - toHamming y

@[simp]

theorem Hamming.ofHamming_sub {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → Sub (β i)] {x y : Hamming β} : ofHamming (x - y) = ofHamming x - ofHamming y

@[simp]

theorem Hamming.toHamming_smul {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [(i : ι) → SMul α (β i)] {r : α} {x : (i : ι) → β i} : toHamming (r • x) = r • 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 • ofHamming x

Instances equipping Hamming with hammingNorm and hammingDist.

instance Hamming.instDist {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : Dist (Hamming β)

@[simp]

theorem Hamming.dist_eq_hammingDist {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x y : Hamming β) : dist x y = ↑(hammingDist (ofHamming x) (ofHamming y))

instance Hamming.instPseudoMetricSpace {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : PseudoMetricSpace (Hamming β)

@[simp]

theorem Hamming.nndist_eq_hammingDist {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x y : Hamming β) : nndist x y = ↑(hammingDist (ofHamming x) (ofHamming y))

instance Hamming.instDiscreteTopology {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : DiscreteTopology (Hamming β)

instance Hamming.instMetricSpace {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] : MetricSpace (Hamming β)

instance Hamming.instNormOfZero {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] : Norm (Hamming β)

@[simp]

theorem Hamming.norm_eq_hammingNorm {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : Hamming β) : ‖x‖ = ↑(hammingNorm (ofHamming x))

instance Hamming.instNormedAddGroupOfAddGroup {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] : NormedAddGroup (Hamming β)

instance Hamming.instNormedAddCommGroupOfAddCommGroup {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddCommGroup (β i)] : NormedAddCommGroup (Hamming β)

@[simp]

theorem Hamming.nnnorm_eq_hammingNorm {ι : Type u_2} {β : ι → Type u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] (x : Hamming β) : ‖x‖₊ = ↑(hammingNorm (ofHamming x))