OAI/Combinatorics/Progressions/Estimates/AllocatedSlicedCoarseSource.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_reconstruction_shift line 12
  2. def OAI.Erdos3.VectorPolynomial.allocatedTranslatedProfileTerm line 74
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedProfileTerm_translate line 90
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedReference_translate line 129
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedProfileTerm_translate_at line 200
  6. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm line 290
  7. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileMass line 303
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedTranslatedProfileTerm_recenter_error line 335
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedTranslatedReference_recenter_error line 418
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedResidueWeightedReference_recenter_error line 442
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileMass_nonneg line 505
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_mesh_error line 522
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_mesh_error_law line 583
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProfileTerm_remesh_law line 607
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredReference_mesh_error line 644
  16. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredCoarseMesh line 715
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredReference_coarse_comparison_law line 722
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredReference_coarse_comparison line 790
  19. def OAI.Erdos3.VectorPolynomial.allocatedEarlyRecenteredMesh line 823
  20. def OAI.Erdos3.VectorPolynomial.allocatedEarlyCoarseInput line 828
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedEarlyCoarseInput_bounds line 833
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedEarlyRecenteredMesh_partition_budget line 851
  23. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedEarlyCoarseLog_bound line 963
  24. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedEarlyRecenteredMesh_budget line 982
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedRecentered_early_coarse_source_law line 1045