OAI/NumberTheory/DirichletL/Mellin/ExponentialSmoothing.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AnalyticBridge.weighted_cauchy_sq line 14
2. theorem OAI.AnalyticBridge.fiber_mass_bound line 40
3. theorem OAI.AnalyticBridge.reassembled_bilinear_bound line 66
4. theorem OAI.AnalyticBridge.square_label_count line 100
5. theorem OAI.AnalyticBridge.four_factor_label_count line 111
6. structure OAI.AnalyticBridge.CRTChoice line 148
7. def OAI.AnalyticBridge.CRTChoice.coordinates line 163
8. theorem OAI.AnalyticBridge.CRTChoice.coordinates_injective line 168
9. theorem OAI.AnalyticBridge.fixed_crt_choice_count line 176
10. theorem OAI.AnalyticBridge.b0_count_scale line 255
11. def OAI.AnalyticBridge.bit6 line 271
12. def OAI.AnalyticBridge.localExponent line 272
13. def OAI.AnalyticBridge.finalExponent1 line 274
14. def OAI.AnalyticBridge.finalExponent2 line 277
15. theorem OAI.AnalyticBridge.local_parity_table line 281
16. theorem OAI.AnalyticBridge.inactive_conductor_case line 288
17. theorem OAI.AnalyticBridge.new_label_squarefree line 294
18. theorem OAI.ExpBound.exp_neg_le_half line 324
19. theorem OAI.ExpBound.norm_tsum_exp_le_two line 334
20. theorem OAI.ShortDraftMellin.inverse_mellin_analytic line 388
21. theorem OAI.ShortDraftMellin.dirichlet_zero_free_of_mellin_bound line 407
22. theorem OAI.ShortDraftMellin.mellin_of_exponential_smoothing line 445
23. theorem OAI.ShortDraftMellin.dirichlet_exponential_mellin_identity line 484
24. theorem OAI.ShortDraftMellin.mobius_char_exp_summable line 511
25. def OAI.ShortDraftMellin.mobiusExpSum line 538
26. theorem OAI.ShortDraftMellin.mobiusExpSum_norm_le_two line 543
27. theorem OAI.ShortDraftMellin.mobiusExpSum_flat_at_zero line 562
28. theorem OAI.ShortDraftMellin.dirichlet_exp_mellin_identity line 585
29. theorem OAI.ShortDraftMellin.inverse_mellin_analytic_of_flat line 596
30. theorem OAI.ShortDraftMellin.dirichlet_exp_zero_free_of_power_bound line 614