OAI/NumberTheory/DirichletL/QuadraticSieve/LogarithmicLoss.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.lifting_annular_scale_bounds line 76
  2. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.lifted_annular_selected line 83
  3. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.ball_selected_high line 140
  4. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.low_threshold line 174
  5. theorem OAI.SecondPassArithmetic.globalCutoffRatio_le line 230
  6. theorem OAI.SecondPassArithmetic.globalNormCaps_polynomial line 248
  7. theorem OAI.SecondPassArithmetic.normLogBin_le_log_upper line 292
  8. theorem OAI.SecondPassArithmetic.globalLogBox_card_le_log line 297
  9. theorem OAI.SecondPassArithmetic.globalLogBox_card_polynomial_log line 311
  10. theorem OAI.SecondPassArithmetic.globalLogRep_le_upper line 326
  11. theorem OAI.SecondPassArithmetic.globalBinLossScale_cancel line 339
  12. theorem OAI.SecondPassArithmetic.globalBinLossScale_polynomial line 348
  13. theorem OAI.CanonicalQuadraticSieve.sieveNorm_small_columns line 378
  14. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.shell_threshold line 392
  15. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.improve line 461
  16. theorem OAI.CanonicalQuadraticSieve.hasSieveExponent_one line 471
  17. theorem OAI.CanonicalQuadraticSieve.sieveNorm_sharp line 474
  18. theorem OAI.CanonicalQuadraticSieve.finite_family_quadratic_large_sieve line 479
  19. theorem OAI.SecondPassArithmetic.globalLogFactor_small_power line 506
  20. theorem OAI.SecondPassArithmetic.globalLogBox_card_small_power line 538
  21. theorem OAI.SecondPassArithmetic.globalLogBox_total_loss line 549
  22. theorem OAI.SecondPassArithmetic.globalBinLossScale_nonneg line 582
  23. theorem OAI.SecondPassArithmetic.globalLogBox_radial_decay line 590