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 filtersReduction.support_run_pure_verifier
Plain-language statement
If a reduction's verifier is a pure function f of the input statement and full transcript, then the verifier output of any complete result in the support of Reduction.run equals f stmt td applied to the input statement and the produced transcript.
Source project: ArkLib
Person-level attribution pending.
reedSolomon_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.mem_rs_code_iff_exists_mle
Plain-language statement
A word f belongs to the RS-code iff there exists a multilinear polynomial g such that f is evaluation of powAlgHom g on points from the eval domain.
Source project: ArkLib
Person-level attribution pending.