OAI/NumberTheory/DirichletL/Reciprocity/RamifiedCuspPhases.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicKubota.actualCubeCuspPhaseSum line 82
  2. theorem OAI.CubicKubota.actualCubeCuspPhaseSum_coprime line 88
  3. theorem OAI.CubicKubota.actualCubeCuspPhaseSum_dvd line 129
  4. lemma OAI.CubicEisenstein.onceCusp_trace_lambda line 173
  5. lemma OAI.CubicEisenstein.onceCusp_lambda_dvd_trace line 177
  6. def OAI.CubicEisenstein.onceCuspScale line 182
  7. def OAI.CubicEisenstein.onceCuspComplement line 184
  8. lemma OAI.CubicEisenstein.onceCusp_scale_complement line 186
  9. lemma OAI.CubicEisenstein.onceCusp_scale_ne_zero line 192
  10. lemma OAI.CubicEisenstein.onceCusp_scale_lambda line 198
  11. lemma OAI.CubicEisenstein.onceCusp_complement_lambda line 203
  12. lemma OAI.CubicEisenstein.onceCusp_scale_coprime line 206
  13. abbrev OAI.CubicEisenstein.OnceRamifiedData line 211
  14. def OAI.CubicEisenstein.onceRamifiedToPrimitive line 213
  15. lemma OAI.CubicEisenstein.onceRamifiedToPrimitive_bijective line 232
  16. def OAI.CubicEisenstein.onceRamifiedEquiv line 281
  17. lemma OAI.CubicEisenstein.onceRamified_row_phase line 284
  18. def OAI.CubicEisenstein.diagonalPrimitiveMap line 304
  19. def OAI.CubicEisenstein.diagonalPrimitiveEquiv line 310
  20. lemma OAI.CubicEisenstein.rowOperator_unitCuspDiagonal line 330
  21. lemma OAI.CubicEisenstein.rowEnergy_unit_smul line 357
  22. lemma OAI.CubicEisenstein.diagonal_ray_summand line 362
  23. def OAI.CubicEisenstein.rayEisenstein line 381
  24. theorem OAI.CubicEisenstein.eisenstein_unit_diagonal line 384
  25. def OAI.CubicEisenstein.affineLowerTerm line 402
  26. lemma OAI.CubicEisenstein.affineLowerTerm_mul_ray line 407
  27. lemma OAI.CubicEisenstein.onceRamified_summand line 414
  28. def OAI.CubicEisenstein.diagonalOnceCuspIndex line 440
  29. def OAI.CubicEisenstein.diagonalUnitCuspIndex line 443
  30. lemma OAI.CubicEisenstein.diagonal_once_summand line 446
  31. lemma OAI.CubicEisenstein.diagonal_unit_summand line 458
  32. theorem OAI.CubicEisenstein.diagonal_once_eisenstein_rows line 470
  33. theorem OAI.CubicEisenstein.diagonal_unit_eisenstein_rows line 478
  34. theorem OAI.CubicEisenstein.hasSum_diagonal_once_integrals line 486
  35. def OAI.CubicEisenstein.eisensteinCoordinateMul line 516
  36. def OAI.CubicEisenstein.eisensteinTorusMul line 521
  37. lemma OAI.CubicEisenstein.eisensteinTorusMul_continuous line 529
  38. lemma OAI.CubicEisenstein.periodVector_coordinateMul line 538
  39. lemma OAI.CubicEisenstein.eisensteinTorusMul_periodTorus line 549
  40. lemma OAI.CubicEisenstein.eisensteinTorusMul_surjective line 556
  41. theorem OAI.CubicEisenstein.eisensteinTorusMul_measurePreserving line 562
  42. lemma OAI.CubicEisenstein.periodTorus_eq_implies_lattice_difference line 566
  43. lemma OAI.CubicEisenstein.periodic_function_periodSection line 583
  44. theorem OAI.CubicEisenstein.period_integral_eisenstein_mul line 590
  45. theorem OAI.CubicEisenstein.finite_index_period_unfold_of_summable line 614
  46. lemma OAI.CubicEisenstein.finite_index_period_lintegral line 647
  47. lemma OAI.CubicEisenstein.finite_index_period_integrals_summable line 677
  48. theorem OAI.CubicEisenstein.finite_index_period_unfold line 685