OAI/Combinatorics/Progressions/Sampling/AllocatedOriginalSampleForecastAtom.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_forecast_individual_period_factor line 15
  2. theorem OAI.Erdos3.VectorPolynomial.exists_forecast_smooth_individual_period_factor line 121
  3. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity line 235
  4. def OAI.Erdos3.VectorPolynomial.allocatedOriginalForecastCap line 239
  5. def OAI.Erdos3.VectorPolynomial.allocatedOriginalForecastLip line 243
  6. def OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleNormalizedForecast line 257
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_ae_probability line 263
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_ae_bounds line 274
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleNormalizedForecast_ae_bounds line 286
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_ae_support line 304
  11. def OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisRowCap line 332
  12. def OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisLiftCap line 337
  13. def OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisLiftLip line 340
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLiftRowCap_eq_allAxis line 348
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLift_prod_add_one_le_allAxis line 352
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLift_prod_le_allAxis line 362
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLift_sum_lip_le_allAxis line 371
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathLift_lip_le_allAxis line 382
  19. def OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisCap line 393
  20. def OAI.Erdos3.VectorPolynomial.allocatedForecastAllAxisLip line 397
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalForecastCap_le_allAxis line 411
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalForecastLip_le_allAxis line 418
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSampleForecastDensity_coordinate_bound_two line 469
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedOriginalSampleForecastAtom line 529
  25. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedOriginalSampleForecastAtom_supported line 565