OAI/NumberTheory/DirichletL/Eisenstein/PrimeRecurrence.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.integralCoverTraceFunction_integral_cusp_decay line 86
  2. def OAI.CubicEisenstein.kernelCoverLegAdjointFunction line 123
  3. lemma OAI.CubicEisenstein.kernelCoverLegAdjointFunction_measurable line 127
  4. theorem OAI.CubicEisenstein.kernelCoverLegAdjointFunction_represents line 132
  5. theorem OAI.CubicEisenstein.kernelCoverLegAdjointFunction_cusp_decay line 147
  6. theorem OAI.CubicEisenstein.commonCover_source_sum_eq_zero_of_inverse_cusp_decay line 162
  7. lemma OAI.CubicEisenstein.integralProjection_quasiMeasurePreserving line 201
  8. theorem OAI.CubicEisenstein.integralQuotient_continuous_lifts_eq line 228
  9. theorem OAI.CubicEisenstein.integralQuotient_zero_continuous_lift line 239
  10. theorem OAI.CubicEisenstein.cubeDifferenceL2_eq_zero line 258
  11. theorem OAI.CubicEisenstein.cubeSourceDifference_eq_zero line 291
  12. theorem OAI.CubicEisenstein.cubicSource_cubeAverage line 305
  13. theorem OAI.CubicEisenstein.sourceArithmeticResidue_prime_cube line 311
  14. lemma OAI.CubicEisenstein.rational_inversion_complex line 327
  15. theorem OAI.CubicEisenstein.exists_nonzero_sourceResidualFourierCoefficient line 335
  16. theorem OAI.CubicEisenstein.exists_nonzero_sourceArithmeticResidue line 381
  17. abbrev OAI.CubicEisenstein.PrincipalRamifiedIndex line 396
  18. def OAI.CubicEisenstein.principalRamifiedIndex line 398
  19. def OAI.CubicEisenstein.principalRamifiedWeight line 401
  20. lemma OAI.CubicEisenstein.principalRamifiedWeight_analytic line 404
  21. lemma OAI.CubicEisenstein.scatteringCoefficient_eq_principalRamified line 411
  22. theorem OAI.CubicEisenstein.principalArithmeticResidue_eq_ramified_table line 425
  23. theorem OAI.CubicEisenstein.sourceArithmeticResidue_eq_ramified_table line 466
  24. lemma OAI.CubicEisenstein.arithmeticResidueSum_frequency_cube line 484
  25. lemma OAI.CubicEisenstein.ramified_prime_Gauss_cancel line 500
  26. lemma OAI.CubicEisenstein.ramified_prime_frequency_not_dvd line 524
  27. lemma OAI.CubicEisenstein.sourceRayPhase_mul_primary line 537
  28. def OAI.CubicEisenstein.principalResidueTerm line 556
  29. lemma OAI.CubicEisenstein.principalResidueTerm_vanish line 560
  30. lemma OAI.CubicEisenstein.principalArithmeticResidue_eq_sum line 569
  31. lemma OAI.CubicEisenstein.principalResidueTerm_prime_recurrence line 590
  32. theorem OAI.CubicEisenstein.principalArithmeticResidue_prime_recurrence line 614
  33. theorem OAI.CubicEisenstein.sourceArithmeticResidue_prime_recurrence line 631