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.indicator_eq_1_of_neg_empty_empty_of_pos_nonempty
Plain-language statement
The indicator polynomial is a constant one polynomial if the set neg is empty while pos is not.
Source project: ArkLib
Person-level attribution pending.
Polynomial.indicator_eq_1_on_pos
Plain-language statement
Indicator evaluated on an element of pos is equal to 1.
Source project: ArkLib
Person-level attribution pending.
Polynomial.indicator_ne_zero_of_pos_nonempty
Plain-language statement
If pos is non-empty then the indicator polynomial is the constant zero polynomial.
Source project: ArkLib
Person-level attribution pending.
Polynomial.splitNth_of_sum_comp
Plain-language statement
splitNth is the left inverse of the n-way recombination: splitting the polynomial ∑ j, X^j * (u j)(X^n) recovers u i for each component i.
Source project: ArkLib
Person-level attribution pending.
PolynomialGenerator.poly_gen_is_zero_evading
Plain-language statement
If G is a polynomial generator, then G is zero-evading with error the maximum of the total degrees of the individual polynomials divided by the size of the smallest evaluation sets S i. Remark 3.20, the version of the statement in the brackets [BCGM25]. Note: Remark 3.20 provides two ways of viewing a polynomial generator as a zero-evading generator...
Source project: ArkLib
Person-level attribution pending.
Pr_add_split_by_complement
Plain-language statement
Law of Total Probability (Partitioning an Event) The probability of an event f r occurring can be calculated by summing the probabilities of two disjoint cases: 1. f r occurs AND g r occurs. 2. f r occurs AND g r does NOT occur. Good to be used with Pr_multi_let_equiv_single_let
Source project: ArkLib
Person-level attribution pending.