OAI/Combinatorics/Progressions/Sampling/ActualForecastDataNativeProductBudget.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.forecastNormalizedTwist_mem_fixed_native_family line 13
  2. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedTwist_lipschitz_exp_bound line 39
  3. theorem OAI.Erdos3.VectorPolynomial.forecastBufferedTwist_mem_early_native_family line 80
  4. theorem OAI.Erdos3.VectorPolynomial.forecastFiniteTwists_common_family line 109
  5. theorem OAI.Erdos3.VectorPolynomial.centeredForecastTwist_mem_common_family line 154
  6. theorem OAI.Erdos3.VectorPolynomial.centeredForecastTwist_eval_mem_common_family line 171
  7. theorem OAI.Erdos3.VectorPolynomial.centeredForecastTwist_sum_eq line 194
  8. theorem OAI.Erdos3.VectorPolynomial.exists_centered_forecast_twist_model line 214
  9. theorem OAI.Erdos3.VectorPolynomial.exists_fixedLaw_centered_forecast_twist_model line 353
  10. structure OAI.Erdos3.VectorPolynomial.ActualForecastData line 488
  11. def OAI.Erdos3.VectorPolynomial.ActualForecastData.zero line 512
  12. theorem OAI.Erdos3.VectorPolynomial.ActualForecastData.zero_target line 522
  13. theorem OAI.Erdos3.VectorPolynomial.ActualForecastData.zero_centerConstant line 525
  14. def OAI.Erdos3.VectorPolynomial.actualForecastOptionFamily line 533
  15. theorem OAI.Erdos3.VectorPolynomial.actualForecastOptionFamily_some line 539
  16. theorem OAI.Erdos3.VectorPolynomial.actualForecastOptionFamily_none_target line 543
  17. theorem OAI.Erdos3.VectorPolynomial.actualForecastOptionFamily_none_centerConstant line 547
  18. theorem OAI.Erdos3.VectorPolynomial.actualForecastOptionFamily_bounds line 552
  19. theorem OAI.Erdos3.VectorPolynomial.ActualForecastData.native_product_lipschitz_bound line 580
  20. theorem OAI.Erdos3.VectorPolynomial.ActualForecastData.native_product_bounds line 617