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 filtersCheckClaim.oracleVerifier_toVerifier_run
Plain-language statement
The pure pass-through oracle verifier's underlying non-oracle verifier returns the combined input statement unchanged.
Source project: ArkLib
Person-level attribution pending.
CheckClaim.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.