OAI/Combinatorics/Progressions/Sampling/PreparedActualSlicedForecastSetup.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.modularInitialRankStrength_eq_forecast line 11
  2. theorem OAI.Erdos3.modularInitialBlockCount_forecast_threshold line 17
  3. theorem OAI.Erdos3.modularInitialAllocation_forecast_parameters line 27
  4. def OAI.Erdos3.VectorPolynomial.actualSlicedForecastDensityBudget line 61
  5. def OAI.Erdos3.VectorPolynomial.actualSlicedForecastDecayBudget line 64
  6. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialSlicedForecastNumerics line 67
  7. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastNumerics line 151
  8. theorem OAI.Erdos3.VectorPolynomial.exists_actualFixedSpatialSlicedForecastNumerics_from_setup line 305
  9. def OAI.Erdos3.VectorPolynomial.actualSlicedForecastModelCapLog line 362
  10. def OAI.Erdos3.VectorPolynomial.actualSlicedForecastModelPeriodLog line 372
  11. theorem OAI.Erdos3.VectorPolynomial.actualSlicedForecastModelPrecision line 382
  12. theorem OAI.Erdos3.VectorPolynomial.exists_actualSlicedForecastModelCapLog_budget line 442
  13. theorem OAI.Erdos3.VectorPolynomial.and_rec_projection line 527

    Distinct definitions of this name: OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastModelLogs.lean:11 (same declaration text), OAI/Combinatorics/Progressions/Sampling/PreparedConcreteSlicedForecastPrecision.lean:11 (same statement text; different proof or body), OAI/Combinatorics/Progressions/Sampling/PreparedSlicedForecastComparisonLogs.lean:212 (same declaration text). Qualify references as OAI.Erdos3.VectorPolynomial.and_rec_projection@path.

  14. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastSpatialBudget line 532
  15. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastBadLog line 537
  16. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastJacobianLog line 540
  17. def OAI.Erdos3.VectorPolynomial.preparedSlicedForecastCapLog line 544
  18. theorem OAI.Erdos3.VectorPolynomial.preparedSliceWidth_inverse line 552
  19. def OAI.Erdos3.VectorPolynomial.preparedActualSlicedForecastSetup line 572