OAI/NumberTheory/DirichletL/Eisenstein/RamifiedValuation.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.ramifiedFunction_valuation_ne_two line 86
  2. theorem OAI.CubicEisenstein.ramifiedBesselValue_squarefree_cube_support line 129
  3. lemma OAI.CubicEisenstein.onceCuspScale_not_three_dvd line 168
  4. lemma OAI.CubicEisenstein.onceCuspScale_lambda_dvd line 176
  5. theorem OAI.CubicEisenstein.ramifiedBesselValue_exact_lambda_valuation line 181
  6. theorem OAI.CubicEisenstein.ramifiedBesselValue_once_squarefree_cube_support line 198
  7. theorem OAI.CubicEisenstein.ramifiedBesselValue_once_squarefree_cube_bound line 226
  8. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_norm line 242
  9. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_product_norm line 253
  10. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_ramified_bound line 279
  11. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_squarefree_cube_norm line 290
  12. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_squarefree_cube_bound line 312
  13. theorem OAI.CubicEisenstein.three_cusp_coefficients_squarefree_cube_bound line 329
  14. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_prime_power_vanish line 351
  15. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_full_squarefree_cube_support line 357
  16. abbrev OAI.CubicEisenstein.ThetaPrimaryCubePair line 399
  17. def OAI.CubicEisenstein.thetaPrimaryProduct line 403
  18. lemma OAI.CubicEisenstein.thetaPrimaryProduct_injective line 408
  19. abbrev OAI.CubicEisenstein.ThetaFullIndex line 416
  20. def OAI.CubicEisenstein.thetaFullFrequency line 418
  21. lemma OAI.CubicEisenstein.thetaFullFrequency_product line 422
  22. lemma OAI.CubicEisenstein.thetaFullFrequency_ne_zero line 427
  23. lemma OAI.CubicEisenstein.thetaFullFrequency_span line 433
  24. theorem OAI.CubicEisenstein.thetaFullFrequency_injective line 438
  25. structure OAI.CubicEisenstein.SourceCuspDatum line 469
  26. def OAI.CubicEisenstein.SourceCuspDatum.matrix line 477
  27. def OAI.CubicEisenstein.SourceCuspDatum.point line 479
  28. def OAI.CubicEisenstein.SourceCuspDatum.dualPoint line 480
  29. def OAI.CubicEisenstein.SourceCuspDatum.heightScale line 481
  30. def OAI.CubicEisenstein.SourceCuspDatum.multiplier line 482
  31. lemma OAI.CubicEisenstein.SourceCuspDatum.heightScale_pos line 484
  32. lemma OAI.CubicEisenstein.SourceCuspDatum.multiplier_norm line 487
  33. lemma OAI.CubicEisenstein.SourceCuspDatum.multiplier_ne_zero line 491
  34. lemma OAI.CubicEisenstein.exists_sourceCuspDatum line 499
  35. def OAI.CubicEisenstein.rationalSourceCusp line 516
  36. lemma OAI.CubicEisenstein.rationalSourceCusp_point line 519
  37. def OAI.CubicEisenstein.sourceCuspZFamily line 523
  38. theorem OAI.CubicEisenstein.SourceCuspDatum.reflection line 526
  39. def OAI.CubicEisenstein.finiteTwistCusp line 534
  40. lemma OAI.CubicEisenstein.finiteTwistCusp_point line 537
  41. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_reflection_of_data line 542
  42. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_reflection line 555
  43. theorem OAI.CubicEisenstein.completedBesselProfile_finite_cusp_reflection line 566
  44. lemma OAI.CubicEisenstein.horizontalPhaseMultiplier_scaled_bar line 587
  45. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaled_fullFunction_horizontal_hasDerivAt line 599
  46. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaled_fullFunction_wirtingerBar line 612
  47. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaledConjugateZTerm line 629
  48. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaledConjugate_wirtingerZ line 633
  49. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaledConjugateZTerm_summable line 646
  50. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaledConjugateZTerm_zero line 666
  51. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.scaledConjugateZTerm_bessel line 670