OAI/Combinatorics/Progressions/Sampling/PreparedCenteredShortForecastGoodInterface.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.preparedForecastGoodCertificateBudget line 10
  2. def OAI.Erdos3.preparedForecastGoodAnalyticBudget line 13
  3. theorem OAI.Erdos3.preparedForecastGoodBudgets line 17
  4. theorem OAI.Erdos3.exists_preparedForecastGoodBudgets_bound line 42
  5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCentered_short_forecastGoodData line 79
  6. def OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastGoodExponent line 250
  7. def OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastSpatialExponent line 253
  8. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastGoodExponent_ge line 256
  9. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastSpatialExponent_ge line 260
  10. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecast_spatialThreshold_inv line 264
  11. def OAI.Erdos3.VectorPolynomial.preparedCenteredShortForecastGoodRequired line 273
  12. def OAI.Erdos3.VectorPolynomial.preparedShortForecastProductiveRequired line 286
  13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedShortForecastRequired_power_budget line 296
  14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedForecastConstructedRequired_power_budget line 374
  15. theorem OAI.Erdos3.VectorPolynomial.exists_preparedShortForecastConstructedRequired_power_budget line 440
  16. def OAI.Erdos3.VectorPolynomial.PreparedCenteredShortForecastGoodModelInterface line 568