OAI/NumberTheory/DirichletL/Eisenstein/FixedFrequencyExpansion.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.ControlledStratumArithmetic.fixedCusp line 87
  2. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.relative line 90
  3. def OAI.CubicEisenstein.ControlledStratumArithmetic.relativeGamma line 101
  4. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.relativeGamma_mul line 107
  5. def OAI.CubicEisenstein.ControlledStratumArithmetic.fixedFactor line 114
  6. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.relative_character line 120
  7. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.fixedFactor_norm line 132
  8. def OAI.CubicEisenstein.ControlledStratumArithmetic.fourierWeight line 145
  9. def OAI.CubicEisenstein.ControlledStratumArithmetic.multiplierSum line 152
  10. def OAI.CubicEisenstein.ControlledStratumArithmetic.bracketProduct line 163
  11. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.multiplierSum_eq line 172
  12. def OAI.CubicEisenstein.ControlledStratumArithmetic.sourceGamma line 202
  13. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.sourceGamma_mul line 208
  14. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.sourceGamma_character line 215
  15. def OAI.CubicEisenstein.ControlledStratumArithmetic.datum line 223
  16. lemma OAI.CubicEisenstein.ControlledStratumArithmetic.datum_point line 232
  17. def OAI.CubicEisenstein.ControlledStratumArithmetic.smoothedValue line 243
  18. def OAI.CubicEisenstein.ControlledStratumArithmetic.reflectedValue line 254
  19. theorem OAI.CubicEisenstein.ControlledStratumArithmetic.smoothed_eq_reflected line 273
  20. theorem OAI.CubicEisenstein.exists_constructed_stratum_reflection line 312
  21. structure OAI.CubicEisenstein.FixedFourierGeometry line 340
  22. lemma OAI.CubicEisenstein.exists_fixedFourierGeometry line 351
  23. def OAI.CubicEisenstein.fixedFourierGeometry line 364
  24. abbrev OAI.CubicEisenstein.FixedFourierGeometry.PhaseResidue line 370
  25. instance OAI.CubicEisenstein.FixedFourierGeometry.phaseResidue_finite line 372
  26. def OAI.CubicEisenstein.FixedFourierGeometry.levelScale line 375
  27. lemma OAI.CubicEisenstein.FixedFourierGeometry.levelScale_pos line 377
  28. lemma OAI.CubicEisenstein.FixedFourierGeometry.levelScale_le line 380
  29. def OAI.CubicEisenstein.FixedFourierGeometry.dualNumerator line 383
  30. def OAI.CubicEisenstein.FixedFourierGeometry.staticPhase line 387
  31. lemma OAI.CubicEisenstein.FixedFourierGeometry.staticPhase_norm_le_one line 390
  32. def OAI.CubicEisenstein.FixedFourierGeometry.array line 394
  33. lemma OAI.CubicEisenstein.FixedFourierGeometry.array_norm_le_one line 397
  34. lemma OAI.CubicEisenstein.FixedFourierGeometry.array_eq line 401
  35. def OAI.CubicEisenstein.FixedReflectionRay line 408
  36. instance OAI.CubicEisenstein.fixedReflectionRay_finite line 411
  37. instance OAI.CubicEisenstein.fixedReflectionRay_fintype line 417
  38. def OAI.CubicEisenstein.fixedReflectionRayCount line 420
  39. def OAI.CubicEisenstein.fixedReflectionRayEquiv line 422
  40. lemma OAI.CubicEisenstein.fixedReflectionRayCount_subpower line 425
  41. theorem OAI.CubicEisenstein.completedT_of_finite_cusp_profiles line 441
  42. def OAI.CanonicalRowCompletion.fixedRowFourierPhase line 516
  43. def OAI.CanonicalRowCompletion.fixedRowFourierCoeff line 519
  44. lemma OAI.CanonicalRowCompletion.fixedRowFourierCoeff_norm line 523
  45. lemma OAI.CanonicalRowCompletion.fixedRowFourierCoeff_mass line 528
  46. lemma OAI.CanonicalRowCompletion.fixedRowFourierPhase_norm line 537
  47. lemma OAI.CanonicalRowCompletion.fixedRowFourierPhase_translation line 540
  48. lemma OAI.CanonicalRowCompletion.fixedRowFourier_inversion line 545
  49. lemma OAI.CanonicalRowCompletion.summand_mul_fixed_twist line 555
  50. def OAI.CanonicalRowCompletion.completedFixedFrequency line 565
  51. lemma OAI.CanonicalRowCompletion.completedFixedFrequency_summable line 570
  52. theorem OAI.CanonicalRowCompletion.completedT_fixed_fourier line 579
  53. theorem OAI.CanonicalRowCompletion.actual_completedT_fixed_fourier line 611