OAI/Combinatorics/Progressions/Sampling/AllocatedFixedPathForecastErrorBudget.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.twoTermErrorWidth_le_error line 12
  2. theorem OAI.Erdos3.spatialTupleTolerance_le_error line 17
  3. theorem OAI.Erdos3.normalizedTupleNarrowWidth_le_exp line 29
  4. theorem OAI.Erdos3.normalizedTupleNarrowWidth_mul_le_exp line 45
  5. def OAI.Erdos3.allocatedJointForecastError line 64
  6. theorem OAI.Erdos3.jointForecast_mesh_prefactor_bound line 71
  7. theorem OAI.Erdos3.jointForecast_spatial_prefactor_bound line 106
  8. theorem OAI.Erdos3.jointForecast_log_ge_parameter line 143
  9. theorem OAI.Erdos3.jointForecast_scaled_small line 146
  10. theorem OAI.Erdos3.jointForecast_small_half line 154
  11. theorem OAI.Erdos3.allocatedJointForecastError_le_prefactor line 159
  12. theorem OAI.Erdos3.allocatedJointForecastError_absorb line 188
  13. theorem OAI.Erdos3.exists_allocatedJointForecastErrorBudget line 217
  14. theorem OAI.Erdos3.allocatedJointForecast_mesh_of_exp_size line 269
  15. def OAI.Erdos3.fixedPathForecastError line 316
  16. theorem OAI.Erdos3.fixedPathForecastError_eq_joint line 323
  17. theorem OAI.Erdos3.fixedPathForecastError_le_prefactor line 333
  18. theorem OAI.Erdos3.fixedPath_scaled_small line 378
  19. theorem OAI.Erdos3.fixedPathForecastError_absorb line 386
  20. theorem OAI.Erdos3.exists_fixedPathForecastErrorBudget line 409
  21. theorem OAI.Erdos3.exists_normalizedTupleForecastWidth_budget line 467
  22. theorem OAI.Erdos3.fixedPath_scalarCubeBoundary_empty line 500
  23. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedFixedPathForecastErrorBudget line 513