OAI/NumberTheory/DirichletL/CubicSieve/ReopeningBounds.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_filter line 85
  2. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_zero line 98
  3. def OAI.CanonicalRowCompletion.progressingCubes line 117
  4. theorem OAI.CanonicalRowCompletion.separatedCubeCoefficient_eq_zero_of_small line 121
  5. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_filter line 133
  6. theorem OAI.CanonicalRowCompletion.progressingCubes_progress line 151
  7. theorem OAI.CanonicalRowCompletion.progressingActiveBin_progress line 168
  8. theorem OAI.CanonicalRowCompletion.outsideCanonicalBin_zero_of_empty_filter line 176
  9. theorem OAI.CanonicalRowCompletion.reopenedCanonicalRow_progressing line 185
  10. def OAI.SecondPassArithmetic.canonicalBudgetCoefficient line 219
  11. theorem OAI.SecondPassArithmetic.canonicalBudgetCoefficient_nonneg line 224
  12. theorem OAI.SecondPassArithmetic.canonicalBudgetScalar_bound line 234
  13. theorem OAI.SecondPassArithmetic.globalFirstQuantitativeBudget_bounded line 289
  14. def OAI.SecondPassArithmetic.reopeningScaleConstant line 345
  15. def OAI.SecondPassArithmetic.reopeningAuxiliaryScale line 347
  16. lemma OAI.SecondPassArithmetic.reopeningScaleConstant_one line 349
  17. lemma OAI.SecondPassArithmetic.reopeningScaleConstant_exp line 353
  18. theorem OAI.SecondPassArithmetic.globalFirstRowCap_reopening line 358
  19. theorem OAI.SecondPassArithmetic.globalFirstRowCap_reopening_bound line 365
  20. theorem OAI.SecondPassArithmetic.globalFirstRowCap_reopening_small_power line 376
  21. theorem OAI.SecondPassArithmetic.reopeningAuxiliaryScale_bounds line 389
  22. theorem OAI.SecondPassArithmetic.globalFirstTailFactor_envelope line 429
  23. theorem OAI.SecondPassArithmetic.globalFirstTailFactor_reopening_power line 452
  24. theorem OAI.SecondPassArithmetic.globalFirstTailFactor_reopening_arbitrary_decay line 478
  25. theorem OAI.SecondPassArithmetic.globalFirstTailFactor_reopening_nat_decay line 497
  26. lemma OAI.SecondPassArithmetic.reopening_cutoff_ratio line 511
  27. lemma OAI.SecondPassArithmetic.globalFirstRowCap_reopening_rpow line 514
  28. lemma OAI.SecondPassArithmetic.reopening_cube_bound line 525
  29. theorem OAI.SecondPassArithmetic.reopening_diagonal_monomial line 539
  30. theorem OAI.SecondPassArithmetic.reopening_recursive_monomial line 563
  31. theorem OAI.SecondPassArithmetic.reopening_diagonal_with_ratio line 588
  32. theorem OAI.SecondPassArithmetic.reopening_recursive_with_ratio line 602