OAI/NumberTheory/DirichletL/QuadraticSieve/UniformTailBounds.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.product_quadratic_norm_all line 77
  2. theorem OAI.SecondPassArithmetic.full_uniform_secondPairRadialMode_tail line 132
  3. theorem OAI.SecondPassArithmetic.full_uniform_secondPairRadialMode_remainder line 184
  4. theorem OAI.SecondPassArithmetic.full_uniform_residualSecondMode_tail_bound line 223
  5. theorem OAI.SecondPassArithmetic.full_uniform_secondSourceTail_bound line 259
  6. theorem OAI.SecondPassArithmetic.full_uniform_firstCoreSecondCutoff_tail_bound line 300
  7. theorem OAI.SecondPassArithmetic.full_uniform_firstCoreSecondCutoff_tail_polynomial line 349
  8. theorem OAI.SecondPassArithmetic.full_uniform_firstCoreSecondCutoff_tail_fixed_source line 386
  9. structure OAI.InitialMeanSquare.ElementDatum line 422
  10. def OAI.InitialMeanSquare.elementRow line 428
  11. def OAI.InitialMeanSquare.elementLabel line 429
  12. def OAI.InitialMeanSquare.elementObservation line 430
  13. theorem OAI.InitialMeanSquare.element_divisor_injective_on_fiber line 432
  14. theorem OAI.InitialMeanSquare.element_fiber_card_le line 459
  15. theorem OAI.InitialMeanSquare.element_weighted_energy_pushforward line 473
  16. def OAI.SecondPassArithmetic.globalFirstDiagonalCost line 513
  17. theorem OAI.SecondPassArithmetic.globalFirstDiagonalCost_nonneg line 524
  18. theorem OAI.SecondPassArithmetic.globalFirstBlockTest_mode_norm line 535
  19. theorem OAI.SecondPassArithmetic.globalFirstSourceZero_bound line 544
  20. def OAI.SecondPassArithmetic.globalFirstTailCost line 581
  21. theorem OAI.SecondPassArithmetic.globalFirstTailCost_nonneg line 590
  22. theorem OAI.SecondPassArithmetic.globalFirstSourceTail_bound line 603