OAI/Combinatorics/Progressions/Dynamics/AllocatedProductCoarseBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.recenteredShiftLog line 13
  2. theorem OAI.Erdos3.recenteredShiftLog_nonneg line 17
  3. theorem OAI.Erdos3.recenteredShiftFactor_exp_bound line 24
  4. theorem OAI.Erdos3.exists_recenteredShiftLog_bound line 73
  5. def OAI.Erdos3.recenteredMesh line 82
  6. theorem OAI.Erdos3.recenteredMesh_spec line 85
  7. theorem OAI.Erdos3.recenteredComparisonError_le_exp line 108
  8. def OAI.Erdos3.VectorPolynomial.allocatedOriginalCoverAccuracy line 146
  9. def OAI.Erdos3.VectorPolynomial.allocatedOriginalMassLog line 149
  10. def OAI.Erdos3.VectorPolynomial.allocatedOriginalCoverMesh line 153
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalCoverMesh_spec line 156
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalCover_error_bound line 172
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalCover_error_bound_mesh line 261
  14. def OAI.Erdos3.VectorPolynomial.allocatedProductCoarseMesh line 352
  15. def OAI.Erdos3.VectorPolynomial.allocatedProductCoarseInput line 357
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedProductCoarseMesh_partition_budget line 361
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalProfile_normalized_mass_bound line 479