OAI/NumberTheory/DirichletL/Mellin/FiniteEulerRestoration.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEulerRestoration.isBigO_power_atTop_div_const line 45
  2. theorem OAI.FiniteEulerRestoration.isBigO_finite_Euler_shifts line 62
  3. theorem OAI.FiniteEulerRestoration.tsum_dvd_shift line 77
  4. theorem OAI.FiniteEulerRestoration.tsum_restore_one_prime line 107
  5. theorem OAI.FiniteEulerRestoration.tsum_restore_one_prime_exp line 150
  6. def OAI.FiniteSFactor.outsideExpSum line 177
  7. theorem OAI.FiniteSFactor.outsideExpSum_restore_insert_prime line 181
  8. theorem OAI.CompactMellinBridge.mellin_weighted_sum line 213
  9. theorem OAI.CompactMellinBridge.normFiber_compact_euler_identity line 272
  10. theorem OAI.CompactMellinBridge.weighted_sum_zero_of_large_t line 311
  11. theorem OAI.CompactMellinBridge.weighted_sum_zero_near_small_D line 333
  12. theorem OAI.CompactMellinBridge.compact_weight_mellin_analytic line 349
  13. theorem OAI.CompactMellinBridge.pair_zero_free_of_compact_weight_bound line 389
  14. theorem OAI.CompactMellinBridge.pair_zero_free_of_weighted_identity_principal_left line 459
  15. theorem OAI.CompactMellinBridge.pair_zero_free_of_compact_weight_bound_principal_left line 507
  16. theorem OAI.CompactMellinBridge.pair_zero_free_of_compact_weight_bound_principal_right line 551
  17. structure OAI.CompactMellinBridge.BaseChangeCompactTest line 593
  18. theorem OAI.CompactMellinBridge.dirichletTarget_of_compact_normFiber_tests line 623