OAI/Combinatorics/Progressions/Dynamics/CoefficientAmbientBudget.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.coefficientSlot_card_le line 11
2. theorem OAI.Erdos3.VectorPolynomial.exists_coefficient_tensor_mass_budget line 23
3. theorem OAI.Erdos3.VectorPolynomial.finiteTensorCoefficientMass_le line 45
4. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientIndex_card_le line 63
5. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientIndex_card_le_real line 74
6. def OAI.Erdos3.VectorPolynomial.coefficientAmbientInputPolynomial line 90
7. theorem OAI.Erdos3.VectorPolynomial.coefficient_ambient_input_exp_bounds line 93
8. theorem OAI.Erdos3.VectorPolynomial.exists_coefficient_ambient_input_budget line 126