OAI/NumberTheory/DirichletL/Eisenstein/FixedCuspArrays.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.sourceCuspCoefficients_full_support line 85
  2. lemma OAI.CubicEisenstein.sourceCuspRadialCoefficient_full_support line 98
  3. theorem OAI.CubicEisenstein.sourceCuspRadialCoefficient_tsum_full_index line 107
  4. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_full_index line 124
  5. lemma OAI.CubicEisenstein.SourceCuspDatum.smoothedKernel_full_index_norm_summable line 138
  6. theorem OAI.CubicEisenstein.completedT_finite_smoothed_full_index line 162
  7. def OAI.CubicEisenstein.fixedCuspCoefficientBound line 195
  8. lemma OAI.CubicEisenstein.fixedCuspCoefficientBound_pos line 198
  9. def OAI.CubicEisenstein.fixedCuspArrayIndex line 201
  10. def OAI.CubicEisenstein.fixedCuspArrayEligible line 204
  11. def OAI.CubicEisenstein.fixedCuspArrayWeight line 207
  12. lemma OAI.CubicEisenstein.fixedCuspArrayWeight_nonneg line 210
  13. lemma OAI.CubicEisenstein.fixedCuspArrayWeight_pos line 215
  14. lemma OAI.CubicEisenstein.sourceCuspCoefficients_squarefree_cube_bound line 220
  15. def OAI.CubicEisenstein.fixedCuspArray line 233
  16. lemma OAI.CubicEisenstein.fixedCuspArray_zero_of_ineligible line 239
  17. lemma OAI.CubicEisenstein.fixedCuspArray_norm_le_one line 243
  18. lemma OAI.CubicEisenstein.fixedCuspArray_reconstruct line 251
  19. def OAI.CubicEisenstein.fixedConjugateCuspArray line 258
  20. lemma OAI.CubicEisenstein.fixedConjugateCuspArray_norm_le_one line 261
  21. lemma OAI.CubicEisenstein.fixedConjugateCuspArray_reconstruct line 265
  22. lemma OAI.CubicEisenstein.fixedConjugateCuspArray_reconstruct_explicit line 273
  23. theorem OAI.IdealGaussCRT.finiteAdditiveFourierCoeff_crt line 291
  24. theorem OAI.IdealGaussCRT.finite_fourier_weighted_crt line 312
  25. def OAI.LocalReflectionBrackets.frequencyMultiplier line 335
  26. def OAI.LocalReflectionBrackets.frequencyRow line 339
  27. lemma OAI.LocalReflectionBrackets.frequencyRow_zero line 343
  28. lemma OAI.LocalReflectionBrackets.frequencyRow_units line 351
  29. theorem OAI.LocalReflectionBrackets.canonical_frequencyRow_zero line 366
  30. theorem OAI.LocalReflectionBrackets.canonical_frequencyRow_units line 374
  31. theorem OAI.LocalReflectionBrackets.canonical_finite_reflection_crt line 390
  32. theorem OAI.LocalReflectionBrackets.canonical_principal_reflection_crt line 424
  33. lemma OAI.CubicEisenstein.upper_right_removed_bottom line 460
  34. lemma OAI.CubicEisenstein.upper_right_removed_top line 465
  35. lemma OAI.CubicEisenstein.upper_right_removed_last line 470
  36. lemma OAI.CubicEisenstein.upper_diagonal_product line 475
  37. structure OAI.CubicEisenstein.FixedCuspShape line 479
  38. lemma OAI.CubicEisenstein.exists_fixedCuspShape line 488
  39. lemma OAI.CubicEisenstein.FixedCuspShape.removed_eq line 495
  40. def OAI.CubicEisenstein.FixedCuspShape.datum line 502
  41. lemma OAI.CubicEisenstein.FixedCuspShape.datum_matrix line 510
  42. lemma OAI.CubicEisenstein.FixedCuspShape.datum_point line 515
  43. lemma OAI.CubicEisenstein.FixedCuspShape.datum_heightScale line 524
  44. lemma OAI.CubicEisenstein.FixedCuspShape.datum_dualPoint line 534
  45. lemma OAI.CubicEisenstein.FixedCuspShape.datum_multiplier line 551
  46. lemma OAI.CubicEisenstein.FixedCuspShape.datum_additive_phase line 569
  47. def OAI.CompletedGauss.ReflectedBranchData.withFixedCuspArray line 595
  48. lemma OAI.CompletedGauss.ReflectedBranchData.withFixedCuspArray_amplitude line 602
  49. theorem OAI.CompletedGauss.ReflectedBranchData.withFixedCuspArray_value line 609
  50. def OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArray line 625
  51. lemma OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArray_norm_le_one line 634
  52. lemma OAI.CompletedGauss.ReflectedBranchData.extractedFixedCuspArray_zero line 639
  53. def OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArray line 651
  54. lemma OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArray_amplitude line 658
  55. theorem OAI.CompletedGauss.ReflectedBranchData.withExtractedFixedCuspArray_value line 665