OAI/NumberTheory/DirichletL/GaussSum/MellinSupport.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.cubeWeight_zero_of_primaryGenerator_zero line 81
  2. lemma OAI.CompletedGauss.completedMellinCoefficient_support line 85
  3. lemma OAI.CompletedGauss.completedMellinCoefficient_zero_off_support line 98
  4. def OAI.CompletedGauss.primaryCubePairToMellinIndex line 104
  5. lemma OAI.CompletedGauss.primaryCubePairToMellinIndex_injective line 110
  6. theorem OAI.CompletedGauss.completedMellinCoefficient_tsum_primary_pairs line 116
  7. theorem OAI.CompletedGauss.completedBesselProfile_primary_pairs line 143
  8. lemma OAI.CubicEisenstein.cubicSourceConjugateFunction_levelTwo line 166
  9. theorem OAI.CubicEisenstein.cubicSourceConjugateFunction_cuspDerivative_levelTwo line 172
  10. lemma OAI.CubicEisenstein.cuspBarProfile_conjugate_reflection_levelTwo line 186
  11. lemma OAI.CubicEisenstein.conjugateSource_cuspRepresentative_zProfile_decay line 203
  12. theorem OAI.CubicEisenstein.conjugateSource_levelTwo_three_cusp_mellin_entire line 218
  13. lemma OAI.CubicEisenstein.upper_triangular_right_cusp_ratio line 254
  14. theorem OAI.CubicEisenstein.conjugateSource_integral_cusp_mellin_entire line 267
  15. lemma OAI.CubicEisenstein.exists_integral_matrix_cusp_ratio line 287
  16. theorem OAI.CubicEisenstein.conjugateSource_rational_cusp_mellin_entire line 319
  17. theorem OAI.CubicEisenstein.conjugateSource_finite_twist_cusp_mellin_entire line 327
  18. def OAI.CubicEisenstein.signedOmegaUnit line 347
  19. lemma OAI.CubicEisenstein.signedOmegaUnit_val line 350
  20. lemma OAI.CubicEisenstein.signedOmegaUnit_surjective line 354
  21. def OAI.CubicEisenstein.signedOmegaEquiv line 362
  22. lemma OAI.CubicEisenstein.cubicSymbol_norm_one line 369
  23. lemma OAI.CubicEisenstein.arithmeticResidueSum_norm_mul_primary line 376
  24. def OAI.CubicEisenstein.lowRamifiedFrequency line 387
  25. lemma OAI.CubicEisenstein.lowRamifiedFrequency_ne_zero line 389
  26. lemma OAI.CubicEisenstein.lowRamifiedFrequency_absNorm line 393
  27. lemma OAI.CubicEisenstein.lowRamifiedFrequency_arithmetic_vanish line 398
  28. lemma OAI.CubicEisenstein.lowRamifiedFrequency_primary_vanish line 408
  29. def OAI.CubicEisenstein.ramifiedCoordMul line 421
  30. def OAI.CubicEisenstein.ramifiedCoordPow line 422
  31. def OAI.CubicEisenstein.lowRamifiedQuotientCoord line 426
  32. def OAI.CubicEisenstein.lowRamifiedSupport line 431
  33. instance OAI.CubicEisenstein.lowRamifiedSupport_decidable line 437
  34. def OAI.CubicEisenstein.lowRamifiedSupportSet line 444
  35. lemma OAI.CubicEisenstein.lowRamifiedSupport_card line 447
  36. lemma OAI.CubicEisenstein.lowRamifiedSupport_exponent line 450
  37. lemma OAI.CubicEisenstein.ramifiedCoordMul_eval line 454
  38. lemma OAI.CubicEisenstein.ramifiedCoordPow_eval line 459
  39. lemma OAI.CubicEisenstein.lowRamifiedQuotientCoord_eval line 466
  40. lemma OAI.CubicEisenstein.lowRamifiedQuotientCoord_relation line 487
  41. lemma OAI.CubicEisenstein.lowRamifiedSupport_of_ne_zero line 518
  42. def OAI.CubicEisenstein.ramifiedRawWeight line 555
  43. lemma OAI.CubicEisenstein.ramifiedRawWeight_norm_le line 558
  44. lemma OAI.CubicEisenstein.ramifiedRawWeight_norm_mul_primary line 565
  45. lemma OAI.CubicEisenstein.ramifiedDecayRatio_cube line 570
  46. lemma OAI.CubicEisenstein.lowRamifiedRawWeight_bound line 574
  47. theorem OAI.CubicEisenstein.lowRamifiedRawWeight_sum line 589