OAI/NumberTheory/DirichletL/QuadraticSieve/PrincipalDifference.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.normalizedPair_boundary_term line 81
  2. def OAI.CanonicalQuadraticSieve.actualPrincipalDifference line 106
  3. theorem OAI.CanonicalQuadraticSieve.actualPrincipalDifference_bound line 114
  4. def OAI.CanonicalQuadraticSieve.middleRatio line 179
  5. theorem OAI.CanonicalQuadraticSieve.middleRatio_bounds line 181
  6. theorem OAI.CanonicalQuadraticSieve.middleRatio_log_bound line 212
  7. theorem OAI.CanonicalQuadraticSieve.middleRatio_argument line 222
  8. theorem OAI.CanonicalQuadraticSieve.actual_middle_radial_block_bound line 246
  9. theorem OAI.SecondPassArithmetic.firstCoreInputRow_smoothed_mode line 305
  10. theorem OAI.SecondPassArithmetic.firstCoreInputRow_smoothed_truncated line 342
  11. theorem OAI.SecondPassArithmetic.firstCoreInputRow_finite_le_truncated_tail line 365
  12. lemma OAI.SecondPassIntegration.childEnergy_eq_difference line 412
  13. theorem OAI.SecondPassIntegration.densityChildEnergy_polynomial_bound line 423
  14. def OAI.SecondPassArithmetic.residualPairWeight line 490
  15. theorem OAI.SecondPassArithmetic.residualSecondMode_tail_eq line 495
  16. def OAI.SecondPassArithmetic.residualTailCost line 523
  17. theorem OAI.SecondPassArithmetic.residualSecondMode_tail_bound line 532
  18. theorem OAI.SecondPassArithmetic.secondSourceTail_bound line 562
  19. theorem OAI.SecondPassArithmetic.primeProductNorm_eq_ideal_norm line 608
  20. theorem OAI.SecondPassArithmetic.primeProductNorm_ge_one line 615
  21. theorem OAI.SecondPassArithmetic.primeProductNorm_mono line 624
  22. def OAI.SecondPassArithmetic.boundedPrimeSupports line 632
  23. theorem OAI.SecondPassArithmetic.boundedPrimeSupports_card line 636
  24. theorem OAI.SecondPassArithmetic.normalizedColumn_subset_norm_bound line 655