OAI/NumberTheory/Jacobsthal/Estimates/RecoveryScale.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_uniform_riesz_right_tails line 12
2. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_left_edge_bound line 61
3. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_horizontal_edge_bound line 103
4. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_mellinFactor line 157
5. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.exists_uniform_riesz_contour_bound line 161
6. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_log_cube_le line 211
7. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.polylog_height_bound line 220
8. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.div_rpow_add_one line 241
9. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_polylog_contour_savings line 246
10. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rpow_perron_sigma line 319
11. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rpow_rieszContourLeft line 324
12. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_character_log_power line 331
13. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight line 398
14. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszWeight_scaled line 401
15. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight_eq line 412
16. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight_nonneg line 418
17. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight_le_one line 424
18. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight_eq_one line 435
19. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszDifferenceWeight_eq_zero line 442
20. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.riesz_rescaled_difference line 447
21. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.sharpSum line 461
22. def OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszRecovery line 463
23. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszSum_extend line 466
24. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszRecovery_eq_sum line 476
25. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.rieszRecovery_sub_sharp line 493
26. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_rieszRecovery_sub_sharp line 517
27. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.norm_rieszRecovery_le line 558
28. theorem OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.sharpSum_norm_le_riesz line 568
29. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.eventually_log_rpow_le_self line 588
30. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.character_vonMangoldt_norm_le line 607
31. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.recovery_scale_bounds line 618
32. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.recovery_power_product line 658
33. lemma OAI.Erdos970.Erdos970Dependency.SiegelWalfisz.recovery_power_times_log line 664