OAI/NumberTheory/DirichletL/GaussSum/ThetaLocalRows.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ActualEisensteinCubic.actual_fixed_kernel_eq_dualFixedTerm line 31
2. def OAI.ActualEisensteinCubic.actualVariableDualKernel line 80
3. def OAI.ActualEisensteinCubic.actualFixedDualKernel line 89
4. theorem OAI.ActualEisensteinCubic.dualScale_cast line 95
5. theorem OAI.ActualEisensteinCubic.actual_variable_kernel_eq_dualVarTerm line 103
6. theorem OAI.ActualEisensteinCubic.actual_fixed_kernel_eq_dualFixedTerm_point line 120
7. theorem OAI.ActualEisensteinCubic.actual_dual_phase_error_tendsto_zero line 127
8. theorem OAI.ActualEisensteinCubic.actualFixedAbelLimit line 175
9. theorem OAI.ActualEisensteinCubic.actual_oscillatory_poisson_kernel line 200
10. theorem OAI.ActualEisensteinCubic.actualVariableAbelLimit line 226
11. theorem OAI.ActualEisensteinCubic.actualOriginalAbelDualLimit line 257
12. theorem OAI.ActualEisensteinCubic.dual_abel_coefficient line 288
13. theorem OAI.ActualEisensteinCubic.full_dual_abel_coefficient line 305
14. theorem OAI.ActualEisensteinCubic.quadraticGammaO_eq_fourTerms line 340
15. theorem OAI.ActualEisensteinCubic.quadraticGammaO_formula line 388
16. theorem OAI.theta_counter_lambda_eq line 396
17. def OAI.pSeven line 405
18. def OAI.PSeven line 406
19. theorem OAI.pSeven_norm line 408
20. theorem OAI.pSeven_ne line 413
21. theorem OAI.PSeven_absNorm line 420
22. theorem OAI.PSeven_maximal line 423
23. theorem OAI.lambda7_norm line 430
24. theorem OAI.nonreal_cube_ne_conj line 436
25. theorem OAI.pSeven_embedding_im_ne_zero line 456
26. def OAI.thetaGammaSeven line 463
27. theorem OAI.thetaGammaSeven_cube line 475
28. theorem OAI.thetaGammaSeven_ne_conj line 494
29. theorem OAI.ShortDraftLocal.direct_theta_jone_inversion line 509
30. theorem OAI.ShortDraftLocal.direct_theta_jone_local_row line 529
31. theorem OAI.ShortDraftLocal.direct_theta_jone_zero line 565
32. theorem OAI.ShortDraftLocal.direct_theta_jone_not_quadratic line 576