OAI/NumberTheory/DirichletL/PrimeRows/RationalApproximation.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalQuant.cpos line 24
  2. theorem OAI.RationalQuant.eventual_log_absorption line 28
  3. theorem OAI.RationalQuant.scale_large_eventually line 77
  4. theorem OAI.RationalQuant.from_rational_prime_rows_with_constant line 99
  5. theorem OAI.RationalQuant.rational_row_error_power line 155
  6. theorem OAI.RationalPrimeExtraction.eventual_count_power line 203
  7. theorem OAI.RationalPrimeExtraction.selected_rows_in_ball line 221
  8. theorem OAI.RationalPrimeExtraction.selected_row_error_bound line 264
  9. theorem OAI.RationalPrimeExtraction.eventual_finite_extraction line 279
  10. theorem OAI.RationalPrimeExtraction.actual_rational_prime_extraction line 332
  11. def OAI.OscSpecial.phaseBoundConstant line 386
  12. theorem OAI.OscSpecial.phaseBoundConstant_pos line 389
  13. theorem OAI.OscSpecial.quadratic_phase_abs_le line 394
  14. theorem OAI.GaussianMoment.scaled_moment_vanishes_const line 436
  15. theorem OAI.ActualEisensteinCubic.breveE_period_div_lam_O line 464
  16. def OAI.ActualEisensteinCubic.fixedDualPhase line 473
  17. theorem OAI.ActualEisensteinCubic.fixedDualPhase_period_two line 476
  18. theorem OAI.ActualEisensteinCubic.fixedDualPhase_eq_of_mod_two line 493
  19. theorem OAI.ActualEisensteinCubic.fixedDualPhase_weighted_partition line 506
  20. def OAI.OscSpecial.dualScale line 549
  21. theorem OAI.OscSpecial.dualScale_tendsto line 552
  22. theorem OAI.OscSpecial.abel_mass_dual_scale line 576