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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersGuruswamiSudan.gs_degree_bound_sq_gt
Plain-language statement
Lower bound: (gs_degree_bound + 1)^2 > (m+1/2)^2 * k * n.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.gs_dvd_property
Plain-language statement
Divisibility via the rate-corrected GS system. Uses gs_degree_bound (ρ=k/n) and gs_johnson instead of the conservative proximity_gap versions.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.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.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.