OAI/NumberTheory/DirichletL/GaussSum/DualKernelSummability.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.nonzeroDualIdeal_norm_pos line 83
  2. lemma OAI.CompletedGauss.nonzeroDualIdeal_inv_pow_summable line 87
  3. def OAI.CompletedGauss.rawDualKernelTerm line 96
  4. lemma OAI.CompletedGauss.rawDualKernel_inverse_square line 101
  5. theorem OAI.CompletedGauss.rawDualKernelTerm_summable_norm line 109
  6. lemma OAI.CompletedGauss.canonical_dual_kernel_argument line 158
  7. def OAI.CompletedGauss.canonicalRawBranchCoefficient line 172
  8. lemma OAI.CompletedGauss.canonicalRawBranchCoefficient_norm line 180
  9. theorem OAI.CompletedGauss.reflectedBranchBlock_canonical line 208
  10. theorem OAI.CompletedGauss.canonicalRawBranch_summable_norm line 242
  11. theorem OAI.CompletedGauss.canonical_reflected_series line 258
  12. def OAI.CompletedGauss.ReflectedBranchData.withCanonicalCuspArray line 288
  13. def OAI.CompletedGauss.ReflectedBranchData.rawValue line 305
  14. theorem OAI.CompletedGauss.ReflectedBranchData.withCanonicalCuspArray_value line 318
  15. def OAI.CompletedGauss.ReflectedBranchData.restrictRows line 352
  16. theorem OAI.CompletedGauss.ReflectedBranchData.restrictRows_value line 364
  17. theorem OAI.CompletedGauss.ReflectedBranchData.sum_restrictRows_selected line 375
  18. lemma OAI.CubicEisenstein.ramifiedFrequencyChar_neg_unit line 406
  19. lemma OAI.CubicEisenstein.arithmeticResidueSum_neg_unit line 416
  20. lemma OAI.CubicEisenstein.principalResidueTerm_neg line 438
  21. lemma OAI.CubicEisenstein.principalArithmeticResidue_neg line 446
  22. theorem OAI.CubicEisenstein.sourceArithmeticResidue_neg line 459
  23. lemma OAI.CubicEisenstein.cubicBesselNormalizer_neg line 471
  24. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_neg line 474
  25. lemma OAI.CubicEisenstein.sourceRayPhase_eq_one_iff_coordinate line 485
  26. lemma OAI.CubicEisenstein.primary_or_negative_primary_of_source_mask line 498
  27. theorem OAI.CubicEisenstein.sourceFourier_supported_three_of_base_zero line 534
  28. theorem OAI.CubicEisenstein.infinityCoefficientScalar_ne_zero line 548
  29. lemma OAI.CubicEisenstein.sourceResidualFourierCoefficient_one_ne_zero line 553
  30. lemma OAI.CubicEisenstein.sourceArithmeticResidue_one_ne_zero line 557
  31. theorem OAI.CubicEisenstein.normalized_infinityCoefficient_squarefree_cube line 561