Documentation

MIPRE.Tailored.Sofic.Hamming

The normalized Hamming distance on permutations #

Paper I (arXiv:2408.00110), I:1351–1370: the normalized Hamming distance d_H(a, b) = P_p[a p ≠ b p] between two permutations of one finite set. We work with the number diffCard a b of points where a and b differ, and dH a b = diffCard a b / |α|.

The facts used by the robustness claim and the stability claims: the triangle inequality, the product bound d(a b, a' b') ≤ d(a, a') + d(b, b') (the paper's "iterated triangle inequality"), inversion invariance d(a⁻¹, b⁻¹) = d(a, b), and the count of the points a commutator moves.

source
def MIPRE.Tailored.Sofic.diffCard {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
ℕ

The number of points at which two permutations differ.

Equations
Instances For
    source
    noncomputable def MIPRE.Tailored.Sofic.dH {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
    ℝ

    The normalized Hamming distance (I:1356): the fraction of points at which two permutations differ.

    Equations
    Instances For
      source
      @[simp]
      theorem MIPRE.Tailored.Sofic.perm_inv_apply_self' {α : Type u_1} (a : Equiv.Perm α) (x : α) :
      a⁻¹ (a x) = x
      source
      @[simp]
      theorem MIPRE.Tailored.Sofic.perm_apply_inv_self' {α : Type u_1} (a : Equiv.Perm α) (x : α) :
      a (a⁻¹ x) = x
      source
      theorem MIPRE.Tailored.Sofic.card_filter_comp_perm {α : Type u_1} [Fintype α] (e : Equiv.Perm α) (P : α → Prop) [DecidablePred P] :
      {p : α | P (e p)}.card = (Finset.filter P Finset.univ).card

      Composing a predicate with a permutation does not change how many points satisfy it.

      source
      theorem MIPRE.Tailored.Sofic.diffCard_comm {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      diffCard a b = diffCard b a
      source
      @[simp]
      theorem MIPRE.Tailored.Sofic.diffCard_self {α : Type u_1} [Fintype α] [DecidableEq α] (a : Equiv.Perm α) :
      diffCard a a = 0
      source
      theorem MIPRE.Tailored.Sofic.diffCard_le_card {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      diffCard a b ≤ Fintype.card α
      source
      theorem MIPRE.Tailored.Sofic.diffCard_triangle {α : Type u_1} [Fintype α] [DecidableEq α] (a b c : Equiv.Perm α) :
      diffCard a c ≤ diffCard a b + diffCard b c

      The triangle inequality.

      source
      theorem MIPRE.Tailored.Sofic.diffCard_mul {α : Type u_1} [Fintype α] [DecidableEq α] (a a' b b' : Equiv.Perm α) :
      diffCard (a * b) (a' * b') ≤ diffCard a a' + diffCard b b'

      The product bound: d(a b, a' b') ≤ d(a, a') + d(b, b').

      source
      theorem MIPRE.Tailored.Sofic.diffCard_inv {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      diffCard a⁻¹ b⁻¹ = diffCard a b

      Inversion does not change the distance.

      source
      theorem MIPRE.Tailored.Sofic.card_commutator_moves {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      {q : α | (a * b * a⁻¹ * b⁻¹) q ≠ q}.card = {r : α | a (b r) ≠ b (a r)}.card

      The points a commutator a b a⁻¹ b⁻¹ moves are as many as those at which a and b do not commute.

      source
      theorem MIPRE.Tailored.Sofic.dH_nonneg {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      0 ≤ dH a b
      source
      theorem MIPRE.Tailored.Sofic.dH_le_one {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      dH a b ≤ 1
      source
      theorem MIPRE.Tailored.Sofic.dH_comm {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      dH a b = dH b a
      source
      theorem MIPRE.Tailored.Sofic.dH_triangle {α : Type u_1} [Fintype α] [DecidableEq α] (a b c : Equiv.Perm α) :
      dH a c ≤ dH a b + dH b c
      source
      theorem MIPRE.Tailored.Sofic.dH_mul {α : Type u_1} [Fintype α] [DecidableEq α] (a a' b b' : Equiv.Perm α) :
      dH (a * b) (a' * b') ≤ dH a a' + dH b b'
      source
      theorem MIPRE.Tailored.Sofic.dH_inv {α : Type u_1} [Fintype α] [DecidableEq α] (a b : Equiv.Perm α) :
      dH a⁻¹ b⁻¹ = dH a b