OAI/NumberTheory/DirichletL/QuadraticSieve/AnnularRecursion.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.weightedRayGramMatrix line 80
  2. theorem OAI.CanonicalQuadraticSieve.weightedRayGcdBlock_eq_quadraticForm line 88
  3. theorem OAI.CanonicalQuadraticSieve.smoothRayGcdBlock_norm_le line 110
  4. def OAI.CanonicalQuadraticSieve.smoothRayThirdNorm line 119
  5. def OAI.CanonicalQuadraticSieve.smoothThirdNorm line 123
  6. theorem OAI.CanonicalQuadraticSieve.smoothRayThirdNorm_bddAbove line 126
  7. theorem OAI.CanonicalQuadraticSieve.smoothRayThirdNorm_nonneg line 139
  8. theorem OAI.CanonicalQuadraticSieve.smoothThirdNorm_nonneg line 146
  9. theorem OAI.CanonicalQuadraticSieve.smoothRayThirdNorm_bound line 149
  10. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_le_smoothThirdNorm line 158
  11. def OAI.CanonicalQuadraticSieve.rayPairValue line 195
  12. theorem OAI.CanonicalQuadraticSieve.rayPairValue_eq line 201
  13. theorem OAI.CanonicalQuadraticSieve.smoothHighWeight_eq_zero line 210
  14. theorem OAI.CanonicalQuadraticSieve.smoothRayGcdBlock_eq_finite line 221
  15. theorem OAI.CanonicalQuadraticSieve.smoothRayGcdBlock_eq_tsum line 227
  16. def OAI.CanonicalQuadraticSieve.highKernelShellRange line 257
  17. theorem OAI.CanonicalQuadraticSieve.mem_highKernelShellRange line 260
  18. def OAI.CanonicalQuadraticSieve.highKernelShellMatrix line 264
  19. def OAI.CanonicalQuadraticSieve.highKernelShellNorm line 267
  20. theorem OAI.CanonicalQuadraticSieve.highKernelShellNorm_nonneg line 269
  21. theorem OAI.CanonicalQuadraticSieve.exists_dyadic_shell line 271
  22. theorem OAI.CanonicalQuadraticSieve.highKernel_dyadic_cover line 287
  23. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_le_dyadic_shells line 296
  24. def OAI.QuadraticInitialBound.annularSieveBump line 337
  25. def OAI.QuadraticInitialBound.annularSieveCutoff line 343
  26. theorem OAI.QuadraticInitialBound.annularSieveCutoff_apply line 350
  27. theorem OAI.QuadraticInitialBound.annularSieveBump_eq_one line 352
  28. theorem OAI.QuadraticInitialBound.annularSieveBump_zero_of_le line 358
  29. theorem OAI.QuadraticInitialBound.annularSieveBump_zero_of_ge line 364
  30. theorem OAI.QuadraticInitialBound.annularSieveCutoff_zero line 370
  31. def OAI.CanonicalQuadraticSieve.annularHighWeight line 381
  32. def OAI.CanonicalQuadraticSieve.annularHighEnergy line 384
  33. theorem OAI.CanonicalQuadraticSieve.highKernelShell_energy_le_annular line 388
  34. def OAI.CanonicalQuadraticSieve.annularRayGcdBlock line 412
  35. theorem OAI.CanonicalQuadraticSieve.highKernelShell_energy_annular_gcd_reduction line 417
  36. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_norm_le line 439
  37. def OAI.CanonicalQuadraticSieve.annularRayThirdNorm line 448
  38. def OAI.CanonicalQuadraticSieve.annularThirdNorm line 452
  39. theorem OAI.CanonicalQuadraticSieve.annularRayThirdNorm_bddAbove line 455
  40. theorem OAI.CanonicalQuadraticSieve.annularRayThirdNorm_nonneg line 468
  41. theorem OAI.CanonicalQuadraticSieve.annularThirdNorm_nonneg line 475
  42. theorem OAI.CanonicalQuadraticSieve.annularRayThirdNorm_bound line 478
  43. theorem OAI.CanonicalQuadraticSieve.highKernelShellNorm_le_annularThirdNorm line 487
  44. theorem OAI.CanonicalQuadraticSieve.annularHighWeight_eq_zero line 523
  45. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_eq_finite line 528
  46. theorem OAI.CanonicalQuadraticSieve.annularRayGcdBlock_eq_tsum line 534
  47. theorem OAI.FiniteSieveOperator.bounded_entry_squared_norm_le line 564
  48. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_trivial line 588
  49. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_short_columns line 605
  50. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_le_annular_recursion line 614
  51. theorem OAI.CanonicalQuadraticSieve.sieveNorm_le_annular_recursion line 626