OAI/NumberTheory/DirichletL/CubicSieve/SupportNorms.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.sourceSupportMobius_norm line 89
  2. theorem OAI.SecondPassArithmetic.primeSubsetGenerator_norm_eq_productNorm line 98
  3. theorem OAI.SecondPassArithmetic.norm_primeProduct_ge_one line 104
  4. theorem OAI.SecondPassArithmetic.secondSourceCommonCoefficient_norm_le_one line 111
  5. theorem OAI.SecondPassArithmetic.secondInputCoefficient_norm_le_test line 127
  6. theorem OAI.SecondPassArithmetic.normalizedColumn_schwartz_bound line 138
  7. theorem OAI.SecondPassArithmetic.residualPairWeight_schwartz_bound line 145
  8. theorem OAI.SecondPassArithmetic.residualPairWeight_support_bounds line 162
  9. theorem OAI.SecondPassArithmetic.tail_radial_scalar_le line 179
  10. theorem OAI.SecondPassArithmetic.sum_pair_indicator line 205
  11. theorem OAI.SecondPassArithmetic.residualTailCost_polynomial line 229
  12. theorem OAI.SecondPassArithmetic.secondSourceTailCost_polynomial line 321
  13. theorem OAI.SecondPassArithmetic.firstCoreSecondCutoff_tail_polynomial line 381
  14. theorem OAI.SecondPassArithmetic.firstCoreSecondCutoff_tail_fixed_source line 416
  15. theorem OAI.SecondPassArithmetic.firstCoreInputRow_complete_finite_transfer line 453
  16. theorem OAI.CanonicalQuadraticSieve.sqrt_scale_shell_upper line 563
  17. theorem OAI.CanonicalQuadraticSieve.original_middle_rectangle_upper line 568
  18. theorem OAI.CanonicalQuadraticSieve.dual_middle_rectangle_upper line 580
  19. def OAI.CanonicalQuadraticSieve.originalMiddleWindowAt line 595
  20. def OAI.CanonicalQuadraticSieve.dualMiddleWindowAt line 606
  21. theorem OAI.CanonicalQuadraticSieve.originalMiddleWindowAt_bounds line 619
  22. theorem OAI.CanonicalQuadraticSieve.dualMiddleWindowAt_bounds line 634
  23. theorem OAI.CanonicalQuadraticSieve.originalMiddleWindowAt_eq_zero line 649
  24. theorem OAI.CanonicalQuadraticSieve.dualMiddleWindowAt_eq_zero line 658