OAI/Combinatorics/Progressions/Estimates/JointCoefficientRetainedTest.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finiteSource_comparison_on_set line 17
  2. theorem OAI.Erdos3.finiteSource_comparison_on_support line 36
  3. theorem OAI.Erdos3.product_density_rounding_error line 68
  4. theorem OAI.Erdos3.finiteSource_product_comparison line 105
  5. theorem OAI.Erdos3.scalarCubeProductDensity_measure line 135
  6. theorem OAI.Erdos3.scalarCubeResidue_pi_imageMeasure line 143
  7. theorem OAI.Erdos3.scalarCubeResidueWeights_pi_riemann line 181
  8. theorem OAI.Erdos3.principalTuple_residue_riemann line 254
  9. theorem OAI.Erdos3.scalarCubeResidueWeights_pi_riemann_on_box line 287
  10. theorem OAI.Erdos3.principalTuple_residue_riemann_on_box line 311
  11. theorem OAI.Erdos3.masked_product_error line 346
  12. theorem OAI.Erdos3.finiteProduct_cap line 364
  13. theorem OAI.Erdos3.finiteProduct_lipschitzOn line 372
  14. theorem OAI.Erdos3.finiteSource_density_l1_of_test_quadrature line 397
  15. theorem OAI.Erdos3.principalTuple_density_l1_of_l1_regular line 434
  16. theorem OAI.Erdos3.principalTuple_residue_retained_riemann line 475
  17. theorem OAI.Erdos3.jointCoefficient_product_error line 510
  18. theorem OAI.Erdos3.jointCoefficient_mean_error line 522
  19. def OAI.Erdos3.jointTupleQuadratureError line 549
  20. theorem OAI.Erdos3.sharedTupleProduct_riemann line 555
  21. theorem OAI.Erdos3.sharedTupleProduct_retained_riemann line 575
  22. theorem OAI.Erdos3.jointCoefficient_average_comparison line 608
  23. theorem OAI.Erdos3.jointCoefficient_principalTuple_comparison line 633
  24. theorem OAI.Erdos3.jointCoefficient_retained_test line 672