OAI/Combinatorics/Progressions/Dynamics/PreparedFiniteScheduleGeometryBudget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteSchedulePowerBudget line 13
2. theorem OAI.Erdos3.VectorPolynomial.canonical_minorVariable_mono line 134
3. theorem OAI.Erdos3.VectorPolynomial.canonical_minorDegree_mono line 140
4. theorem OAI.Erdos3.VectorPolynomial.canonical_minorConstant_mono line 146
5. theorem OAI.Erdos3.VectorPolynomial.canonical_minorLog_mono line 156
6. theorem OAI.Erdos3.VectorPolynomial.canonical_inverseAxis_mono line 172
7. theorem OAI.Erdos3.VectorPolynomial.canonical_derivativeAxis_mono line 181
8. theorem OAI.Erdos3.VectorPolynomial.canonical_weightAxis_mono line 189
9. theorem OAI.Erdos3.VectorPolynomial.canonical_jointSource_mono line 199
10. theorem OAI.Erdos3.VectorPolynomial.canonical_profileInput_mono line 216
11. theorem OAI.Erdos3.VectorPolynomial.exists_canonicalSliceEarlyScale_budget line 227
12. theorem OAI.Erdos3.VectorPolynomial.exists_primitiveCanonicalSliceEarlyScale_budget line 340
13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleEarlyBudget line 402
14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleEarlyBudgetWithCutoff line 493
15. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleGeometryBudget line 584