OAI/Combinatorics/Progressions/Geometry/AllocatedAmbientBoxTests.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredSpatialTwist line 34
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredSpatialTwist_bound line 43
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredResidueWeight_expansion line 60
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredSpatialCoefficient_sum_le line 82
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredSpatial_sum_expansion line 101
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredSpatial_mixedMass_le line 120
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredClippedFullGridCover_expansion line 198
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredProductFullGridCover_expansion line 296
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedRecentered_exists_twisted_source line 383
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialAssembly line 497
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialAssembly_coefficient_mass line 555
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialAssembly_pointwise line 627
  13. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialApproximation line 747
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialApproximation_window_error line 769
  15. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSiteFactor line 891
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSiteFactor_sum line 905
  17. def OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSpatialApproximation line 1001
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredMaskedSpatialApproximation_normalized line 1022
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedRecenteredNormalizedSiteFactor_norm line 1122
  20. def OAI.Erdos3.VectorPolynomial.allocatedAmbientMaskedSpatialApproximation line 1213
  21. def OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation line 1226
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientMaskedSpatialApproximation_reconstruction line 1245
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation_reconstruction line 1252
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientMaskedSpatialApproximation_normalized line 1262
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation_test_congr line 1376
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation_zero_of_test_zero line 1396
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation_testExtension_eq line 1417
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedAmbientNormalizedSpatialApproximation_testExtension_nonzero_mem_box line 1426