OAI/Combinatorics/Progressions/Probability/CoefficientProductLaw.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.coefficientProductDensity line 12
2. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_nonneg line 17
3. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_bound line 23
4. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_ne_zero_factors line 30
5. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_probability line 37
6. theorem OAI.Erdos3.VectorPolynomial.coefficientProductDensity_coordinate_law line 76