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 : (i : ι) → β i) (y : (i : ι) → β i) : ℕ

The Hamming distance function to the naturals.

Equations

• hammingDist x y = (Finset.filter (fun (i : ι) => x i ≠ y i) Finset.univ).card

@[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 : (i : ι) → β i} {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 : (i : ι) → β i) (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 : (i : ι) → β i) (y : (i : ι) → β i) (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 : (i : ι) → β i) (y : (i : ι) → β i) (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 : (i : ι) → β i) (y : (i : ι) → β i) (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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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 : (i : ι) → γ i} {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 : (i : ι) → γ i} {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 : (i : ι) → β i} {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 : (i : ι) → β i} {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.

Equations

• hammingNorm x = (Finset.filter (fun (i : ι) => x i ≠ 0) Finset.univ).card

@[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 : (i : ι) → β i) (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.

Equations

• Hamming β = ((i : ι) → β i)

Instances inherited from normal Pi types.

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

Equations

• Hamming.instInhabited = { default := fun (x : ι) => default }

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

Equations

• Hamming.instFintypeOfDecidableEq = Pi.fintype

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

Equations

• ⋯ = ⋯

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

Equations

• Hamming.instDecidableEqOfFintype = Fintype.decidablePiFintype

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

Equations

• Hamming.instZero = Pi.instZero

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

Equations

• Hamming.instNeg = Pi.instNeg

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

Equations

• Hamming.instAdd = Pi.instAdd

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

Equations

• Hamming.instSub = Pi.instSub

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

Equations

• Hamming.instSMul = Pi.instSMul

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

Equations

• Hamming.instSMulWithZero = Pi.smulWithZero α

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

Equations

• Hamming.instAddMonoid = Pi.addMonoid

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

Equations

• Hamming.instAddCommMonoid = Pi.addCommMonoid

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

Equations

• Hamming.instAddCommGroup = Pi.addCommGroup

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

Equations

• Hamming.instModule α β = Pi.module ι β α

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.

Equations

• Hamming.toHamming = Equiv.refl ((i : ι) → β i)

@[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.

Equations

• Hamming.ofHamming = Equiv.refl (Hamming β)

@[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 β) : 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 : Hamming β} {y : Hamming β} : 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 β} : 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 : Hamming β} {y : Hamming β} : 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 : Hamming β} {y : Hamming β} : 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 β} : Hamming.ofHamming (r • x) = r • Hamming.ofHamming x

Instances equipping Hamming with hammingNorm and hammingDist.

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

Equations

• Hamming.instDist = { dist := fun (x y : Hamming β) => ↑(hammingDist (Hamming.ofHamming x) (Hamming.ofHamming y)) }

@[simp]

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

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

Equations

• Hamming.instPseudoMetricSpace = PseudoMetricSpace.mk ⋯ ⋯ ⋯ (fun (x y : Hamming β) => ↑⟨dist x y, ⋯⟩) ⋯ ⊥ ⋯ { cobounded' := ⊥, le_cofinite' := ⋯ } ⋯

@[simp]

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

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

Equations

• ⋯ = ⋯

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

Equations

• Hamming.instMetricSpace = MetricSpace.ofT0PseudoMetricSpace (Hamming β)

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

Equations

• Hamming.instNormOfZero = { norm := fun (x : Hamming β) => ↑(hammingNorm (Hamming.ofHamming x)) }

@[simp]

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

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

Equations

• Hamming.instNormedAddCommGroupOfAddCommGroup = NormedAddCommGroup.mk ⋯

@[simp]

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