OAI/NumberTheory/DirichletL/QuadraticSieve/PrimePools.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CanonicalQuadraticSieve.canonicalPoolMaximal line 81
  2. theorem OAI.CanonicalQuadraticSieve.poolGood line 86
  3. theorem OAI.CanonicalQuadraticSieve.poolOdd line 91
  4. def OAI.CanonicalQuadraticSieve.poolPrimary line 96
  5. theorem OAI.CanonicalQuadraticSieve.poolPrimary_ne_zero line 98
  6. theorem OAI.CanonicalQuadraticSieve.poolPrimary_span line 101
  7. theorem OAI.CanonicalQuadraticSieve.primaryPrime_eq_primaryGenerator line 105
  8. theorem OAI.CanonicalQuadraticSieve.primaryGenerator_eq_poolProduct line 112
  9. theorem OAI.CanonicalQuadraticSieve.quadraticRow_eq_pool line 124
  10. theorem OAI.CanonicalQuadraticSieve.poolPrimary_coprime line 131
  11. theorem OAI.CanonicalQuadraticSieve.poolPrimary_good line 138
  12. theorem OAI.CanonicalQuadraticSieve.poolPrimary_odd line 141
  13. theorem OAI.CanonicalQuadraticSieve.quadraticRow_eq_primaryPool line 146
  14. theorem OAI.CanonicalQuadraticSieve.quadraticRow_eq_primeSubset line 156
  15. theorem OAI.CanonicalQuadraticSieve.idealSupport_disjoint_of_coprime line 162
  16. theorem OAI.CanonicalQuadraticSieve.primaryGenerator_unit_mod_four line 173
  17. theorem OAI.CanonicalQuadraticSieve.columnRay_idealQuotient_eq line 185
  18. theorem OAI.CanonicalQuadraticSieve.quadraticRow_eq_primarySubset line 212
  19. theorem OAI.CanonicalQuadraticSieve.quadraticRow_zero_of_ne_one line 227
  20. theorem OAI.CanonicalQuadraticSieve.quadratic_pair_zero_of_nontrivial line 245
  21. theorem OAI.CanonicalQuadraticSieve.quadratic_pair_tsum_remove_zero line 251
  22. def OAI.SecondPassArithmetic.radialPairKernel line 276
  23. theorem OAI.SecondPassArithmetic.actualSecondKernel_eq_coupled line 283
  24. theorem OAI.SecondPassArithmetic.secondChildKernelPair_fixed_pool line 303
  25. theorem OAI.SecondPassArithmetic.actualSecondKernel_eq_coupled_children line 340
  26. def OAI.SecondPassIntegration.elementNorm line 361
  27. lemma OAI.SecondPassIntegration.elementNorm_pos line 363
  28. lemma OAI.SecondPassIntegration.elementNorm_mul line 366
  29. theorem OAI.SecondPassIntegration.seven_radial_ratio line 369
  30. theorem OAI.SecondPassIntegration.second_radial_dyadic_argument line 384
  31. def OAI.SecondPassIntegration.conjugateProfile line 405
  32. lemma OAI.SecondPassIntegration.conjugateProfile_apply line 408
  33. theorem OAI.SecondPassIntegration.normalizedColumn_pair_union line 411
  34. theorem OAI.SecondPassArithmetic.active_row_norm_le_one line 458
  35. def OAI.SecondPassArithmetic.secondPairRadialMode line 465
  36. theorem OAI.SecondPassArithmetic.secondPairRadialMode_summable line 472
  37. theorem OAI.SecondPassArithmetic.maskedSecondDual_eq_modes line 504
  38. def OAI.SecondPassArithmetic.residualSecondMode line 516
  39. theorem OAI.SecondPassArithmetic.residualSecondMode_summable line 525
  40. def OAI.SecondPassArithmetic.secondFrequencyKernel line 551
  41. theorem OAI.SecondPassArithmetic.residualSecondMode_tsum line 560
  42. def OAI.SecondPassArithmetic.secondOverlapBlock line 584
  43. theorem OAI.SecondPassArithmetic.secondOverlapBlock_eq_modes line 590
  44. theorem OAI.SecondPassArithmetic.residualSecondMode_eq_frequencyKernel line 648