OAI/Combinatorics/Progressions/Sampling/PrecenterForecastNativePartners.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.CenteredForecastModel line 13
  2. def OAI.Erdos3.CenteredForecastModelBounds line 22
  3. theorem OAI.Erdos3.exists_centeredFiniteForecastModels line 38
  4. theorem OAI.Erdos3.centeredFiniteForecastModels_integral_sum_norm_le line 56
  5. def OAI.Erdos3.centeredFiniteForecastResidualBadSet line 90
  6. theorem OAI.Erdos3.centeredFiniteForecastResidualBadSet_bound line 94
  7. theorem OAI.Erdos3.centeredFiniteForecastModels_residualBadSet line 128
  8. theorem OAI.Erdos3.centeredFiniteForecastModels_centeredResidualBadSet line 157
  9. def OAI.Erdos3.centeredFiniteForecastUniformResidualBadSet line 197
  10. theorem OAI.Erdos3.centeredFiniteForecastUniformResidualBadSet_bound line 203
  11. theorem OAI.Erdos3.centeredFiniteForecastModels_uniformResidualBadSet line 272
  12. def OAI.Erdos3.centeredStagedForecastUniformResidualBadSet line 320
  13. theorem OAI.Erdos3.centeredStagedForecastUniformResidualBadSet_bound line 331
  14. theorem OAI.Erdos3.centeredStagedForecastModels_uniformResidualBadSet line 392
  15. theorem OAI.Erdos3.exists_fixed_linear_model_partners_of_pointwise_error line 437
  16. theorem OAI.Erdos3.exists_precenter_forecast_native_partners line 478