OAI/Combinatorics/Progressions/Sampling/PreparedForecastRequiredPowerBudget.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCentered_forecastGoodData line 18
  2. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastGoodConclusion line 189
  3. def OAI.Erdos3.VectorPolynomial.preparedCenteredForecastGoodExponent line 245
  4. def OAI.Erdos3.VectorPolynomial.preparedCenteredForecastSpatialExponent line 248
  5. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecastGoodExponent_ge line 251
  6. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecastSpatialExponent_ge line 255
  7. theorem OAI.Erdos3.VectorPolynomial.preparedCenteredForecast_spatialThreshold_inv line 259
  8. def OAI.Erdos3.VectorPolynomial.preparedCenteredForecastGoodRequired line 268
  9. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastGoodProperty line 283
  10. def OAI.Erdos3.VectorPolynomial.PreparedCenteredShortForecastGoodConclusion line 320
  11. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastReadFamily line 376
  12. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastPathPoint line 398
  13. def OAI.Erdos3.VectorPolynomial.PreparedCenteredForecastPathContinuation line 439
  14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCentered_forecastPathFamily line 478
  15. def OAI.Erdos3.VectorPolynomial.PreparedCenteredShortForecastGoodProperty line 551
  16. def OAI.Erdos3.VectorPolynomial.PreparedCenteredSlicedForecastPathPoint line 588
  17. def OAI.Erdos3.VectorPolynomial.PreparedCenteredSlicedForecastPathContinuation line 630
  18. theorem OAI.Erdos3.VectorPolynomial.exists_preparedCentered_slicedForecastPathFamily line 665
  19. theorem OAI.Erdos3.VectorPolynomial.exists_preparedRetainedActualForecastFactory line 770
  20. def OAI.Erdos3.VectorPolynomial.preparedForecastProductiveRequired line 829
  21. theorem OAI.Erdos3.VectorPolynomial.exists_preparedForecastRequired_power_budget line 839