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 filtersBCIKS20AppendixA.canonicalRepOf𝒪_mk
Plain-language statement
Canonical representatives of quotient constructors are computed by modByMonic.
Source project: ArkLib
Person-level attribution pending.
BCIKS20AppendixA.H_tilde_equiv_H_tilde'
Plain-language statement
The polynomial H_tilde' agrees with the monicization H_tilde after embedding into Polynomial (RatFunc F).
Source project: ArkLib
Person-level attribution pending.
BCIKS20AppendixA.mk_canonicalRepOf𝒪
Plain-language statement
The canonical representative maps back to the original quotient element of 𝒪.
Source project: ArkLib
Person-level attribution pending.
BerlekampWelch.decoder_eq_some
Project documentation
Correctness theorem for Berlekamp-Welch decoder: If a codeword is close to a polynomial p of degree < k then the decoder succeeds and returns some p. ### Parameters: - e k : ℕ - Error capacity and degree bound - [NeZero n] - Non-zero codeword length - ωs : Fin n → F - Distinct evaluation points (injective mapping) - f : Fin n → F - Recei...
Source project: ArkLib
Person-level attribution pending.
BerlekampWelch.linsolve_always_some_berlekamp_welch
Plain-language statement
If only up to e errors happened linsolve cannot fail to find a solution.
Source project: ArkLib
Person-level attribution pending.
BerlekampWelch.Q'_div_E'_eq_p
Plain-language statement
If there has happened up to e errors then any other E' and Q' satifying Berlekamp-Welch condition will result in the same quotient Q' \ E' = p.
Source project: ArkLib
Person-level attribution pending.