OAI/Combinatorics/Progressions/Fourier/AllocatedMaskedCoefficientFourier.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficientAmbientDensity_bounds line 28
  2. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_coefficient_fourier_approximation line 41
  3. def OAI.Erdos3.VectorPolynomial.coefficientAmbientBudgetExponent line 80
  4. theorem OAI.Erdos3.VectorPolynomial.coefficientAmbientBudgetExponent_bound line 83
  5. def OAI.Erdos3.VectorPolynomial.allocatedFourierLogBudget line 89
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedFourierLogBudget_nonneg line 92
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFourierLogBudget_bound line 98
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedCoefficient_fourier_input_budget line 117
  9. def OAI.Erdos3.VectorPolynomial.allocatedFourierOutputBudget line 158
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedFourierOutputBudget_dominates line 162
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFourierOutputBudget_bound line 175
  12. def OAI.Erdos3.VectorPolynomial.allocatedMaskedFourierBudget line 199
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedMaskedFourierBudget_bounds line 203
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedMaskedFourierBudget_bound line 215
  15. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_coefficient_uniform_fourier line 264
  16. def OAI.Erdos3.VectorPolynomial.allocatedJetFourierBudget line 313
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedJetFourierBudget_nonneg line 316
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedJetFourierBudget_dominates line 322
  19. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedJetFourierBudget_bound line 353
  20. def OAI.Erdos3.VectorPolynomial.selectedScaleDimensionBudget line 373
  21. theorem OAI.Erdos3.VectorPolynomial.selectedScaleDimensionBudget_nonneg line 376
  22. theorem OAI.Erdos3.VectorPolynomial.le_selectedScaleDimensionBudget line 380
  23. theorem OAI.Erdos3.VectorPolynomial.degree_le_selectedScaleDimensionBudget line 384
  24. theorem OAI.Erdos3.VectorPolynomial.coefficientCount_le_selectedScaleDimensionBudget line 388
  25. def OAI.Erdos3.VectorPolynomial.selectedFourierInputBudget line 394
  26. theorem OAI.Erdos3.VectorPolynomial.selectedFourierInputBudget_nonneg line 397
  27. theorem OAI.Erdos3.VectorPolynomial.le_selectedFourierInputBudget line 401
  28. def OAI.Erdos3.VectorPolynomial.selectedFourierOutputBudget line 406
  29. theorem OAI.Erdos3.VectorPolynomial.exists_selectedFourierOutputBudget_bound line 409
  30. def OAI.Erdos3.VectorPolynomial.selectedFourierExponent line 423
  31. theorem OAI.Erdos3.VectorPolynomial.selectedFourierExponent_two_le line 426
  32. theorem OAI.Erdos3.VectorPolynomial.selectedFourierOutputBudget_bound line 429
  33. def OAI.Erdos3.VectorPolynomial.allocatedMaskedCoefficientDensity line 450
  34. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_coefficient_fourier line 462
  35. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_coefficient_uniform_fourier line 504