OAI/Combinatorics/Progressions/Sampling/ForecastGoodPathMeanNorm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.forecastUniformAtomTransfer line 13
  2. theorem OAI.Erdos3.forecastUniformAtomTransfer_outer line 59
  3. theorem OAI.Erdos3.forecastBoundedSignalTransfer line 89
  4. theorem OAI.Erdos3.exists_forecast_detecting_atom line 135
  5. theorem OAI.Erdos3.forecastUniformAtomTransfer_integral_of_exists line 170
  6. theorem OAI.Erdos3.forecastUniformAtomTransfer_integral line 200
  7. theorem OAI.Erdos3.norm_integral_le_good_bound_add_exception line 236
  8. theorem OAI.Erdos3.forecastUniformAtomTransfer_integral_of_exists_off_exception line 264
  9. theorem OAI.Erdos3.integral_norm_le_good_bound_add_exception line 307
  10. theorem OAI.Erdos3.forecastUniformAtomTransfer_mean_norm_of_exists_off_exception line 334
  11. theorem OAI.Erdos3.physicalForecastComparison_mean_norm line 377
  12. theorem OAI.Erdos3.integral_norm_off_exception_le line 422
  13. theorem OAI.Erdos3.physicalForecastComparison_good_mean_norm line 442