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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersCheckClaim.reduction_completeness
Plain-language statement
The CheckClaim reduction satisfies perfect completeness with respect to the predicate as the input relation, and the output relation being always true.
Source project: ArkLib
Person-level attribution pending.
Code.dist_pos_of_Nontrivial
Plain-language statement
A non-trivial code (a code with at least two distinct codewords) must have a minimum distance greater than 0.
Source project: ArkLib
Person-level attribution pending.
Code.distFromCode_le_iff_relDistFromCode_le
Plain-language statement
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.
Source project: ArkLib
Person-level attribution pending.
Code.distFromCode'_eq_distFromCode
Project documentation
For finite nonempty codes, the computable distance equals the noncomputable distance.
Source project: ArkLib
Person-level attribution pending.
Code.eq_of_le_uniqueDecodingRadius
Plain-language statement
A stronger version of distFromCode_eq_of_lt_half_dist: If two codewords v and w are both within the uniqueDecodingRadius of u (i.e. 2 * Δ₀(u, v) < ‖C‖₀ and 2 * Δ₀(u, w) < ‖C‖₀), then they must be equal.
Source project: ArkLib
Person-level attribution pending.
Code.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.