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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersPolynomial.FoldingPolynomial.folding_polynomial_deg_y_bound
Plain-language statement
The degree of foldingPolynomial is less than q.degree in the second variable, when q is not a constant polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folding_polynomial_is_unique
Plain-language statement
The uniqueness of the folding polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.folding_polynomial_is_unique'
Project documentation
Alternative uniqueness theorem for the folding polynomial. The only difference is the h_x condition which in this theorem is only and inequality. Handy in practice since degreeX is defined as a supremum so inequality is much easier to prove for it.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.polyFold_base
Plain-language statement
Base case of polyFold: when k = 0 or f has degree below k, polyFold f k r = C (f.eval r).
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.polyFold_natDegree_le
Plain-language statement
The degree bound of polyFold in terms of the degree of the original polynomial and k.
Source project: ArkLib
Person-level attribution pending.
Polynomial.FoldingPolynomial.polyFold_step
Plain-language statement
Recursive case of polyFold: when 0 < k ≤ f.natDegree, polyFold f k r = C ((f %ₘ X^k).eval r) + X * polyFold (f /ₘ X^k) k r.
Source project: ArkLib
Person-level attribution pending.