Documentation

Mathlib.InformationTheory.Hamming

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 #

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
Instances For
    @[simp]
    theorem hammingDist_self {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) :

    Corresponds to dist_self.

    theorem hammingDist_nonneg {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] {x : (i : ι) → β i} {y : (i : ι) → β i} :

    Corresponds to dist_nonneg.

    theorem hammingDist_comm {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) :

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

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

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

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

    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} :
    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} :
    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
    Instances For
      @[simp]
      theorem hammingDist_zero_right {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] (x : (i : ι) → β i) :

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

      Corresponds to norm_nonneg.

      @[simp]
      theorem hammingNorm_zero {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] :

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

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

      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} :
      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} :
      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) :
      theorem hammingDist_eq_hammingNorm {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → AddGroup (β i)] (x : (i : ι) → β i) (y : (i : ι) → β i) :

      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
      Instances For

        Instances inherited from normal Pi types.

        instance Hamming.instInhabited {ι : Type u_2} {β : ιType u_3} [(i : ι) → Inhabited (β i)] :
        Equations
        • Hamming.instInhabited = { default := fun (x : ι) => default }
        instance Hamming.instFintypeOfDecidableEq {ι : Type u_2} {β : ιType u_3} [DecidableEq ι] [Fintype ι] [(i : ι) → Fintype (β i)] :
        Equations
        • Hamming.instFintypeOfDecidableEq = Pi.fintype
        instance Hamming.instNontrivialOfNonemptyOfDefault {ι : Type u_2} {β : ιType u_3} [Inhabited ι] [∀ (i : ι), Nonempty (β i)] [Nontrivial (β default)] :
        Equations
        • =
        instance Hamming.instDecidableEqOfFintype {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] :
        Equations
        • Hamming.instDecidableEqOfFintype = Fintype.decidablePiFintype
        instance Hamming.instZero {ι : Type u_2} {β : ιType u_3} [(i : ι) → Zero (β i)] :
        Equations
        • Hamming.instZero = Pi.instZero
        instance Hamming.instNeg {ι : Type u_2} {β : ιType u_3} [(i : ι) → Neg (β i)] :
        Equations
        • Hamming.instNeg = Pi.instNeg
        instance Hamming.instAdd {ι : Type u_2} {β : ιType u_3} [(i : ι) → Add (β i)] :
        Equations
        • Hamming.instAdd = Pi.instAdd
        instance Hamming.instSub {ι : Type u_2} {β : ιType u_3} [(i : ι) → Sub (β i)] :
        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)] :
        Equations
        instance Hamming.instAddMonoid {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddMonoid (β i)] :
        Equations
        • Hamming.instAddMonoid = Pi.addMonoid
        instance Hamming.instAddCommMonoid {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddCommMonoid (β i)] :
        Equations
        • Hamming.instAddCommMonoid = Pi.addCommMonoid
        instance Hamming.instAddCommGroup {ι : Type u_2} {β : ιType u_3} [(i : ι) → AddCommGroup (β i)] :
        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

        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
        Instances For
          @[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
          Instances For
            @[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)] :
            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)] :
            Equations
            @[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)] :
            Equations
            • =
            instance Hamming.instMetricSpace {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] :
            Equations
            instance Hamming.instNormOfZero {ι : Type u_2} {β : ιType u_3} [Fintype ι] [(i : ι) → DecidableEq (β i)] [(i : ι) → Zero (β i)] :
            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)] :
            Equations
            @[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))