OAI/Combinatorics/Progressions/Lattices/AllocatedAffineCanonicalBackendBudget.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetHeightLog line 10
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetHeightLog_bounds line 12
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetHeightLog_exp_bounds line 34
  4. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetRightLog line 53
  5. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetLeftLog line 57
  6. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetCompareLog line 61
  7. def OAI.Erdos3.VectorPolynomial.allocatedAffineResetMapBudget line 64
  8. def OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalNativeBudget line 68
  9. def OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudget line 71
  10. structure OAI.Erdos3.VectorPolynomial.AllocatedAffineResetMapBudgetBounds line 78
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetMapBudget_bounds line 87
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetMapBudget_denominator line 100
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineResetLogBudget_nonnegative line 112
  14. structure OAI.Erdos3.VectorPolynomial.AllocatedAffineCanonicalBudgetBounds line 118
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudget_bounds line 136
  16. structure OAI.Erdos3.VectorPolynomial.AllocatedAffineCanonicalExpBounds line 173
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudget_exp_bounds line 190
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudget_le_diagonal line 220
  19. def OAI.Erdos3.VectorPolynomial.canonicalSectionPolynomial line 262
  20. def OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudgetPolynomial line 266
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBudgetPolynomial_eval line 284
  22. def OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackendPolynomial line 299
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackendPolynomial_eval line 304
  24. theorem OAI.Erdos3.VectorPolynomial.power_le_recursiveParameter line 315
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonical_cutoffCost_le_recursive line 321
  26. structure OAI.Erdos3.VectorPolynomial.AllocatedAffineCanonicalBackendBounds line 333
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackendPolynomial_bounds line 343
  28. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedAffineCanonicalBackend_budget line 377
  29. def OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackendExponent line 390
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackendExponent_ge_two line 393
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedAffineCanonicalBackend_bounds line 397