OAI/Combinatorics/Progressions/Estimates/CanonicalSiteBlocks.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.siteSpectrumBlockCount line 13
  2. theorem OAI.Erdos3.siteSpectrumBlockCount_pos line 17
  3. theorem OAI.Erdos3.siteSpectrumBlockCount_bound line 21
  4. theorem OAI.Erdos3.principalProfileSize_le_radius line 34
  5. theorem OAI.Erdos3.principalProfileSize_le_natScale line 39
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedUniformBlocks_spectrum_bound line 45
  7. def OAI.Erdos3.VectorPolynomial.allocatedPositiveSitePeriod line 55
  8. def OAI.Erdos3.VectorPolynomial.allocatedSiteKernelMaskLog line 78
  9. def OAI.Erdos3.VectorPolynomial.allocatedSiteScaleNumeric line 81
  10. def OAI.Erdos3.VectorPolynomial.allocatedSiteScaleLog line 84
  11. def OAI.Erdos3.VectorPolynomial.allocatedSiteSourceLog line 89
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteKernelMaskLog_nonneg line 93
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScaleNumeric_bounds line 96
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteSourceLog_bounds line 106
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSiteSourceLog_bound line 121
  16. def OAI.Erdos3.VectorPolynomial.allocatedSiteScale line 144
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_lower line 148
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_period_window line 153
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_upper line 172
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_ready line 186
  21. theorem OAI.Erdos3.VectorPolynomial.boundedCoefficientExponent_card_add_one_le_site_numeric line 211
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteScale_coefficient_count line 238
  23. def OAI.Erdos3.VectorPolynomial.canonicalSiteBlockCount line 258
  24. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlockCount_pos line 260
  25. instance OAI.Erdos3.VectorPolynomial.canonicalSiteBlockCount_neZero line 264
  26. abbrev OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks line 267
  27. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks_spectrum_count line 270
  28. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlockCount_jet_bound line 278
  29. def OAI.Erdos3.VectorPolynomial.canonicalSiteBlockEmbedding line 288
  30. def OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks_jetEmbedding line 297
  31. def OAI.Erdos3.VectorPolynomial.canonicalSiteVariableFactor line 303
  32. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks_variables_card line 305
  33. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks_variables_bound line 312
  34. theorem OAI.Erdos3.VectorPolynomial.canonicalSiteBlocks_coefficient_count line 337