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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersreedSolomon_multilinearCorrelatedAgreement_Nat
Plain-language statement
Corollary 3.7: RS Codes have Tensor-Style Proximity Gaps (Unique Decoding) Example 4.1 shows that ε=n is tight for RS codes (Ben+23 Thm 4.1 is sharp).
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.dim_eq_card_of_lt
Plain-language statement
The dimension of an RS-code equals the cardinality of the evaluation points if the original degree exceeds the cardinality.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.dim_eq_deg_of_le
Plain-language statement
Dimension formula for RS code with arbitrary finite index type ι.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.genMatIsVandermonde
Plain-language statement
The Vandermonde matrix is the generator matrix for an RS code of length ι and dimension deg.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.relativeUniqueDecodingRadius_RS_eq
Plain-language statement
Relative unique decoding radius for RS code with arbitrary finite index type ι.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.toPolynomial_mem_lt_deg
Plain-language statement
The polynomials corresponding to Reed-Solomon codewords are of degree smaller than deg.
Source project: ArkLib
Person-level attribution pending.