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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,225 to 1,230 of 2,569 results.
GuruswamiSudan.gs_existence
Mathematical statement
GS existence with rate-corrected degree bound (ρ = k/n). Requires k > 1 for the counting argument and m ≥ 1 for multiplicity.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.gs_numVars_gt_numConstraints_of_gt_one
Mathematical statement
numVars with gs_degree_bound exceeds numConstraints (for k > 1).
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.gs_sufficient_multiplicity_bound
Mathematical statement
The degree bound with ρ = k/n is strictly less than m times the number of agreement points, provided the distance is within the rate-corrected Johnson radius gs_johnson.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.interpolate_eq_of_degree_lt
Mathematical statement
If a polynomial q has degree less than n, then interpolating its values at n points recovers q.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.mem_decoder_of_dist
Mathematical statement
If a polynomial of degree is -close to the received word, it appears in the decoder output.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.natWeightedDegree_add_le
Mathematical statement
The weighted degree of a sum is at most the maximum of the weighted degrees.
Source project: ArkLib
Person-level attribution pending.