OAI/NumberTheory/DirichletL/Eisenstein/ScatteringResidues.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.scalar_residue_sub_continuous line 85
  2. lemma OAI.CubicEisenstein.weightedOutgoingConstant_residue_limit line 95
  3. lemma OAI.CubicEisenstein.baseOutgoingConstant_residue_limit line 104
  4. theorem OAI.CubicEisenstein.kernelCuspHeightFourier_zero_residue line 114
  5. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_zero_residue_seven_thirds line 159
  6. def OAI.CubicEisenstein.cubicResidualFullModeAmplitude line 170
  7. lemma OAI.CubicEisenstein.cubicResidualFullModeAmplitude_zero line 175
  8. lemma OAI.CubicEisenstein.cubicResidualFullModeAmplitude_nonzero line 180
  9. lemma OAI.CubicEisenstein.cubicResidualFullModeAmplitude_zero_density line 185
  10. lemma OAI.CubicEisenstein.cubicResidualFullModeAmplitude_nonzero_density line 196
  11. theorem OAI.CubicEisenstein.kernelCuspHeightFourier_residue_full line 204
  12. def OAI.CubicEisenstein.cubicResidualFunction line 244
  13. lemma OAI.CubicEisenstein.cubicResidualFunction_continuous line 248
  14. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_height_continuous line 256
  15. lemma OAI.CubicEisenstein.periodDomain_integrable_of_continuous line 264
  16. lemma OAI.CubicEisenstein.cubicResidualFunction_fourier line 271
  17. lemma OAI.CubicEisenstein.cubicResidualFunction_heightFourier line 293
  18. lemma OAI.CubicEisenstein.cubicResidualFunction_period line 322
  19. lemma OAI.CubicEisenstein.kernelCuspHeightPullback_memLp line 335
  20. lemma OAI.CubicEisenstein.kernelCuspCoordinates_memLp line 341
  21. lemma OAI.CubicEisenstein.complex_memLp_two_sections line 363
  22. lemma OAI.CubicEisenstein.kernelCuspSections_memLp line 371
  23. lemma OAI.CubicEisenstein.cuspCoordinateLift_measurable line 377
  24. lemma OAI.CubicEisenstein.kernelCuspFourierCoordinate_integrable line 380
  25. def OAI.CubicEisenstein.kernelCuspSliceCoefficient line 406
  26. lemma OAI.CubicEisenstein.kernelCuspHeightFourier_eq_slice_integral line 410
  27. lemma OAI.CubicEisenstein.kernelCuspSliceCoefficient_integrable line 435
  28. lemma OAI.CubicEisenstein.third_character_eq_one_iff_basis line 461
  29. lemma OAI.CubicEisenstein.omega3_pow_exp_eq_one_iff line 488
  30. lemma OAI.CubicEisenstein.eisEmbedding_omega_actual line 516
  31. lemma OAI.CubicEisenstein.trace_third_coordinate line 523
  32. lemma OAI.CubicEisenstein.ramified_symbol_primaryCoord line 539
  33. lemma OAI.CubicEisenstein.ramified_symbol_at_one line 556
  34. lemma OAI.CubicEisenstein.ramified_symbol_at_omega line 564
  35. lemma OAI.CubicEisenstein.ramifiedFrequencyChar_mk line 572
  36. lemma OAI.CubicEisenstein.coords_mul_omega_second line 581
  37. def OAI.CubicEisenstein.ramifiedCongruence line 591
  38. lemma OAI.CubicEisenstein.ramifiedFrequencyChar_eq_one_iff line 596
  39. theorem OAI.CubicEisenstein.ramified_arithmetic_explicit_table line 608
  40. def OAI.CubicEisenstein.ramifiedUnitIndex line 616
  41. lemma OAI.CubicEisenstein.ramifiedUnitIndex_spec line 618
  42. def OAI.CubicEisenstein.explicitRamifiedCoefficient line 623
  43. theorem OAI.CubicEisenstein.arithmeticResidueSum_eq_explicitRamifiedCoefficient line 630
  44. theorem OAI.CubicEisenstein.scatteringCoefficient_explicit_ramified line 640