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 2 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersArkLib.Lattices.Hachi.evalSplit_eq_eval
Plain-language statement
The split. Evaluating a multilinear polynomial equals the vector–matrix–vector product of its reshaped coefficient matrix with the monomial bases of the low and high evaluation points (Hachi [NOZ26, §4]).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Hachi.evalSplitEval_eq_eval
Plain-language statement
The split (Lagrange representation). Evaluating a multilinear polynomial given by its hypercube values equals the vector–matrix–vector product of its reshaped value matrix with the Lagrange bases of the low and high evaluation points.
Source project: ArkLib
Person-level attribution pending.