Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersCode.exists_relClosest_codeword_of_Nonempty_Code
Plain-language statement
This follows proof strategy from exists_closest_codeword_of_Nonempty_Code. However, it's NOT used to construct pickRelClosestCodeword_of_Nonempty_Code.
Source project: ArkLib
Person-level attribution pending.
Code.finite_relHammingDistRange
Plain-language statement
The range of the relative Hamming distance function is finite.
Source project: ArkLib
Person-level attribution pending.
Code.jointAgreement_iff_jointProximity
Plain-language statement
Equivalence between the agreement-based definition jointAgreement and the distance/proximity-based definition jointProximity (the latter is represented in upperbound of interleaved-code distance).
Source project: ArkLib
Person-level attribution pending.
Code.pairRelDist_le_iff_pairDist_le
Plain-language statement
Equivalence between relative and natural distance bounds.
Source project: ArkLib
Person-level attribution pending.
Code.relCloseToCode_iff_relCloseToCodeword_of_minDist
Plain-language statement
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?
Source project: ArkLib
Person-level attribution pending.
Code.relDist_floor_bound_iff_complement_bound
Project documentation
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...
Source project: ArkLib
Person-level attribution pending.