OAI/Combinatorics/Progressions/Fourier/AllocatedSiteSpectrumBudget.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedGridTorusLog line 13
  2. def OAI.Erdos3.VectorPolynomial.allocatedSpectrumScaleLog line 15
  3. def OAI.Erdos3.VectorPolynomial.allocatedSpectrumCardEnvelope line 18
  4. def OAI.Erdos3.VectorPolynomial.allocatedSpectrumFrequencyEnvelope line 23
  5. def OAI.Erdos3.VectorPolynomial.allocatedGridFamilyLog line 28
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrumScaleLogs_nonneg line 31
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrumCardEnvelope_nonneg line 36
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrumFrequencyEnvelope_nonneg line 43
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedGridFamilyLog_nonneg line 51
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrumCardEnvelope_member line 57
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrumFrequencyEnvelope_member line 72
  12. theorem OAI.Erdos3.VectorPolynomial.finiteBooleanRows_card_le line 88
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedSpectrum_scales line 101
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedGridPointCap_exp_bound line 114
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedGridFamilyCap_exp_bound line 131
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedGridRetainedFrequency_exp_bound line 144
  17. def OAI.Erdos3.VectorPolynomial.allocatedInactiveTorusLog line 170
  18. def OAI.Erdos3.VectorPolynomial.allocatedInactiveScaleLog line 172
  19. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrumLog line 175
  20. def OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrumPrimitiveLog line 180
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveScaleLogs_nonneg line 184
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrumLog_nonneg line 189
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrumLog_member line 196
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedInactiveSpectrumPrimitiveLog_bound line 212
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrum_scales line 234
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedInactiveSpectrum_exp_bounds line 277
  27. def OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrumCapLog line 311
  28. def OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrumInput line 314
  29. def OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrumFrequencyLog line 317
  30. def OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrumLog line 322
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrumLog_bounds line 326
  32. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedSiteSpectrumLog_bound line 342
  33. theorem OAI.Erdos3.VectorPolynomial.allocatedSiteSpectrum_primitive_budget line 365