hammingDist_ne_zero
theorem hammingDist_ne_zero :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
hammingDist x y ≠ 0 ↔ x ≠ y
This theorem, `hammingDist_ne_zero`, establishes a property of the Hamming distance between two functions `x` and `y` (where the function domain is a finite type `ι` and the codomain is decided by another function `β`). Specifically, it states that the Hamming distance between `x` and `y` is non-zero if and only if `x` and `y` are not the same function. This Hamming distance is calculated as the cardinality of the set of indices where `x` and `y` disagree. The equality of functions is decidable, meaning that we can always decide whether two functions are equal or not.
More concisely: The Hamming distance between two functions x and y, where the domain is finite type ι and codomain is decided by β, is non-zero if and only if x and y are not equal.
|
hammingDist_triangle_left
theorem hammingDist_triangle_left :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
(x y z : (i : ι) → β i), hammingDist x y ≤ hammingDist z x + hammingDist z y
This theorem, known as `hammingDist_triangle_left`, is a variation of the triangle inequality for the Hamming distance. For any types `ι` and `β` (where `β` is a function from `ι` to some type), assuming `ι` is a finite type and for every `i` in `ι`, the equality of `β i` is decidable, the theorem states that for any three functions `x`, `y`, and `z` from `ι` to `β i`, the Hamming distance between `x` and `y` is always less than or equal to the sum of the Hamming distances between `z` and `x`, and `z` and `y`. The Hamming distance between two functions is defined as the number of points at which these functions give different results.
More concisely: For finite types `ι` and functions `β : ι →* X` where the equality of `β i` is decidable, the Hamming distance between any three functions `x`, `y`, and `z` from `ι` to `β i` satisfies the triangle inequality: `hammingDist x y ≤ hammingDist x z + hammingDist z y`.
|
hammingNorm_zero
theorem hammingNorm_zero :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)], hammingNorm 0 = 0
The theorem `hammingNorm_zero` states that for any type `ι`, any function `β` from `ι` to another type, given that `ι` is a finite type and for any `i` in `ι`, `β i` has a decidable equality and a zero element, the hamming norm of the zero function (i.e., a function that maps every element to zero) is equal to zero. In other words, the number of non-zero elements in the zero function is zero.
More concisely: For any finite type `ι` and function `β : ι → X` with decidable equality and a zero element for each `β i`, the Hamming norm of the zero function `λ i, 0` from `ι` to `X` is equal to zero.
|
hammingDist_zero_right
theorem hammingDist_zero_right :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)] (x : (i : ι) → β i), hammingDist x 0 = hammingNorm x
This theorem, `hammingDist_zero_right`, states that for any given finite type `ι` and any type `β` indexed by `ι`, if `β` elements have a decidable equality and a zero element, then the Hamming distance of any function `x` from `ι` to `β` and the zero function is equivalent to the Hamming norm of `x`. The Hamming distance here measures the number of positions where `x` and the zero function differ, and the Hamming norm of `x` measures the number of non-zero elements in `x`.
More concisely: For any finite type `ι` and type `β` indexed by `ι` with decidable equality and a zero element, the Hamming distance between a function `x` from `ι` to `β` and the zero function equals the Hamming norm of `x`.
|
hammingDist_nonneg
theorem hammingDist_nonneg :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
0 ≤ hammingDist x y
This theorem, `hammingDist_nonneg`, asserts that for any types `ι` and `β`, where `β` is a type function of `ι`, and given the conditions that `ι` is a finite type and there exists decidable equality for each `i` in `ι` for `β i`, the Hamming distance between any two elements `x` and `y`, which are functions from `i : ι` to `β i`, is always a non-negative integer. In simpler terms, it states that the Hamming distance, which calculates the number of positions at which the corresponding values are different, can't be negative.
More concisely: For any finite type `ι` and type function `β` over `ι`, the Hamming distance between any two functions `x` and `y` from `ι` to `β` is a non-negative integer.
|
hammingDist_triangle_right
theorem hammingDist_triangle_right :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
(x y z : (i : ι) → β i), hammingDist x y ≤ hammingDist x z + hammingDist y z
This theorem, referred to as `hammingDist_triangle_right`, is a variation of the triangle inequality for Hamming distance. For any finite type `ι`, function type `β` from `ι` to any type with decidable equality, and any three functions `x`, `y`, and `z` of type `β`, the Hamming distance between `x` and `y` is less than or equal to the sum of the Hamming distances between `x` and `z`, and `y` and `z`. In other words, the direct Hamming distance from `x` to `y` is never greater than the Hamming distance from `x` to `z` plus the Hamming distance from `y` to `z`. This theorem generalizes the triangle inequality to Hamming distance in the context of functions.
More concisely: For any finite type ι, function type β from ι to any type with decidable equality, and functions x, y, z of type β, the Hamming distance between x and y is less than or equal to the sum of the Hamming distances between x and z, and z and y.
|
hammingDist_eq_hammingNorm
theorem hammingDist_eq_hammingNorm :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → AddGroup (β i)] (x y : (i : ι) → β i), hammingDist x y = hammingNorm (x - y)
This theorem, referred to as `hammingDist_eq_hammingNorm`, states that for any given types `ι` and `β` where `β` is dependent on `ι`, and for any two functions `x` and `y` from `ι` to `β`, the Hamming distance between `x` and `y` is equal to the Hamming norm of the difference between `x` and `y`. This holds under the conditions that `ι` is a finite type, `β` has decidable equality and `β` forms an additive group. The Hamming distance between two functions is defined as the number of points at which the two functions differ, while the Hamming norm of a function is the number of points at which the function is not zero.
More concisely: For any finite type `ι`, and dependent type `β` forming an additive group with decidable equality, the Hamming distance between two functions from `ι` to `β` equals the Hamming norm of their pointwise difference.
|
eq_of_hammingDist_eq_zero
theorem eq_of_hammingDist_eq_zero :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
hammingDist x y = 0 → x = y
The theorem `eq_of_hammingDist_eq_zero` states that for any two functions `x` and `y` from an index type `ι` to a family of types `β i`, where each `β i` has decidable equality and `ι` is a finite type, if the Hamming distance between `x` and `y` is zero, then `x` and `y` must be equal. The Hamming distance is defined here as the number of indices at which the corresponding values of the two functions differ.
More concisely: If `x` and `y` are functions from a finite type `ι` to types `β i` with decidable equality, and their Hamming distance is zero, then `x` and `y` are equal.
|
hammingNorm_eq_zero
theorem hammingNorm_eq_zero :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x = 0 ↔ x = 0
This theorem, named `hammingNorm_eq_zero`, states that for any types `ι` and `β` where `β` is a function of `ι`, and given that `ι` is a type with finite elements, `β i` has decidable equality and a zero element for any `i` in `ι`, the Hamming weight (or norm) of a function `x : ι → β i` is zero if and only if the function `x` itself equals to the zero function. In other words, this theorem asserts that a function over a finite set has a Hamming weight of zero only if all of its output values are zero.
More concisely: For a function `x : ι → β` over a finite type `ι` with decidable equality and a zero element, `x` has Hamming weight zero if and only if `x` equals the zero function.
|
swap_hammingDist
theorem swap_hammingDist :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)],
Function.swap hammingDist = hammingDist
The theorem `swap_hammingDist` states the property of the Hamming distance, namely that the Hamming distance is symmetrical in its arguments. More specifically, for any finite type `ι` and any type function `β` from `ι` to another type, provided that for each `i : ι`, equality in `β i` is decidable, the Hamming distance function corresponds to its own swapped version. This means if we denote `hammingDist` by `d`, we have `d(x, y) = d(y, x)` for all `x` and `y`.
More concisely: For any finite type `ι` and type function `β` from `ι` to a type with decidable equality, the Hamming distance function `d` satisfies `d(x, y) = d(y, x)` for all `x, y : ι`.
|
hammingNorm_nonneg
theorem hammingNorm_nonneg :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, 0 ≤ hammingNorm x
The theorem `hammingNorm_nonneg` establishes that for all types `ι` and `β` (where `β` is a function from `ι` to a type), given that `ι` is a finite type, the equality of `β i` is decidable for all `i` in `ι`, and `0` is defined for `β i` for all `i` in `ι`, then the Hamming weight function of any function from `ι` to `β i` is always non-negative. In other words, the Hamming weight function, which counts the number of non-zero elements in the function's range, will always return a value greater than or equal to zero.
More concisely: For any finite type `ι` and function `β : ι → Type`, if `β i` is decidably equal to zero or a non-zero value for all `i` in `ι`, then the Hamming weight of any function from `ι` to `β i` is non-negative.
|
hammingDist_comm
theorem hammingDist_comm :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y : (i : ι) → β i),
hammingDist x y = hammingDist y x
The theorem `hammingDist_comm` states that the Hamming distance between two vectors `x` and `y` over a finite type `ι` is commutative. In other words, for any two vectors `x` and `y` from the space indexed by type `ι`, where each element of the space has a decidable equality, the Hamming distance from `x` to `y` is the same as the Hamming distance from `y` to `x`. The Hamming distance is calculated as the number of positions at which the corresponding values are different.
More concisely: For any two vectors `x` and `y` of equal length over a finite type `ι` with decidable equality, the Hamming distance between `x` and `y` equals the Hamming distance between `y` and `x`.
|
hammingDist_eq_zero
theorem hammingDist_eq_zero :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
hammingDist x y = 0 ↔ x = y
The theorem `hammingDist_eq_zero` asserts that for any finite type `ι`, any indexed type `β` such that for each `i : ι`, the type `β i` has decidable equality, and any two functions `x` and `y` mapping from `ι` to `β`, the Hamming distance between `x` and `y` is zero if and only if `x` and `y` are the same function. In other words, if the number of positions at which `x` and `y` output different values is zero, then `x` and `y` must be the same function.
More concisely: For any finite type ι and indexed type β with decidable equality, two functions x and y from ι to β have Hamming distance zero if and only if they are equal as functions.
|
hammingDist_self
theorem hammingDist_self :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x : (i : ι) → β i),
hammingDist x x = 0
This theorem states that for any finite type `ι` and any type `β` indexed by `ι`, if there exists a decidable equality on each `β i`, then the Hamming distance of any function `x : (i : ι) → β i` to itself is always 0. In other words, the Hamming distance, which counts the number of positions at which the corresponding values are different, between a function and itself is always zero, as there are no positions at which they differ.
More concisely: For any finite type `ι` and type `β` indexed by `ι` equipped with a decidable equality, the Hamming distance of a function `x : ι → β` to itself is always 0.
|
hammingDist_triangle
theorem hammingDist_triangle :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
(x y z : (i : ι) → β i), hammingDist x z ≤ hammingDist x y + hammingDist y z
This theorem is a version of the triangular inequality for the Hamming distance. Given three functions `x`, `y`, and `z` from an index type `ι` to types `β i` (where `i` is an element of `ι`), the theorem states that the Hamming distance between `x` and `z` is always less than or equal to the sum of the Hamming distances between `x` and `y`, and `y` and `z`. This holds for any `ι` that is a finite type and any `β i` that has decidable equality.
More concisely: For any finite type `ι` and functions `x, y, z : ι → β i` with decidable equality on `β i`, the Hamming distance between `x` and `z` is less than or equal to the sum of the Hamming distances between `x` and `y`, and `y` and `z`.
|
hammingNorm_ne_zero_iff
theorem hammingNorm_ne_zero_iff :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x ≠ 0 ↔ x ≠ 0
This theorem, `hammingNorm_ne_zero_iff`, is a statement about the Hamming weight function or Hamming norm, which is applied to objects of type `(i : ι) → β i`. The theorem says that for all types `ι` and any other type `β` that is indexed by `ι`, given that `ι` is a finite type and that `β i` has decidable equality and a zero-element for each `i : ι`, the Hamming norm of an object `x : (i : ι) → β i` is not zero if and only if `x` is not the zero object. In other words, the Hamming norm of `x` is non-zero exactly when `x` itself is non-zero.
More concisely: For any finite type `ι` and type `β` indexed by `ι`, the Hamming norm of a function `x : (i : ι) → β i` is non-zero if and only if `x` is not the zero function.
|
hamming_zero_eq_dist
theorem hamming_zero_eq_dist :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
0 = hammingDist x y ↔ x = y
This theorem, named `hamming_zero_eq_dist`, states that for any types `ι` and `β`, where `β` is a type dependent on `ι`, and for any two functions `x` and `y` from `ι` to `β`, the Hamming distance between `x` and `y` is zero if and only if `x` is equal to `y`. Here, `Fintype ι` denotes that `ι` has finitely many elements and `DecidableEq (β i)` asserts that equality between elements of type `β i` can be decided. In essence, this theorem relates the equality of two functions to their Hamming distance, a widely used measure in information theory to calculate the difference between two strings of equal length.
More concisely: For functions `x` and `y` from a finite type `ι` to a type `β` with decidable equality, the Hamming distance between `x` and `y` is zero if and only if `x` equals `y`.
|
hammingDist_zero_left
theorem hammingDist_zero_left :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)], hammingDist 0 = hammingNorm
The theorem `hammingDist_zero_left` asserts that for any type `ι` and any function `β` mapping `ι` to another type, given that `ι` is a finite type and that there is a decidable equality and a zero defined for each `ι` mapped by `β`, the Hamming distance of any member from zero is equivalent to its Hamming norm. In other words, this theorem states that for any element, the number of positions where it differs from zero (Hamming distance) is equal to the number of its non-zero positions (Hamming norm).
More concisely: For any finite type `ι` and function `β:` `ι` → * from a type `ι` to another type with decidable equality and a zero element, the Hamming distance of any `x` in `ι` equals the number of non-zero components of `β x`.
|
hammingNorm_pos_iff
theorem hammingNorm_pos_iff :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, 0 < hammingNorm x ↔ x ≠ 0
The theorem `hammingNorm_pos_iff` states that for all types `ι` and for all type functions `β` that map elements of `ι` to some type, given that `ι` has finite type (`Fintype ι`), each `i` in `ι` provides a decidable equality for `β i` (`DecidableEq (β i)`), and each `i` in `ι` has an associated zero (`Zero (β i)`), then for any function `x` from `ι` to `β i`, the Hamming weight (or Hamming norm) of `x` is greater than zero if and only if `x` is not the zero function. In other words, a function has a non-zero Hamming weight if and only if it is not the zero function.
More concisely: For a function `x` from a finite type `ι` with decidable equality and associated zero for each element, the Hamming weight of `x` is positive if and only if `x` is not the zero function.
|
hammingDist_smul
theorem hammingDist_smul :
∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
[inst_2 : (i : ι) → SMul α (β i)] {k : α} {x y : (i : ι) → β i},
(∀ (i : ι), IsSMulRegular (β i) k) → hammingDist (k • x) (k • y) = hammingDist x y
The theorem `hammingDist_smul` states that for any types `α`, `ι` and a type function `β : ι → Type`, given that `ι` is a finite type, each `β i` for `i : ι` has decidable equality, and each `β i` is a scalar multiplication space over `α`, for any scalar `k : α` and any two functions `x, y : (i : ι) → β i`, if `k` is a scalar multiplication regular element for each `β i`, then the Hamming distance between the scalar multiplication of `k` and `x` and the scalar multiplication of `k` and `y` is equal to the Hamming distance between `x` and `y`. In simpler terms, the Hamming distance remains preserved under scalar multiplication by a regular element.
More concisely: For finite types `ι` and type functions `β : ι → ℝ`, if each `β i` is a scalar multiplication space over a commutative ring `α` and `k` is a regular scalar element in `α` for each `β i`, then the Hamming distance between the scalar multiplications of `k` and `x` and `k` and `y`, for functions `x, y : ι → β i`, equals the Hamming distance between `x` and `y`.
|
hammingDist_pos
theorem hammingDist_pos :
∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {x y : (i : ι) → β i},
0 < hammingDist x y ↔ x ≠ y
This theorem, `hammingDist_pos`, states that for any types `ι` and `β`, where `β` is a function from `ι` to another type and `ι` is a fintype, i.e., a finite type, and we have decidable equality for all `i : ι` over `β i`, then the Hamming distance between two functions `x` and `y` (from `ι` to `β`) is greater than zero if and only if `x` is not equal to `y`. In other words, the Hamming distance measures how different the two functions are, with a zero distance implying that the functions are the same.
More concisely: For functions `x` and `y` from a finite type `ι` to another type `β` with decidable equality, their Hamming distance is positive if and only if `x` is not equal to `y`.
|