mathlib3 documentation

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 #

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) :

Corresponds to dist_self.

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

Corresponds to dist_nonneg.

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

Corresponds to dist_comm.

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

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) :

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) :

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} :
hamming_dist x 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} :
hamming_dist x 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 = hamming_dist x 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} :

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 < hamming_dist x 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} :
hamming_dist x 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)) hamming_dist x 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)) = hamming_dist x y
theorem hamming_dist_smul_le_hamming_dist {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_smul α (β i)] {k : α} {x y : Π (i : ι), β i} :
theorem hamming_dist_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [fintype ι] [Π (i : ι), decidable_eq (β i)] [Π (i : ι), has_smul α (β i)] {k : α} {x y : Π (i : ι), β i} (hk : (i : ι), is_smul_regular (β i) k) :

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} :

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} :

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} :

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} :
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)) hamming_norm x
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)) = hamming_norm x
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 : ι), smul_with_zero α (β 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 : ι), smul_with_zero α (β 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) :

Corresponds to dist_eq_norm.

The hamming type synonym #

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)] [nontrivial inhabited.default)] :
@[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 : ι), has_smul α (β i)] :
Equations
@[protected, instance]
def hamming.smul_with_zero {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [has_zero α] [Π (i : ι), has_zero (β i)] [Π (i : ι), smul_with_zero α (β i)] :
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 : ι), module α (β i)] :
module α (hamming β)
Equations

API to/from the type synonym.

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

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

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

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

Equations
@[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 : ι), has_smul α (β i)] {r : α} {x : Π (i : ι), β i} :
@[simp]
theorem hamming.of_hamming_smul {α : Type u_1} {ι : Type u_2} {β : ι Type u_3} [Π (i : ι), has_smul α (β 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.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 β) :
@[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 β) :