OAI/Combinatorics/Progressions/Sampling/ActualForecastModelPrecision.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.forecastCoverCutoffInput line 17
  2. theorem OAI.Erdos3.VectorPolynomial.forecastCoverCutoffInput_lipschitz line 22
  3. theorem OAI.Erdos3.VectorPolynomial.forecastCoverCutoffInput_physicalGridFactorInput line 28
  4. theorem OAI.Erdos3.exists_forecast_early_approximation_budget line 50
  5. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_early_native_family_budget line 170
  6. def OAI.Erdos3.VectorPolynomial.forecastBufferedFullResidue line 278
  7. def OAI.Erdos3.VectorPolynomial.forecastBufferedCoveredSiteFactor line 283
  8. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedCoveredSiteFactor_on_chart line 294
  9. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedCoveredSiteFactor_zero_of_cutoff_zero line 309
  10. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_buffered_cover_factor line 321
  11. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_buffered_normalized_twist line 421
  12. theorem OAI.Erdos3.VectorPolynomial.forecast_spatial_coordinate_exp_bound line 508
  13. theorem OAI.Erdos3.VectorPolynomial.forecast_ambient_coordinate_cutoff_exp_bounds line 520
  14. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFixedSpatialForecastParameters line 580
  15. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastLogs line 678
  16. def OAI.Erdos3.VectorPolynomial.actualFixedSpatialForecastLogs line 695
  17. structure OAI.Erdos3.VectorPolynomial.ActualFixedSpatialForecastLogs.Nonnegative line 714
  18. theorem OAI.Erdos3.VectorPolynomial.actualFixedSpatialForecastLogs_nonneg line 739
  19. theorem OAI.Erdos3.VectorPolynomial.actualFixedSpatialForecastLogs_period_le_native line 771
  20. theorem OAI.Erdos3.VectorPolynomial.actualFixedSpatialForecastLogs_cap_accuracy_independent line 792
  21. theorem OAI.Erdos3.VectorPolynomial.actualForecastModelPrecision line 799