OAI/NumberTheory/DirichletL/QuadraticSieve/PoissonComparison.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.hasSieveExponent_one_of_approximation line 77
  2. def OAI.CanonicalQuadraticSieve.bootstrapExponent line 112
  3. theorem OAI.CanonicalQuadraticSieve.bootstrapExponent_gt_one line 114
  4. theorem OAI.CanonicalQuadraticSieve.bootstrapExponent_le_two line 119
  5. theorem OAI.CanonicalQuadraticSieve.bootstrapExponent_step line 126
  6. theorem OAI.CanonicalQuadraticSieve.hasSieveExponent_one_of_improvement line 133
  7. def OAI.CanonicalQuadraticSieve.divisorTwist line 153
  8. def OAI.CanonicalQuadraticSieve.centeredRetainedDual line 156
  9. def OAI.CanonicalQuadraticSieve.centeredMaskedSource line 164
  10. def OAI.CanonicalQuadraticSieve.maskedPoissonDifference line 171
  11. lemma OAI.CanonicalQuadraticSieve.finite_centering_identity line 177
  12. theorem OAI.CanonicalQuadraticSieve.maskedPoissonDifference_centered line 184
  13. theorem OAI.CanonicalQuadraticSieve.maskedPoissonDifference_norm_le line 201
  14. theorem OAI.CanonicalQuadraticSieve.divisorTwist_norm_le line 244
  15. theorem OAI.CanonicalQuadraticSieve.retainedDualMajorant_coefficient_scale_le line 249
  16. theorem OAI.CanonicalQuadraticSieve.centeredRetainedDual_sum_bound line 275
  17. def OAI.CanonicalQuadraticSieve.poissonComparisonMajorant line 317
  18. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.masked_poisson_complete line 333
  19. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_energy_eq line 389
  20. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_energy_ray_sum line 402
  21. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_energy_divisor_sum line 420
  22. theorem OAI.CanonicalQuadraticSieve.gcdRaySupport_weighted_sum_bound line 441
  23. theorem OAI.CanonicalQuadraticSieve.divisorEnergyFactor_diagonal line 463
  24. theorem OAI.CanonicalQuadraticSieve.poissonComparisonMajorant_energy_factor line 471
  25. def OAI.SecondPassArithmetic.globalSecondOuterWeight line 496
  26. theorem OAI.SecondPassArithmetic.globalSecondOuterWeight_squarefree line 507
  27. theorem OAI.SecondPassArithmetic.globalSecondOuterWeight_norm_le line 524
  28. def OAI.SecondPassArithmetic.globalPooledOuterBound line 547
  29. theorem OAI.SecondPassArithmetic.globalSecondOuterWeight_bin_bound line 551