OAI/Combinatorics/Progressions/Dynamics/AllocatedActiveBudgetedSite.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.siteExponentialOutputLog line 11
  2. theorem OAI.Erdos3.siteExponentialOutputLog_nonneg line 14
  3. theorem OAI.Erdos3.siteExponentialOutput_bounds line 17
  4. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteBudgetLog line 62
  5. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteOutputLog line 67
  6. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSitePrimitiveLog line 72
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteBudgetLog_bounds line 76
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteOutputLog_bounds line 94
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedInactiveSitePrimitiveLog_bound line 105
  10. theorem OAI.Erdos3.siteCharacterLipschitz_exp_bound line 132
  11. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteFactor line 165
  12. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteCap line 169
  13. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteBias line 173
  14. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteSize line 177
  15. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSiteFrequency line 183
  16. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSitePeriod line 187
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSite_construction_bounds line 196
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSite_output_bounds line 236
  19. def OAI.Erdos3.VectorPolynomial.allocatedActiveSpectrumLog line 299
  20. def OAI.Erdos3.VectorPolynomial.allocatedActivePointCapLog line 304
  21. def OAI.Erdos3.VectorPolynomial.allocatedActiveSiteBudgetLog line 307
  22. def OAI.Erdos3.VectorPolynomial.allocatedActiveSiteOutputLog line 311
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSpectrumLog_nonneg line 314
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSpectrumLog_member line 321
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePointCapLog_nonneg line 337
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteBudgetLog_bounds line 343
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSiteOutputLog_nonneg line 355
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedActivePointCap_exp_bound line 367
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSpectrum_exp_bounds line 378
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveSite_construction_bounds line 399
  31. def OAI.Erdos3.VectorPolynomial.allocatedInactivePointCapLog line 438
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedInactivePointCapLog_nonneg line 442
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveGrid_norm_exp_bound line 466
  34. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_inactive_budgeted_site_expansion line 502
  35. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveGrid_norm_exp_bound line 573
  36. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_active_budgeted_site_expansion line 601