OAI/NumberTheory/DirichletL/Eisenstein/CoverTrace.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.integralCoverSheet_measure line 85
  2. theorem OAI.CubicEisenstein.integralCoverMap_measure line 101
  3. lemma OAI.CubicEisenstein.integralCoverMap_measurePreserving line 127
  4. abbrev OAI.CubicEisenstein.IntegralQuotientL2 line 143
  5. def OAI.CubicEisenstein.integralCoverPullback line 146
  6. theorem OAI.CubicEisenstein.integralCoverPullback_ae line 153
  7. theorem OAI.CubicEisenstein.integralCoverPullback_norm_le line 166
  8. theorem OAI.CubicEisenstein.integralCoverPullback_inner line 179
  9. def OAI.CubicEisenstein.integralCoverTrace line 210
  10. theorem OAI.CubicEisenstein.integralCoverTrace_pairing line 215
  11. theorem OAI.CubicEisenstein.integralCoverTrace_pullback line 221
  12. theorem OAI.CubicEisenstein.integralCoverPullback_opNorm_le line 229
  13. theorem OAI.CubicEisenstein.integralCoverTrace_opNorm_le line 235
  14. def OAI.CubicEisenstein.integralCoverAverage line 241
  15. theorem OAI.CubicEisenstein.integralCoverAverage_pullback line 246
  16. theorem OAI.CubicEisenstein.integralCoverPullback_injective line 254
  17. def OAI.CubicEisenstein.integralCoverFiberPoint line 263
  18. lemma OAI.CubicEisenstein.integralCoverFiberPoint_mk line 275
  19. lemma OAI.CubicEisenstein.integralCoverFiberPoint_rep line 279
  20. lemma OAI.CubicEisenstein.integralCoverFiberPoint_smul line 286
  21. lemma OAI.CubicEisenstein.integralCoverFiberPoint_measurable line 294
  22. def OAI.CubicEisenstein.integralCoverTraceLift line 302
  23. lemma OAI.CubicEisenstein.integralCoverTraceLift_smul line 307
  24. def OAI.CubicEisenstein.integralCoverTraceFunction line 315
  25. lemma OAI.CubicEisenstein.integralCoverTraceFunction_projection line 321
  26. lemma OAI.CubicEisenstein.integralCoverTraceFunction_measurable line 325
  27. theorem OAI.CubicEisenstein.integralCoverTraceFunction_cusp_decay line 334
  28. def OAI.CubicEisenstein.IntegralCoverIntertwines line 384
  29. lemma OAI.CubicEisenstein.integralCoverIntertwines_action line 389
  30. lemma OAI.CubicEisenstein.integralCoverIntertwines_inverse line 394
  31. def OAI.CubicEisenstein.integralConjugateMap line 403
  32. lemma OAI.CubicEisenstein.integralConjugateMap_projection line 410
  33. lemma OAI.CubicEisenstein.integralConjugateMap_measurable line 415
  34. lemma OAI.CubicEisenstein.integralConjugateMap_continuous line 421
  35. lemma OAI.CubicEisenstein.integralConjugateMap_inverse line 426
  36. def OAI.CubicEisenstein.integralConjugateHomeomorph line 436
  37. lemma OAI.CubicEisenstein.integralConjugate_fundamentalDomain line 450
  38. theorem OAI.CubicEisenstein.integralConjugateMap_measurePreserving line 465
  39. def OAI.CubicEisenstein.integralConjugatePullback line 481
  40. theorem OAI.CubicEisenstein.integralConjugatePullback_ae line 488
  41. lemma OAI.CubicEisenstein.scaled_cusp_periodic_upper line 505
  42. theorem OAI.CubicEisenstein.sourceCusp_scaled_periodic line 524
  43. lemma OAI.CubicEisenstein.sourceCusp_scaled_continuous line 547
  44. theorem OAI.CubicEisenstein.sourceCusp_average_enlarged line 559
  45. theorem OAI.CubicEisenstein.period_integral_eisenstein_affine line 577
  46. lemma OAI.CubicEisenstein.complex_upper_triangular_bottom_ne_zero line 588
  47. lemma OAI.CubicEisenstein.complex_upper_triangular_action line 595