OAI/Combinatorics/Progressions/Estimates/AllocatedCanonicalNormalizer.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealCutoff_complex_mul line 28
  2. theorem OAI.Erdos3.VectorPolynomial.allocatedRowIdealApproximation_error line 46
  3. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_row_ideal_site_approximation line 95
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_on_chart line 180
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteChartFactor_zero_of_cutoff_zero line 192
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRowIdealProduct line 217
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRowIdealProduct_error line 241
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_buffered_row_ideal_approximation line 265
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedRowIdealProduct_error_cutoff line 347
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_buffered_row_ideal_approximation_cutoff line 370
  11. theorem OAI.Erdos3.VectorPolynomial.mixedCoveredRowsOfSites_chart_value line 439
  12. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_mem_chart line 486
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedProductSiteCutoff_zero_outside line 504
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedBufferedSiteProduct_zero_outside line 511
  15. def OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer line 551
  16. def OAI.Erdos3.VectorPolynomial.allocatedProductMaskedIdealCoefficient line 571
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedProductMaskedIdealCoefficient_bound line 592
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedProductPrefactor_masked_error line 605
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedGridJetScale_natural_ratio line 697
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_pos line 716
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_inv_eq line 725
  22. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_inv_le line 778
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedProductIdealNormalizer_inv_le_exp line 835
  24. def OAI.Erdos3.VectorPolynomial.allocatedCanonicalNormalizerLog line 862
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCanonicalIdealNormalizer_pre_bound line 878