Research proof index

The range of the relative Hamming distance function is finite.

Equivalence between the agreement-based definition jointAgreement and the distance/proximity-based definition jointProximity (the latter is represented in upperbound of interleaved-code distance).

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...

A word u is relatively close to a code C within an relative error bound δ if and only if it is relatively close within the equivalent absolute error bound ⌊δ * n⌋.