OAI/NumberTheory/DirichletL/Detector/PrincipalRemainderBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.active_prime_sum_bound line 16
  2. def OAI.SevenEighths.ProbePrincipalRemainderBounds.slotConstant line 61
  3. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.slotConstant_nonneg line 64
  4. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.window_sharp_bound line 71
  5. def OAI.SevenEighths.ProbePrincipalRemainderBounds.scalePower line 119
  6. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.scalePower_nonneg line 122
  7. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.continued_source_sharp_pointwise line 138
  8. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.full_sharp_pointwise line 177
  9. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.residue_sharp_pointwise line 217
  10. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.vertical_triple_eq_joint line 248
  11. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.vertical_pair_eq_joint line 258
  12. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.normalizer_norm_pos line 267
  13. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.full_scale_bound line 280
  14. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.residue_scale_bound line 335
  15. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.full_vertical_scale_bound line 397
  16. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.residue_vertical_scale_bound line 432
  17. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.ordered_remainders_scale_bound line 468
  18. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.source_scale_identity line 518
  19. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.source_w_scale_identity line 531
  20. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.source_z_scale_identity line 538
  21. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.eventual_annulus_threshold line 545
  22. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.source_remainders_power_bound line 561
  23. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.source_w_strict_exponent line 594
  24. lemma OAI.SevenEighths.ProbePrincipalRemainderBounds.source_z_strict_exponent line 597
  25. theorem OAI.SevenEighths.ProbePrincipalRemainderBounds.source_remainders_strict_saving line 600