OAI/NumberTheory/DirichletL/QuadraticSieve/AnnularLifting.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.squarefreeHighRange line 82
  2. def OAI.CanonicalQuadraticSieve.annularLift line 85
  3. theorem OAI.CanonicalQuadraticSieve.annularLift_injective line 89
  4. theorem OAI.CanonicalQuadraticSieve.annularLift_properties line 97
  5. theorem OAI.CanonicalQuadraticSieve.annularLift_row_sum line 105
  6. lemma OAI.CanonicalQuadraticSieve.exists_lifted_annular_scale line 118
  7. lemma OAI.CanonicalQuadraticSieve.sum_injective_mask_le line 134
  8. theorem OAI.CanonicalQuadraticSieve.squarefreeHigh_energy_le_annuli line 148
  9. def OAI.CanonicalQuadraticSieve.liftingDivisibleColumns line 206
  10. def OAI.CanonicalQuadraticSieve.liftingQuotientColumn line 209
  11. theorem OAI.CanonicalQuadraticSieve.liftingQuotientColumn_injective line 219
  12. def OAI.CanonicalQuadraticSieve.liftingFreeCoefficient line 226
  13. def OAI.CanonicalQuadraticSieve.liftingDividedCoefficient line 229
  14. theorem OAI.CanonicalQuadraticSieve.liftingFreeCoefficient_coprime line 232
  15. theorem OAI.CanonicalQuadraticSieve.liftingDividedCoefficient_coprime line 239
  16. theorem OAI.CanonicalQuadraticSieve.liftingDividedCoefficient_row_sum line 252
  17. theorem OAI.CanonicalQuadraticSieve.liftingCoefficient_row_split line 259
  18. theorem OAI.CanonicalQuadraticSieve.liftingCoefficient_energy line 275
  19. theorem OAI.CanonicalQuadraticSieve.liftingCoefficient_row_energy line 289
  20. theorem OAI.CanonicalQuadraticSieve.liftingFreeCoefficient_shell line 305
  21. theorem OAI.CanonicalQuadraticSieve.liftingDividedCoefficient_shell line 313
  22. theorem OAI.CanonicalQuadraticSieve.coefficientOnShell_zero_or_scale line 332
  23. def OAI.CanonicalQuadraticSieve.ballQuadraticEnergy line 349
  24. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_low_high line 352
  25. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_lifted_annuli line 373
  26. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_mono line 400
  27. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_coefficientAtScale line 409
  28. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_column_shells line 415
  29. theorem OAI.CanonicalQuadraticSieve.ballQuadraticEnergy_column_shells_at_scale line 424
  30. theorem OAI.CanonicalQuadraticSieve.columnDyadicLength_scale_upper line 436
  31. theorem OAI.CanonicalQuadraticSieve.columnDyadicScale_bounds line 451
  32. theorem OAI.CanonicalQuadraticSieve.gcdPool_admissible line 465
  33. theorem OAI.CanonicalQuadraticSieve.annularHighEnergy_gcd_reduction line 470
  34. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.annular_energy_from_scalar_cost line 483
  35. def OAI.CanonicalQuadraticSieve.cutoffRescaleCoefficient line 543
  36. theorem OAI.CanonicalQuadraticSieve.cutoffRescaleCoefficient_eq line 545
  37. theorem OAI.CanonicalQuadraticSieve.cutoffRescaleCoefficient_bounds line 553
  38. theorem OAI.CanonicalQuadraticSieve.selectedPoissonK_rescale line 572
  39. def OAI.CanonicalQuadraticSieve.largeGcdThreshold line 586
  40. theorem OAI.CanonicalQuadraticSieve.largeGcdThreshold_quotient_power line 588
  41. theorem OAI.CanonicalQuadraticSieve.largeGcdThreshold_bounds line 597
  42. theorem OAI.CanonicalQuadraticSieve.high_kernel_chosen_scale line 613
  43. theorem OAI.CanonicalQuadraticSieve.chosen_large_gcd_main line 631
  44. theorem OAI.CanonicalQuadraticSieve.chosen_large_gcd_full line 637