OAI/NumberTheory/DirichletL/Eisenstein/CorrespondencePullback.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.integralCoverMap_quasiMeasurePreserving line 86
  2. def OAI.CubicEisenstein.kernelCorrespondenceL2 line 99
  3. lemma OAI.CubicEisenstein.kernelCorrespondenceL2_representative line 106
  4. lemma OAI.CubicEisenstein.kernelCorrespondenceTest_mass line 123
  5. lemma OAI.CubicEisenstein.kernelCorrespondenceFunction_integrable line 132
  6. lemma OAI.CubicEisenstein.kernelCorrespondenceFunction_integral line 146
  7. def OAI.CubicEisenstein.coverEnergyDensity line 178
  8. def OAI.CubicEisenstein.coverGradientAt line 182
  9. lemma OAI.CubicEisenstein.coverEnergyDensity_nonneg line 186
  10. lemma OAI.CubicEisenstein.coverGradientAt_norm_sq line 191
  11. lemma OAI.CubicEisenstein.coverEnergyDensity_comp line 213
  12. lemma OAI.CubicEisenstein.coverGradientAt_sum line 223
  13. lemma OAI.CubicEisenstein.norm_sum_sq_le_card line 231
  14. lemma OAI.CubicEisenstein.coverEnergyDensity_sum_le line 241
  15. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_eq_cover line 254
  16. lemma OAI.CubicEisenstein.rational_unipotent_upper line 266
  17. lemma OAI.CubicEisenstein.rational_cusp_lower_section line 276
  18. lemma OAI.CubicEisenstein.hyperbolicEisenstein_fixed_upper line 292
  19. theorem OAI.CubicEisenstein.sourceEisenstein_unit_lower line 295
  20. theorem OAI.CubicEisenstein.sourceEisenstein_primitive_lower_four line 309
  21. lemma OAI.CubicEisenstein.continuous_fixed_left_Eisenstein line 328
  22. lemma OAI.CubicEisenstein.integrable_fixed_left_Eisenstein_fourier line 336
  23. def OAI.CubicEisenstein.ramifiedCuspGaussSeries line 352
  24. theorem OAI.CubicEisenstein.ramifiedSourceEisenstein_fourier line 360
  25. theorem OAI.CubicEisenstein.finite_unramified_residue line 448
  26. lemma OAI.CubicEisenstein.cuspStrip_integrable_continuous line 548
  27. def OAI.CubicEisenstein.sourceArbitraryHeightFamily line 554
  28. def OAI.CubicEisenstein.sourceArbitraryHeightFourier line 559
  29. lemma OAI.CubicEisenstein.sourceArbitraryHeightFamily_analyticAt line 564
  30. lemma OAI.CubicEisenstein.sourceArbitraryHeightFamily_residue_limit line 572
  31. lemma OAI.CubicEisenstein.sourceProjection_integral line 585
  32. lemma OAI.CubicEisenstein.sourceArbitraryHeightFamily_initial line 607
  33. lemma OAI.CubicEisenstein.arbitraryCuspHeightFourier_residue_integral line 618
  34. lemma OAI.CubicEisenstein.sourceArbitraryHeightFourier_residue_integral line 629