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 filtersGuruswamiSudan.gs_numVars_gt_numConstraints_of_gt_one
Plain-language statement
numVars with gs_degree_bound exceeds numConstraints (for k > 1).
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.gs_sufficient_multiplicity_bound
Plain-language 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
Plain-language 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
Plain-language 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
Plain-language statement
The weighted degree of a sum is at most the maximum of the weighted degrees.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.natWeightedDegree_coeffsToPoly_le
Plain-language statement
The weighted degree of the polynomial constructed from coefficients is bounded by D.
Source project: ArkLib
Person-level attribution pending.