OAI/NumberTheory/DirichletL/Eisenstein/RamifiedSixBranches.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.arbitraryIntervalWhittaker line 86
  2. lemma OAI.CubicEisenstein.arbitraryIntervalWhittaker_analyticAt line 89
  3. lemma OAI.CubicEisenstein.ramifiedSource_height_fourier_average line 96
  4. abbrev OAI.CubicEisenstein.RamifiedSixBranch line 141
  5. def OAI.CubicEisenstein.unitCuspUnramifiedIndex line 143
  6. def OAI.CubicEisenstein.ramifiedSixIndex line 146
  7. def OAI.CubicEisenstein.ramifiedSixWeight line 155
  8. lemma OAI.CubicEisenstein.ramifiedSixWeight_analytic line 169
  9. lemma OAI.CubicEisenstein.ramifiedCuspGaussSeries_eq_six line 188
  10. def OAI.CubicEisenstein.ramifiedArithmeticResidue line 198
  11. theorem OAI.CubicEisenstein.ramifiedSource_height_residue line 208
  12. theorem OAI.CubicEisenstein.ramifiedSource_height_residue_integral line 242
  13. def OAI.CubicEisenstein.kernelCorrespondenceMatrix line 270
  14. lemma OAI.CubicEisenstein.kernelCorrespondenceTest_field line 273
  15. lemma OAI.CubicEisenstein.kernelCorrespondenceTest_energyDensity_le line 290
  16. lemma OAI.CubicEisenstein.kernelCorrespondenceTest_energy_le line 336
  17. def OAI.CubicEisenstein.kernelCorrespondenceTestLinear line 378
  18. lemma OAI.CubicEisenstein.kernelCorrespondenceL2_norm_le line 402
  19. lemma OAI.CubicEisenstein.kernelCorrespondenceTest_graph_norm line 423
  20. def OAI.CubicEisenstein.kernelCorrespondenceEnergy line 437
  21. lemma OAI.CubicEisenstein.kernelCorrespondenceEnergy_core line 441
  22. lemma OAI.CubicEisenstein.kernelCorrespondenceEnergy_mass line 447
  23. def OAI.CubicEisenstein.ramifiedCuspShiftNumerator line 468
  24. lemma OAI.CubicEisenstein.ramifiedCuspShift_congr line 471
  25. lemma OAI.CubicEisenstein.ramifiedCuspShift_support line 482
  26. lemma OAI.CubicEisenstein.ramifiedSource_affine_shift line 491
  27. lemma OAI.CubicEisenstein.ramifiedSource_weighted_shift line 512
  28. theorem OAI.CubicEisenstein.ramifiedSource_active_weighted_periodic line 537
  29. def OAI.CubicEisenstein.ramifiedScaledMode line 559
  30. lemma OAI.CubicEisenstein.ramifiedScaledMode_shift line 563
  31. lemma OAI.CubicEisenstein.ramifiedScaledMode_periodic line 575
  32. theorem OAI.CubicEisenstein.ramifiedSource_scaled_fourier_off_support line 584
  33. lemma OAI.CubicEisenstein.ramifiedSource_height_continuous line 607
  34. theorem OAI.CubicEisenstein.ramifiedSource_scaled_fourier_active line 618