Relative Hamming distance and Hamming distance one

The coordinates where two functions agree and those where they differ make up all the coordinates (card_filter_eq_add_hammingDist), so the Hamming distance is the number of coordinates times one minus the density of the coordinates of agreement (hammingDist_eq_card_mul_one_sub_dens). The relative Hamming distance is the probability that the two functions differ at a uniformly random coordinate (hammingDist_div_eq_expect). A distance of at most r + s splits into one of at most r followed by one of at most s (exists_hammingDist_le_and_hammingDist_le).

Two functions are at Hamming distance one when they differ at exactly one coordinate (hammingDist_eq_one_iff); changing one coordinate of a function to a new value moves it to distance one (hammingDist_update_of_ne), and two functions at distance at most one that differ at a coordinate differ only there (update_eq_of_hammingDist_le_one). Updating two functions at the same coordinate changes their distance only through that coordinate (hammingDist_update_update). The pairs of A × B at Hamming distance one are the edges of the Hamming graph between A and B (hammingEdges); counting them from either side gives the same number (card_hammingEdges_comm, card_hammingEdges_eq_sum_card_filter).

Main definitions

• hammingEdges: the pairs of A × B at Hamming distance one.

Main results

• card_filter_eq_add_hammingDist, hammingDist_eq_card_mul_one_sub_dens: the coordinates of agreement and of disagreement.
• hammingDist_div_eq_expect: the relative Hamming distance is a probability.
• exists_hammingDist_le_and_hammingDist_le: splitting a distance.
• hammingDist_eq_one_iff: Hamming distance one.
• update_eq_of_hammingDist_le_one, update_not_eq_of_hammingDist_le_one: functions at distance at most one differ at most at one coordinate.
• hammingDist_update_update: updating two functions at the same coordinate.
• card_hammingEdges_eq_sum_card_filter: counting the edges of the Hamming graph.

Relative Hamming distance

theorem card_filter_eq_add_hammingDist {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i) : {i : ι | x i = y i}.card + hammingDist x y = Fintype.card ι

The coordinates where two functions agree and those where they differ make up all the coordinates.

theorem hammingDist_eq_card_mul_one_sub_dens {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {𝕜 : Type u_3} [Field 𝕜] [CharZero 𝕜] (x y : (i : ι) → β i) : ↑(hammingDist x y) = ↑(Fintype.card ι) * (1 - ↑{i : ι | x i = y i}.dens)

The Hamming distance is the number of coordinates times one minus the density of the coordinates where the functions agree.

theorem hammingDist_div_eq_expect {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {𝕜 : Type u_3} [Semifield 𝕜] [CharZero 𝕜] (x y : (i : ι) → β i) : ↑(hammingDist x y) / ↑(Fintype.card ι) = Finset.univ.expect fun (i : ι) => if x i ≠ y i then 1 else 0

The relative Hamming distance is a probability: that of the two functions differing at a uniformly random coordinate.

theorem exists_hammingDist_le_and_hammingDist_le {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i} {r s : ℕ} (h : hammingDist x y ≤ r + s) : ∃ (z : (i : ι) → β i), hammingDist x z ≤ r ∧ hammingDist z y ≤ s

Splitting a distance: between two functions at Hamming distance at most r + s lies a function at distance at most r from the first and at most s from the second. It takes the values of the second on at most r of the coordinates where the two differ, and the values of the first elsewhere.

Hamming distance one

theorem hammingDist_eq_one_iff {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i} : hammingDist x y = 1 ↔ ∃ (i : ι), x i ≠ y i ∧ ∀ (j : ι), j ≠ i → x j = y j

Two functions are at Hamming distance one when they differ at exactly one coordinate.

theorem hammingDist_update_of_ne {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] [DecidableEq ι] {x : (i : ι) → β i} {i : ι} {v : β i} (h : x i ≠ v) : hammingDist x (Function.update x i v) = 1

Changing one coordinate to a new value moves to Hamming distance one.

theorem update_eq_of_hammingDist_le_one {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] [DecidableEq ι] {x y : (i : ι) → β i} (h : hammingDist x y ≤ 1) {i : ι} (hi : x i ≠ y i) : Function.update x i (y i) = y

Two functions at Hamming distance at most one that differ at i differ only at i: changing the i-th coordinate of the first to that of the second gives the second.

theorem update_not_eq_of_hammingDist_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {x y : ι → Bool} (h : hammingDist x y ≤ 1) {i : ι} (hi : x i ≠ y i) : (Function.update x i !x i) = y

Two Boolean functions at Hamming distance at most one that differ at i differ only at i: the second is the first with its i-th bit flipped.

theorem hammingDist_update_update {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] [DecidableEq ι] (x y : (i : ι) → β i) (i : ι) (a b : β i) : (hammingDist (Function.update x i a) (Function.update y i b) + if x i ≠ y i then 1 else 0) = hammingDist x y + if a ≠ b then 1 else 0

Updating two functions at the same coordinate changes their Hamming distance only through that coordinate.

def hammingEdges {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (A B : Finset ((i : ι) → β i)) : Finset (((i : ι) → β i) × ((i : ι) → β i))

The pairs of A × B at Hamming distance one: the edges of the Hamming graph between A and B.

@[simp]

theorem mem_hammingEdges {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {A B : Finset ((i : ι) → β i)} {e : ((i : ι) → β i) × ((i : ι) → β i)} : e ∈ hammingEdges A B ↔ e.1 ∈ A ∧ e.2 ∈ B ∧ hammingDist e.1 e.2 = 1

A pair is an edge between A and B exactly when its first entry is in A, its second entry is in B, and they are at Hamming distance one.

theorem card_hammingEdges_comm {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (A B : Finset ((i : ι) → β i)) : (hammingEdges A B).card = (hammingEdges B A).card

There are as many edges from A to B as from B to A.

theorem card_hammingEdges_filter_add_card_hammingEdges_filter_not {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] {A B : Finset ((i : ι) → β i)} (p : ((i : ι) → β i) → Prop) [DecidablePred p] : (hammingEdges A (Finset.filter p B)).card + (hammingEdges A ({b ∈ B | ¬p b})).card = (hammingEdges A B).card

Splitting B splits the edges.

theorem card_hammingEdges_eq_sum_card_filter {ι : Type u_1} [Fintype ι] {β : ι → Type u_2} [(i : ι) → DecidableEq (β i)] (A B : Finset ((i : ι) → β i)) : (hammingEdges A B).card = ∑ a ∈ A, {b ∈ B | hammingDist a b = 1}.card

The number of edges is the sum over A of the numbers of neighbors in B.