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.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.
GuruswamiSudan.rootMultiplicity_le_of_coeff_ne_zero
Plain-language statement
If the (s, t)-coefficient of shift Q x y is non-zero, then the root multiplicity of Q at (x, y) is at most s + t.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.roots_le_degree_of_deg_lt_roots
Plain-language statement
If a polynomial R has roots at points indexed by A with multiplicity at least m, and its degree is strictly less than m * |A|, then R must be the zero polynomial.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.sufficient_multiplicity_bound
Plain-language statement
The degree bound is strictly less than m times the number of agreement points, provided the distance is within the Johnson radius.
Source project: ArkLib
Person-level attribution pending.
GuruswamiSudan.toPolynomial_degree_le
Plain-language statement
The polynomial corresponding to a codeword has degree at most k-1.
Source project: ArkLib
Person-level attribution pending.
H₂_imag_axis_pos
Plain-language statement
H₂(it) > 0 for all t > 0. Blueprint: Lemma 6.43 - H₂ is positive on the imaginary axis. Proof strategy: Each term exp(-π(n+1/2)²t) > 0, so Θ₂(it) > 0, hence H₂ = Θ₂^4 > 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.