OAI/Combinatorics/Progressions/Sampling/AllocatedExternalLocalGoodForecastPath.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.forecastContinuous_modular_norm_le line 66
  2. theorem OAI.Erdos3.VectorPolynomial.forecastContinuous_modular_early_norm_le line 138
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityPhysicalForecast_norm_le line 256
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedDensityPhysicalForecast_early_norm_le line 318
  5. theorem OAI.Erdos3.VectorPolynomial.fixedSpatialKernel_scaled_forecast_early_norm_le line 443
  6. theorem OAI.Erdos3.VectorPolynomial.actualForecastPrimeNeZero line 552
  7. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath line 575
  8. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.normalizedNoise line 631
  9. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.primeNeZero line 636
  10. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets line 673
  11. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_center line 681
  12. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_base line 684
  13. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_noise line 687
  14. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_sample line 690
  15. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_read line 693
  16. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_commonTuple line 696
  17. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_primes line 699
  18. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_exponent line 702
  19. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_prescribed line 705
  20. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_origin line 708
  21. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_Rbad line 711
  22. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_lower line 714
  23. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_width line 717
  24. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.enlargeBudgets_normalizedNoise line 720
  25. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup line 745
  26. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.logs line 822
  27. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastSetup.logs_nonneg line 826
  28. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.physicalPolynomial line 866
  29. theorem OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.physicalPolynomial_mem line 873
  30. def OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastPath.target line 881
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredFramedRead_bad_depth_eq line 932
  32. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredFramedRead_bad_product_eq line 961
  33. def OAI.Erdos3.VectorPolynomial.preparedCenteredActualForecastPath line 1009
  34. def OAI.Erdos3.VectorPolynomial.preparedCenteredSupportedActualForecastPath line 1095
  35. def OAI.Erdos3.VectorPolynomial.preparedCenteredGoodActualForecastPath line 1174
  36. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.goodForecastPath line 1294
  37. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.goodForecastPath_data line 1317
  38. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.goodForecastPathForSetup line 1333
  39. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.goodForecastPathForSetup_data line 1341