OAI/Combinatorics/Progressions/Sampling/ForecastModularCutoff.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.forecastJointGridPrefactor_le_exp line 9
  2. theorem OAI.Erdos3.exists_rationalForecast_order_cutoff line 93
  3. theorem OAI.Erdos3.rationalForecast_cutoff_power_bound line 117
  4. theorem OAI.Erdos3.exists_forecast_approximation_parameters line 132
  5. theorem OAI.Erdos3.exists_forecast_weighted_approximation_parameters line 174
  6. def OAI.Erdos3.forecastJointGridCutoff line 207
  7. theorem OAI.Erdos3.forecastJointGridCutoff_lower line 210
  8. theorem OAI.Erdos3.forecastJointGridCutoff_pos_unconditional line 213
  9. theorem OAI.Erdos3.forecastJointGridCutoff_one_le line 216
  10. theorem OAI.Erdos3.forecastJointGridCutoff_pos line 219
  11. theorem OAI.Erdos3.forecastJointGridCutoff_le_exp line 222
  12. theorem OAI.Erdos3.forecastJointGridCutoff_div_bound line 231
  13. theorem OAI.Erdos3.forecastJointGridCutoff_tail_le line 244
  14. theorem OAI.Erdos3.exists_forecast_mesh_floor line 257
  15. theorem OAI.Erdos3.exists_active_residue_mesh_floor line 278
  16. def OAI.Erdos3.modularForecastRankConstant line 307
  17. theorem OAI.Erdos3.modularForecastRankConstant_decay line 310
  18. theorem OAI.Erdos3.modularForecastRankConstant_dimension line 318
  19. def OAI.Erdos3.forecastJointGridError line 331
  20. def OAI.Erdos3.forecastJointGridMeshLog line 336
  21. def OAI.Erdos3.forecastJointGridMesh line 339
  22. theorem OAI.Erdos3.forecastJointGridMeshLog_nonneg line 342
  23. theorem OAI.Erdos3.forecastJointGridMesh_bounds line 347
  24. theorem OAI.Erdos3.forecastJointGridError_absorb line 353
  25. theorem OAI.Erdos3.forecastJointGridErrorBudget line 390
  26. theorem OAI.Erdos3.forecastModularCharge_exp_bound line 418
  27. theorem OAI.Erdos3.exists_forecast_modular_approximation_parameters line 435