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.natWeightedDegree_smul_le
Plain-language statement
The weighted degree of a scalar multiple is at most the weighted degree of the polynomial.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.natWeightedDegree_sum_le
Plain-language statement
The weighted degree of a sum is bounded by the supremum of the weighted degrees.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.numVars_lower_bound_tight
Plain-language statement
A tighter lower bound for the number of variables when k > 1 : 2(k-1) * numVars ≥ D(D+2).
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.polySol_ne_zero
Plain-language statement
The solved polynomial is non-zero.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.proximity_gap_degree_bound_sq_gt
Plain-language statement
Lower bound for the square of (D+1). Specifically, (D+1)^2 > (m+1/2)^2 * (k+1) * n.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.rootMultiplicity_ge_of_shift_zero
Plain-language statement
If the shifted polynomial has no non-zero coefficients of total degree less than m, then the root multiplicity is at least m.
Source project: ArkLib
Person-level attribution pending.