OAI/NumberTheory/DirichletL/QuadraticSieve/PrincipalTruncation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CanonicalQuadraticSieve.lowPrincipalIdeal line 80
  2. def OAI.CanonicalQuadraticSieve.lowPrincipalLattice line 85
  3. theorem OAI.CanonicalQuadraticSieve.lowPrincipalLattice_eq_six_ideal line 89
  4. theorem OAI.CanonicalQuadraticSieve.lowPrincipalIdeal_eq_lattice line 144
  5. theorem OAI.CanonicalQuadraticSieve.originalPairLow_principal_lattice line 150
  6. def OAI.CanonicalQuadraticSieve.lowPrincipalMain line 182
  7. def OAI.CanonicalQuadraticSieve.lowPrincipalMiddle line 186
  8. def OAI.CanonicalQuadraticSieve.lowPrincipalError line 190
  9. theorem OAI.CanonicalQuadraticSieve.lowPrincipalIdeal_truncated line 194
  10. theorem OAI.CanonicalQuadraticSieve.gcdMaskPrimes_card_le line 211
  11. theorem OAI.CanonicalQuadraticSieve.gcdMaskPrimes_subsets_bound line 216
  12. theorem OAI.CanonicalQuadraticSieve.lowPrincipalError_bound line 227
  13. theorem OAI.CanonicalQuadraticSieve.tsum_admissible_norm_cutoff line 260
  14. theorem OAI.CanonicalQuadraticSieve.originalPairLow_principal_finite line 284
  15. theorem OAI.SecondPassArithmetic.activeGaussRowFactor_norm_le_one line 311
  16. theorem OAI.SecondPassArithmetic.secondPairRadialMode_tail line 328
  17. def OAI.SecondPassArithmetic.secondExpansionPool line 380
  18. theorem OAI.SecondPassArithmetic.mem_secondExpansionPool line 385
  19. theorem OAI.SecondPassArithmetic.sum_secondExpansionPool line 398
  20. def OAI.SecondPassArithmetic.secondExpansionSector line 438
  21. theorem OAI.SecondPassArithmetic.sum_secondExpansionSector line 442
  22. theorem OAI.SecondPassArithmetic.secondExpansionSector_valid line 463
  23. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_expansionPool line 472
  24. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_fixed_sectors line 500
  25. theorem OAI.SecondPassArithmetic.normalized_truncatedSecondSource_eq_raw_sectors line 521
  26. theorem OAI.SecondPassArithmetic.secondPairRadialMode_summable_norm line 571
  27. theorem OAI.SecondPassArithmetic.secondPairRadialMode_remainder line 592