OAI/NumberTheory/DirichletL/QuadraticSieve/GcdReduction.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.gcdPool line 77
  2. theorem OAI.CanonicalQuadraticSieve.mem_gcdPool line 80
  3. theorem OAI.CanonicalQuadraticSieve.gcdPool_ne_zero line 84
  4. theorem OAI.CanonicalQuadraticSieve.energy_eq_gcd_blocks line 92
  5. theorem OAI.CanonicalQuadraticSieve.energy_le_gcd_blocks line 121
  6. theorem OAI.CanonicalQuadraticSieve.highKernel_large_gcd_blocks line 130
  7. theorem OAI.CanonicalQuadraticSieve.highKernel_energy_gcd_reduction line 165
  8. def OAI.FiniteSieveRestriction.sectorCoefficient line 186
  9. theorem OAI.FiniteSieveRestriction.sectorCoefficient_energy line 189
  10. theorem OAI.FiniteSieveRestriction.norm_sum_square_card line 201
  11. theorem OAI.FiniteSieveRestriction.sector_energy_bound line 208
  12. def OAI.CanonicalQuadraticSieve.columnRay line 234
  13. def OAI.CanonicalQuadraticSieve.rayGcdBlock line 236
  14. theorem OAI.CanonicalQuadraticSieve.rayGcdBlock_eq line 241
  15. theorem OAI.CanonicalQuadraticSieve.highKernel_energy_ray_gcd_reduction line 260
  16. theorem OAI.FiniteSieveOperator.quadratic_form_bound line 296
  17. def OAI.CanonicalQuadraticSieve.rayGramMatrix line 322
  18. theorem OAI.CanonicalQuadraticSieve.rayGcdBlock_eq_quadraticForm line 328
  19. theorem OAI.CanonicalQuadraticSieve.rayGcdBlock_norm_le line 346
  20. def OAI.CanonicalQuadraticSieve.rayThirdNorm line 352
  21. def OAI.CanonicalQuadraticSieve.thirdNorm line 357
  22. theorem OAI.CanonicalQuadraticSieve.rayThirdNorm_bddAbove line 360
  23. theorem OAI.CanonicalQuadraticSieve.rayThirdNorm_nonneg line 374
  24. theorem OAI.CanonicalQuadraticSieve.thirdNorm_nonneg line 381
  25. theorem OAI.CanonicalQuadraticSieve.rayThirdNorm_bound line 384
  26. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_le_thirdNorm line 396
  27. def OAI.CanonicalQuadraticSieve.weightedGcdBlock line 432
  28. theorem OAI.CanonicalQuadraticSieve.highKernel_weightedGcdBlock_bound line 436
  29. theorem OAI.CanonicalQuadraticSieve.highKernel_large_weighted_gcd_blocks line 478
  30. theorem OAI.FiniteSieveRestriction.sector_weighted_energy_bound line 519
  31. theorem OAI.CanonicalQuadraticSieve.weighted_energy_eq_gcd_blocks line 544
  32. theorem OAI.CanonicalQuadraticSieve.weighted_energy_le_gcd_blocks line 554
  33. theorem OAI.CanonicalQuadraticSieve.highKernel_weighted_energy_gcd_reduction line 563
  34. def OAI.CanonicalQuadraticSieve.weightedRayGcdBlock line 583
  35. theorem OAI.CanonicalQuadraticSieve.highKernel_weighted_energy_ray_gcd_reduction line 589
  36. def OAI.CanonicalQuadraticSieve.smoothHighWeight line 625
  37. def OAI.CanonicalQuadraticSieve.smoothHighEnergy line 628
  38. theorem OAI.CanonicalQuadraticSieve.highKernel_energy_le_smooth line 632
  39. def OAI.CanonicalQuadraticSieve.smoothRayGcdBlock line 653
  40. theorem OAI.CanonicalQuadraticSieve.highKernel_energy_smooth_gcd_reduction line 658