OAI/Combinatorics/Progressions/Geometry/AllocatedInactiveSupportBudget.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.two_mul_add_three_exp_bound line 11
  2. theorem OAI.Erdos3.blockJetScaleBound_four_exp line 20
  3. def OAI.Erdos3.VectorPolynomial.allocatedNaturalSupportLog line 43
  4. def OAI.Erdos3.VectorPolynomial.allocatedNaturalSiteLog line 45
  5. def OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientLog line 47
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSupportLog_nonneg line 49
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSiteLog_nonneg line 52
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientLog_nonneg line 55
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedIntegerBlock_card_le line 65
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedGridTorusFactor_exp_bound line 71
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSupportRadius_exp_bound line 85
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedNaturalSiteRadius_exp_bound line 109
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteCoefficientRadius_exp_bound line 130
  14. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSupportLog line 160
  15. def OAI.Erdos3.VectorPolynomial.allocatedInactiveLongRadius line 166
  16. def OAI.Erdos3.VectorPolynomial.allocatedInactiveShortRadius line 170
  17. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteRadius line 176
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveLongRadius_le_natural line 181
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveShortRadius_exp_bound line 198
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteRadius_exp_bound line 232