Research proof index

A word u is close to a code C within an absolute error bound e if and only if it is close within the equivalent relative error bound e / n.

This follows proof strategy from exists_closest_codeword_of_Nonempty_Code. However, it's NOT used to construct pickRelClosestCodeword_of_Nonempty_Code.

The range of the relative Hamming distance function is finite.

Equivalence between relative and natural distance bounds.

Relative distance version of closeToCode_iff_closeToCodeword_of_minDist. If the distance to a code is at most δ, then there exists a codeword within distance δ. NOTE: can we make this shorter using relDistFromCode_eq_distFromCode_div?

The equivalence between the two lowerbound of upperBound in Nat and NNReal context. In which, upperBound is viewed as the size of an agreement set S (e.g. between two words, or between a word to a code, ...). Specifically, n - ⌊δ * n⌋ ≤ (upperBound : ℕ) ↔ (1 - δ) * n ≤ (upperBound : ℝ≥0). This lemma is useful for jumping back-and-forth between...