OAI/NumberTheory/DirichletL/Eisenstein/GaussFactorization.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.cubicBesselNormalizer line 85
  2. def OAI.CubicEisenstein.cubicResidualFourierCoefficient line 88
  3. lemma OAI.CubicEisenstein.sourceFourierKernel_cubic_height line 91
  4. lemma OAI.CubicEisenstein.cuspWhittakerHeightFactor_punctured_ne_zero line 131
  5. lemma OAI.CubicEisenstein.continuedNonzeroScattering_eq_arithmetic_germ line 146
  6. lemma OAI.CubicEisenstein.cuspWeightedWhittakerHeightFactor_differentiableAt line 167
  7. lemma OAI.CubicEisenstein.cuspWeightedWhittakerHeightFactor_analyticAt line 178
  8. lemma OAI.CubicEisenstein.kernelCuspWeightedFourierFamily_cross_identity line 186
  9. lemma OAI.CubicEisenstein.upperVertical_tendsto_cubic_punctured line 220
  10. lemma OAI.CubicEisenstein.kernelCuspWeightedFourier_residue_factor line 236
  11. lemma OAI.CubicEisenstein.cuspWeightedWhittakerHeightFactor_center_bessel line 276
  12. lemma OAI.CubicEisenstein.kernelCuspWeightedFourier_residue_bessel line 289
  13. lemma OAI.CubicEisenstein.denominatorRep_mk_congr line 307
  14. lemma OAI.CubicEisenstein.isCoprime_right_congr_of_dvd line 313
  15. abbrev OAI.CubicEisenstein.CubicUnitResidue line 319
  16. def OAI.CubicEisenstein.denominatorCRTMap line 322
  17. lemma OAI.CubicEisenstein.denominatorCRTMap_injective line 331
  18. lemma OAI.CubicEisenstein.denominatorCRTMap_surjective line 348
  19. def OAI.CubicEisenstein.denominatorCRTEquiv line 387
  20. def OAI.CubicEisenstein.residueAdditive line 392
  21. lemma OAI.CubicEisenstein.residueAdditive_congr line 395
  22. def OAI.CubicEisenstein.cubicUnitGaussSum line 408
  23. lemma OAI.CubicEisenstein.residueAdditive_three_congr line 413
  24. lemma OAI.CubicEisenstein.residueAdditive_crt line 426
  25. lemma OAI.CubicEisenstein.arithmetic_crt_summand line 441
  26. theorem OAI.CubicEisenstein.arithmeticResidueSum_crt line 473
  27. lemma OAI.CubicEisenstein.residueAdditive_mul line 506
  28. lemma OAI.CubicEisenstein.residueAdditive_swap line 513
  29. lemma OAI.CubicEisenstein.arithmeticResidueSum_frequency_congr line 519
  30. theorem OAI.CubicEisenstein.arithmeticResidueSum_frequency_twist line 529
  31. lemma OAI.CubicEisenstein.cubicUnitGaussSum_frequency_congr line 554
  32. def OAI.CubicEisenstein.cubicUnitResidueMul line 569
  33. lemma OAI.CubicEisenstein.cubicUnitResidueMul_injective line 574
  34. def OAI.CubicEisenstein.cubicUnitResidueMulEquiv line 580
  35. lemma OAI.CubicEisenstein.cubicUnitResidueMul_rep_congr line 587
  36. theorem OAI.CubicEisenstein.cubicUnitGaussSum_frequency_twist line 597
  37. theorem OAI.CubicEisenstein.arithmeticResidueSum_coprime_product line 627