OAI/Combinatorics/Progressions/Sampling/ForecastContinuousRetainedExpansion.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.forecastSiteMixtureCoefficient line 21
  2. theorem OAI.Erdos3.forecastSiteMixture_expansion line 25
  3. theorem OAI.Erdos3.forecastSiteMixture_coefficient_mass line 36
  4. theorem OAI.Erdos3.forecastResidueWeight_mass line 47
  5. theorem OAI.Erdos3.forecastSiteMixture_weighted_mass line 55
  6. theorem OAI.Erdos3.forecastSiteMixture_inactive_mass line 67
  7. theorem OAI.Erdos3.forecastSiteMixture_error line 81
  8. theorem OAI.Erdos3.forecastSiteMixture_weighted_error line 91
  9. theorem OAI.Erdos3.forecastSiteMixture_twisted_error line 100
  10. theorem OAI.Erdos3.forecastSiteMixture_twisted_expansion line 117
  11. theorem OAI.Erdos3.forecastSiteMixture_factor_bounds line 132
  12. theorem OAI.Erdos3.forecastSiteMixture_factor_support line 161
  13. theorem OAI.Erdos3.forecastSiteMixture_factor_comp_bounds line 173
  14. theorem OAI.Erdos3.forecastSiteMixture_factor_comp_support line 205
  15. def OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity line 252
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_probability_data line 264
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_cap_lipschitz line 274
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_image_law line 296
  19. theorem OAI.Erdos3.VectorPolynomial.fixedPathDensity_unit_factor line 315
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_normalized_bounds line 343
  21. theorem OAI.Erdos3.VectorPolynomial.forecastInactive_actual_smooth_factor_bounds line 408
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_zero_off_ball line 500
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedPathForecastDensity_compact line 514
  24. theorem OAI.Erdos3.forecast_singleton_site_eval line 537
  25. theorem OAI.Erdos3.forecastRetained_normalized_expansion line 546
  26. theorem OAI.Erdos3.forecastRetained_normalized_coefficient_mass line 570
  27. theorem OAI.Erdos3.VectorPolynomial.forecastRetained_actual_smooth_expansion line 624
  28. theorem OAI.Erdos3.VectorPolynomial.forecastRetained_actual_smooth_error line 672
  29. theorem OAI.Erdos3.forecastContinuous_site_factor_bounds line 716
  30. theorem OAI.Erdos3.forecastRetained_continuous_expansion line 753
  31. theorem OAI.Erdos3.forecastRetained_continuous_error line 791