OAI/Combinatorics/Progressions/Polynomial/ForecastSlicedEarlyUnrestrictedPolynomialBudget.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.majorArcBiasLog_mono_budget line 10
  2. theorem OAI.Erdos3.majorArcLocalizationLog_mono_budget line 16
  3. theorem OAI.Erdos3.majorArcLengthLog_mono_budget line 22
  4. theorem OAI.Erdos3.majorArcErrorLog_mono_budget line 28
  5. theorem OAI.Erdos3.majorArcCoverLog_mono_budget line 34
  6. theorem OAI.Erdos3.positiveModerateLengthLog_mono_budget line 40
  7. theorem OAI.Erdos3.positiveModerateCoverLog_mono_budget line 46
  8. theorem OAI.Erdos3.positiveModerateSpectrumLog_mono_budget line 52
  9. theorem OAI.Erdos3.positiveModerateAccuracyLog_mono_budget line 58
  10. theorem OAI.Erdos3.positiveRetainedBiasLog_mono_budget line 64
  11. theorem OAI.Erdos3.positiveSpectrumCardLog_mono_budget line 70
  12. theorem OAI.Erdos3.positiveRetainedFrequencyLog_mono_budget line 76
  13. theorem OAI.Erdos3.positiveRetainedDenominatorLog_mono_budget line 82
  14. theorem OAI.Erdos3.positiveRetainedComplexityLog_mono_budget line 88
  15. theorem OAI.Erdos3.majorArcSpectrumLog_mono_budget line 94
  16. theorem OAI.Erdos3.uniformBlockAccuracyLog_mono_budget line 100
  17. theorem OAI.Erdos3.uniformSpectrumSizeLog_mono_budget line 106
  18. theorem OAI.Erdos3.uniformRetainedBiasLog_mono_budget line 112
  19. theorem OAI.Erdos3.uniformSpectrumCardLog_mono_budget line 118
  20. theorem OAI.Erdos3.uniformRetainedFrequencyLog_mono_budget line 124
  21. theorem OAI.Erdos3.uniformRetainedDenominatorLog_mono_budget line 130
  22. theorem OAI.Erdos3.slicedGridSiteLog_mono line 136
  23. theorem OAI.Erdos3.slicedGridSiteLog_eval line 144
  24. theorem OAI.Erdos3.exists_slicedGridSiteLog_uniform_budget line 150
  25. theorem OAI.Erdos3.VectorPolynomial.slicedFixedZeroGeometryLog_mono line 189
  26. theorem OAI.Erdos3.VectorPolynomial.slicedFixedZeroGeometryLog_eval₂ line 201
  27. theorem OAI.Erdos3.uniformProductAccuracyLog_mono line 213
  28. theorem OAI.Erdos3.uniformProductAccuracyLog_eval₂ line 221
  29. def OAI.Erdos3.VectorPolynomial.slicedFixedUniformSitePolynomial line 237
  30. theorem OAI.Erdos3.VectorPolynomial.slicedFixedUniformSitePolynomial_eval line 240
  31. theorem OAI.Erdos3.VectorPolynomial.slicedFixedUniformSiteLog_mono line 246
  32. theorem OAI.Erdos3.VectorPolynomial.exists_slicedFixedUniform_polynomial_budget line 255
  33. theorem OAI.Erdos3.VectorPolynomial.exists_slicedFixedUniform_tail_polynomial_budget line 316
  34. def OAI.Erdos3.VectorPolynomial.forecastSlicedEarlyDiagonalBudget line 335
  35. def OAI.Erdos3.VectorPolynomial.forecastSlicedEarlyPolynomial line 353
  36. theorem OAI.Erdos3.VectorPolynomial.forecastSlicedEarlyPolynomial_eval line 372
  37. theorem OAI.Erdos3.forecastSlicedEarlyLogs_le_diagonal line 393
  38. theorem OAI.Erdos3.exists_forecastSlicedEarly_polynomial_budget line 517
  39. theorem OAI.Erdos3.forecastSlicedEarlyLogs_le_diagonal_of_dimensions line 583
  40. theorem OAI.Erdos3.exists_forecastSlicedEarly_unrestricted_polynomial_budget line 707