OAI/NumberTheory/DirichletL/Eisenstein/ResidualOrthogonality.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_kernel_invariant line 84
  2. def OAI.CubicEisenstein.cubicSourceQuotientFunction line 94
  3. lemma OAI.CubicEisenstein.cubicSourceQuotientFunction_projection line 99
  4. lemma OAI.CubicEisenstein.cubicSourceQuotientFunction_measurable line 103
  5. lemma OAI.CubicEisenstein.cubicSourceQuotientFunction_represents line 107
  6. abbrev OAI.CubicKubota.CubeLegIndex line 122
  7. def OAI.CubicKubota.cubeLegTarget line 124
  8. lemma OAI.CubicKubota.cubeLegTarget_le line 128
  9. lemma OAI.CubicKubota.cubeLegTarget_finiteIndex line 134
  10. def OAI.CubicKubota.cubeLegEquiv line 140
  11. def OAI.CubicKubota.cubeLegMatrix line 145
  12. lemma OAI.CubicKubota.cubeLeg_intertwines line 149
  13. def OAI.CubicKubota.cubeLeg line 158
  14. def OAI.CubicKubota.cubeLegCoefficient line 166
  15. def OAI.CubicKubota.cubeLegQuotientFunction line 170
  16. lemma OAI.CubicKubota.cubeLegQuotientFunction_projection line 177
  17. lemma OAI.CubicKubota.cubeLegQuotientFunction_measurable line 182
  18. lemma OAI.CubicKubota.cubeLeg_representative line 188
  19. def OAI.CubicKubota.cubeDifferenceL2 line 198
  20. def OAI.CubicKubota.cubeDifferenceQuotientFunction line 202
  21. lemma OAI.CubicKubota.cubeDifferenceQuotientFunction_projection line 206
  22. lemma OAI.CubicKubota.cubeDifferenceQuotientFunction_measurable line 217
  23. lemma OAI.CubicKubota.cubeDifferenceL2_representative line 225
  24. lemma OAI.CubicEisenstein.sourceCuspLeadingCoefficient_ramified line 258
  25. theorem OAI.CubicEisenstein.sourceCuspRemainder_representatives_decay line 264
  26. theorem OAI.CubicEisenstein.cubeSourceDifference_cubic_decay line 293
  27. lemma OAI.CubicEisenstein.cubeCuspTriangular_norm_sq_le line 308
  28. lemma OAI.CubicEisenstein.cubeReducedRemainder_bound_from_height line 317
  29. theorem OAI.CubicEisenstein.cubeSourceDifference_cubic_decay_from_height line 348
  30. def OAI.CubicEisenstein.cubeInverseLeftMatrix line 386
  31. lemma OAI.CubicEisenstein.cubeAverageMatrix_inverse_factor line 389
  32. lemma OAI.CubicEisenstein.cubeAverageMatrix_inverse_cusp_factor line 404
  33. theorem OAI.CubicEisenstein.cubeSourceDifference_inverse_cubic_decay line 427
  34. lemma OAI.CubicEisenstein.kernelSourcePullback_pairing_inverse line 478
  35. lemma OAI.CubicEisenstein.kernelSourcePullback_integral_cusp_decay line 485
  36. lemma OAI.CubicEisenstein.cubicEisensteinResidue_source_translate_orthogonal line 499
  37. theorem OAI.CubicEisenstein.cubicSourceResidue_orthogonal_of_integral_cusp_decay line 518
  38. theorem OAI.CubicEisenstein.commonCover_source_span_vanish line 530
  39. theorem OAI.CubicEisenstein.kernelCoverLeg_adjoint_sum_eigenvector line 563