OAI/NumberTheory/DirichletL/Eisenstein/CubeCuspAverage.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.sourceCusp_average_enlarged_affine line 83
  2. theorem OAI.CubicEisenstein.sourceCusp_average_complex_upper line 93
  3. lemma OAI.CubicEisenstein.sourceCuspConstant_congruent line 109
  4. lemma OAI.CubicEisenstein.sourceCuspConstant_congruent_zero line 127
  5. def OAI.CubicEisenstein.cubeCuspTriangular line 143
  6. lemma OAI.CubicEisenstein.cubeCuspTriangular_factor line 146
  7. lemma OAI.CubicEisenstein.cubeCuspTriangular_entries line 152
  8. lemma OAI.CubicEisenstein.cubeCuspTriangular_integral_scale line 222
  9. lemma OAI.CubicEisenstein.cube_scale_norm_real line 238
  10. lemma OAI.CubicEisenstein.cubeCuspTriangular_norm_sq line 243
  11. lemma OAI.CubicEisenstein.cubeCuspTriangular_height line 254
  12. lemma OAI.CubicKubota.levelTwo_primary_shift_cases line 284
  13. lemma OAI.CubicEisenstein.rationalComplex_S_sq_action line 312
  14. lemma OAI.CubicEisenstein.rationalComplex_T_eq line 327
  15. theorem OAI.CubicEisenstein.exists_primary_cusp_shift line 333
  16. lemma OAI.CubicKubota.matrix_mul_upper_first_column line 387
  17. def OAI.CubicKubota.CubeCuspData.right_upper line 394
  18. lemma OAI.CubicKubota.CubeCuspData.right_upper_exponent line 409
  19. lemma OAI.CubicKubota.CubeCuspData.right_upper_character line 412
  20. lemma OAI.CubicEisenstein.cubeAverage_continuous line 433
  21. lemma OAI.CubicEisenstein.cubeAverage_cusp_integral line 444
  22. theorem OAI.CubicEisenstein.kernelSourceProjection_variationalResolvent line 476
  23. theorem OAI.CubicEisenstein.kernelSourceProjection_operatorGraph line 485
  24. theorem OAI.CubicEisenstein.kernelSourceProjection_eigenvector line 491
  25. theorem OAI.CubicEisenstein.kernelSourceProjection_cubicEisensteinResidue_eigenvector line 496
  26. def OAI.CubicEisenstein.sourceCuspLeadingCoefficient line 510
  27. def OAI.CubicEisenstein.sourceCuspRemainder line 513
  28. lemma OAI.CubicEisenstein.sourceCuspLeadingCoefficient_decomposition line 517
  29. lemma OAI.CubicEisenstein.sourceCuspRemainder_decomposition line 526
  30. theorem OAI.CubicEisenstein.sourceCuspRemainder_bound_all line 543
  31. lemma OAI.CubicEisenstein.sourceCuspConstant_one line 553
  32. lemma OAI.CubicEisenstein.sourceCuspLeadingCoefficient_one line 558
  33. lemma OAI.CubicEisenstein.sourceCuspRemainder_one line 563
  34. theorem OAI.CubicEisenstein.sourceCuspRemainder_principal_cubic_decay line 572
  35. lemma OAI.CubicEisenstein.integralCoverDomain_projection_measurePreserving line 590
  36. lemma OAI.CubicEisenstein.integralCoverSheet_measurePreserving line 597
  37. lemma OAI.CubicEisenstein.integralCoverFiberPoint_rep_smul line 604
  38. lemma OAI.CubicEisenstein.integralCoverFiber_integrable line 609
  39. theorem OAI.CubicEisenstein.integralCoverTraceFunction_integrable line 623
  40. lemma OAI.CubicEisenstein.integralCoverFiber_integral line 634
  41. theorem OAI.CubicEisenstein.integralCoverTraceFunction_integral line 643