OAI/NumberTheory/DirichletL/GaussSum/AbelPhaseLimit.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.sum_zmod_two_square line 27
  2. theorem OAI.ActualEisensteinCubic.fixedDualPhase_quotient_two_four_residues line 35
  3. theorem OAI.ActualEisensteinCubic.fixedDualPhase_coordinates line 76
  4. theorem OAI.ActualEisensteinCubic.fixedDualPhase_four_terms line 85
  5. def OAI.OscSpecial.dualQ line 109
  6. def OAI.OscSpecial.dualTrace line 112
  7. def OAI.OscSpecial.phaseA line 116
  8. def OAI.OscSpecial.phaseAngle line 117
  9. def OAI.OscSpecial.dualAmp line 119
  10. def OAI.OscSpecial.dualVarTerm line 121
  11. def OAI.OscSpecial.dualFixedTerm line 124
  12. theorem OAI.OscSpecial.dualQ_nonneg line 128
  13. theorem OAI.OscSpecial.phaseAngle_bound line 133
  14. theorem OAI.OscSpecial.r_eq_one_add_phaseA line 142
  15. theorem OAI.OscSpecial.phaseA_nonneg line 147
  16. theorem OAI.OscSpecial.dual_phase_term_error line 152
  17. def OAI.OscSpecial.dualRealGauss line 171
  18. theorem OAI.OscSpecial.dualRealGauss_summable line 174
  19. theorem OAI.OscSpecial.dualMoment_summable line 191
  20. theorem OAI.OscSpecial.dualAmp_eq_realGauss line 204
  21. theorem OAI.OscSpecial.dualAmp_norm_var line 207
  22. theorem OAI.OscSpecial.dualAmp_norm_fixed line 213
  23. theorem OAI.OscSpecial.dualAmp_summable line 219
  24. theorem OAI.OscSpecial.dualVar_summable line 227
  25. theorem OAI.OscSpecial.dualFixed_summable line 232
  26. theorem OAI.OscSpecial.dualAmp_le_small line 237
  27. def OAI.OscSpecial.phaseErrorConstant line 253
  28. theorem OAI.OscSpecial.phaseErrorConstant_nonneg line 256
  29. theorem OAI.OscSpecial.normalized_dual_phase_sum_error line 262
  30. theorem OAI.OscSpecial.dual_moment_reindex line 329
  31. theorem OAI.OscSpecial.normalized_dual_phase_sum_error_tendsto_zero line 354
  32. theorem OAI.OscSpecial.dualGaussian_eq_dualVarTerm line 401
  33. theorem OAI.ActualEisensteinCubic.osc_q_eq_eis_norm_sq line 443
  34. theorem OAI.ActualEisensteinCubic.two_coordinate_norm_four line 451
  35. theorem OAI.abel_transfer line 465
  36. theorem OAI.ActualEisensteinCubic.gamma_scalar line 492
  37. theorem OAI.ActualEisensteinCubic.breveE_norm_one_all line 509
  38. theorem OAI.ActualEisensteinCubic.fixedDualPhase_norm_one line 517
  39. theorem OAI.ActualEisensteinCubic.variableDualPhase_abel_limit line 527