# mathlib3documentation

information_theory.hamming

# Hamming spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• hamming_dist x y: the Hamming distance between x and y, the number of entries which differ.
• hamming_norm 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.to_hamming, hamming.of_hamming: functions for casting between hamming β and Π i, β i.
• hamming.normed_add_comm_group: the Hamming norm forms a normed group on hamming β.
def hamming_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : Π (i : ι), β i) :

The Hamming distance function to the naturals.

Equations
@[simp]
theorem hamming_dist_self {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x : Π (i : ι), β i) :
x = 0

Corresponds to dist_self.

theorem hamming_dist_nonneg {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
0 y

Corresponds to dist_nonneg.

theorem hamming_dist_comm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : Π (i : ι), β i) :
y = x

Corresponds to dist_comm.

theorem hamming_dist_triangle {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :
z y + z

Corresponds to dist_triangle.

theorem hamming_dist_triangle_left {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :
y x + y

Corresponds to dist_triangle_left.

theorem hamming_dist_triangle_right {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y z : Π (i : ι), β i) :
y z + z

Corresponds to dist_triangle_right.

theorem swap_hamming_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :

Corresponds to swap_dist.

theorem eq_of_hamming_dist_eq_zero {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
y = 0 x = y

Corresponds to eq_of_dist_eq_zero.

@[simp]
theorem hamming_dist_eq_zero {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
y = 0 x = y

Corresponds to dist_eq_zero.

@[simp]
theorem hamming_zero_eq_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
0 = y x = y

Corresponds to zero_eq_dist.

theorem hamming_dist_ne_zero {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
y 0 x y

Corresponds to dist_ne_zero.

@[simp]
theorem hamming_dist_pos {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
0 < y x y

Corresponds to dist_pos.

@[simp]
theorem hamming_dist_lt_one {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
y < 1 x = y
theorem hamming_dist_le_card_fintype {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {x y : Π (i : ι), β i} :
theorem hamming_dist_comp_le_hamming_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι Type u_4} [Π (i : ι), decidable_eq (γ i)] (f : Π (i : ι), γ i β i) {x y : Π (i : ι), γ i} :
hamming_dist (λ (i : ι), f i (x i)) (λ (i : ι), f i (y i)) y
theorem hamming_dist_comp {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι Type u_4} [Π (i : ι), decidable_eq (γ i)] (f : Π (i : ι), γ i β i) {x y : Π (i : ι), γ i} (hf : (i : ι), function.injective (f i)) :
hamming_dist (λ (i : ι), f i (x i)) (λ (i : ι), f i (y i)) = y
theorem hamming_dist_smul_le_hamming_dist {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), (β i)] {k : α} {x y : Π (i : ι), β i} :
hamming_dist (k x) (k y) y
theorem hamming_dist_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), (β i)] {k : α} {x y : Π (i : ι), β i} (hk : (i : ι), is_smul_regular (β i) k) :
hamming_dist (k x) (k y) = y

Corresponds to dist_smul with the discrete norm on α.

def hamming_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : Π (i : ι), β i) :

The Hamming weight function to the naturals.

Equations
@[simp]
theorem hamming_dist_zero_right {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : Π (i : ι), β i) :

Corresponds to dist_zero_right.

@[simp]
theorem hamming_dist_zero_left {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :

Corresponds to dist_zero_left.

@[simp]
theorem hamming_norm_nonneg {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :

Corresponds to norm_nonneg.

@[simp]
theorem hamming_norm_zero {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :

Corresponds to norm_zero.

@[simp]
theorem hamming_norm_eq_zero {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :
x = 0

Corresponds to norm_eq_zero.

theorem hamming_norm_ne_zero_iff {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :
x 0

Corresponds to norm_ne_zero_iff.

@[simp]
theorem hamming_norm_pos_iff {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :
x 0

Corresponds to norm_pos_iff.

@[simp]
theorem hamming_norm_lt_one {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :
x = 0
theorem hamming_norm_le_card_fintype {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] {x : Π (i : ι), β i} :
theorem hamming_norm_comp_le_hamming_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι Type u_4} [Π (i : ι), decidable_eq (γ i)] [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (γ i)] (f : Π (i : ι), γ i β i) {x : Π (i : ι), γ i} (hf : (i : ι), f i 0 = 0) :
hamming_norm (λ (i : ι), f i (x i))
theorem hamming_norm_comp {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] {γ : ι Type u_4} [Π (i : ι), decidable_eq (γ i)] [Π (i : ι), has_zero (β i)] [Π (i : ι), has_zero (γ i)] (f : Π (i : ι), γ i β i) {x : Π (i : ι), γ i} (hf₁ : (i : ι), function.injective (f i)) (hf₂ : (i : ι), f i 0 = 0) :
hamming_norm (λ (i : ι), f i (x i)) =
theorem hamming_norm_smul_le_hamming_norm {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] [has_zero α] [Π (i : ι), (β i)] {k : α} {x : Π (i : ι), β i} :
theorem hamming_norm_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] [has_zero α] [Π (i : ι), (β i)] {k : α} (hk : (i : ι), is_smul_regular (β i) k) (x : Π (i : ι), β i) :
theorem hamming_dist_eq_hamming_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_group (β i)] (x y : Π (i : ι), β i) :
y = hamming_norm (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.normed_add_comm_group which uses the sup norm.

Equations
• = Π (i : ι), β i
Instances for hamming

Instances inherited from normal Pi types.

@[protected, instance]
def hamming.inhabited {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), inhabited (β i)] :
Equations
@[protected, instance]
def hamming.fintype {ι : Type u_2} {β : ι Type u_3} [decidable_eq ι] [fintype ι] [Π (i : ι), fintype (β i)] :
Equations
@[protected, instance]
def hamming.nontrivial {ι : Type u_2} {β : ι Type u_3} [inhabited ι] [ (i : ι), nonempty (β i)]  :
@[protected, instance]
def hamming.decidable_eq {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :
Equations
@[protected, instance]
def hamming.has_zero {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_zero (β i)] :
Equations
@[protected, instance]
def hamming.has_neg {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_neg (β i)] :
Equations
@[protected, instance]
def hamming.has_add {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_add (β i)] :
Equations
@[protected, instance]
def hamming.has_sub {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_sub (β i)] :
Equations
@[protected, instance]
def hamming.has_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), (β i)] :
(hamming β)
Equations
@[protected, instance]
def hamming.smul_with_zero {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [has_zero α] [Π (i : ι), has_zero (β i)] [Π (i : ι), (β i)] :
(hamming β)
Equations
@[protected, instance]
def hamming.add_monoid {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), add_monoid (β i)] :
Equations
@[protected, instance]
def hamming.add_comm_monoid {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), add_comm_monoid (β i)] :
Equations
@[protected, instance]
def hamming.add_comm_group {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), add_comm_group (β i)] :
Equations
@[protected, instance]
def hamming.module {ι : Type u_2} (α : Type u_1) [semiring α] (β : ι Type u_3) [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), (β i)] :
(hamming β)
Equations
• = (λ (i : ι), β i) α

API to/from the type synonym.

def hamming.to_hamming {ι : Type u_2} {β : ι Type u_3} :
(Π (i : ι), β i)

to_hamming is the identity function to the hamming of a type.

Equations
def hamming.of_hamming {ι : Type u_2} {β : ι Type u_3} :
Π (i : ι), β i

of_hamming is the identity function from the hamming of a type.

Equations
@[simp]
theorem hamming.to_hamming_symm_eq {ι : Type u_2} {β : ι Type u_3} :
@[simp]
theorem hamming.of_hamming_symm_eq {ι : Type u_2} {β : ι Type u_3} :
@[simp]
theorem hamming.to_hamming_of_hamming {ι : Type u_2} {β : ι Type u_3} (x : hamming β) :
@[simp]
theorem hamming.of_hamming_to_hamming {ι : Type u_2} {β : ι Type u_3} (x : Π (i : ι), β i) :
@[simp]
theorem hamming.to_hamming_inj {ι : Type u_2} {β : ι Type u_3} {x y : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_inj {ι : Type u_2} {β : ι Type u_3} {x y : hamming β} :
@[simp]
theorem hamming.to_hamming_zero {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_zero (β i)] :
@[simp]
theorem hamming.of_hamming_zero {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_zero (β i)] :
@[simp]
theorem hamming.to_hamming_neg {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_neg (β i)] {x : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_neg {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_neg (β i)] {x : hamming β} :
@[simp]
theorem hamming.to_hamming_add {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_add (β i)] {x y : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_add {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_add (β i)] {x y : hamming β} :
@[simp]
theorem hamming.to_hamming_sub {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_sub (β i)] {x y : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_sub {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_sub (β i)] {x y : hamming β} :
@[simp]
theorem hamming.to_hamming_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), (β i)] {r : α} {x : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), (β i)] {r : α} {x : hamming β} :

Instances equipping hamming with hamming_norm and hamming_dist.

@[protected, instance]
def hamming.has_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :
Equations
@[simp]
theorem hamming.dist_eq_hamming_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : hamming β) :
@[protected, instance]
def hamming.pseudo_metric_space {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :
Equations
@[simp]
theorem hamming.nndist_eq_hamming_dist {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] (x y : hamming β) :
@[protected, instance]
def hamming.metric_space {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] :
Equations
@[protected, instance]
def hamming.has_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] :
Equations
@[simp]
theorem hamming.norm_eq_hamming_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_zero (β i)] (x : hamming β) :
@[protected, instance]
def hamming.seminormed_add_comm_group {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] :
Equations
@[simp]
theorem hamming.nnnorm_eq_hamming_norm {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] (x : hamming β) :
@[protected, instance]
def hamming.normed_add_comm_group {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), add_comm_group (β i)] :
Equations