OAI/NumberTheory/DirichletL/Eisenstein/FixedThetaTwists.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.fixedThetaTwist_mul line 81
  2. def OAI.CubicEisenstein.fixedThetaRowCoeff line 88
  3. lemma OAI.CubicEisenstein.fixedThetaRowCoeff_norm line 92
  4. theorem OAI.CubicEisenstein.fixedThetaTwist_fixed_fourier line 97
  5. theorem OAI.CubicEisenstein.fixedThetaTwist_free_fourier line 110
  6. theorem OAI.CubicEisenstein.actual_fixedTheta_fourier line 125
  7. lemma OAI.CompletedGauss.admissiblePrimeGood line 157
  8. theorem OAI.CompletedGauss.quadraticRow_eq_primeIndex line 160
  9. theorem OAI.CompletedGauss.completedLocalExponent_residual line 180
  10. theorem OAI.CompletedGauss.residual_bracket_eq_quadraticRow line 186
  11. def OAI.CompletedGauss.residualQuadraticPhase line 197
  12. lemma OAI.CompletedGauss.residualQuadraticPhase_norm_le_one line 200
  13. theorem OAI.CompletedGauss.residual_bracket_extracted_columns line 203
  14. def OAI.CompletedGauss.actualResidualModelRow line 227
  15. lemma OAI.CompletedGauss.actualResidualModelRow_val line 234
  16. lemma OAI.CompletedGauss.actualResidualModelRow_shell line 238
  17. theorem OAI.CompletedGauss.completedBranchScale_raw_argument line 248
  18. def OAI.CompletedGauss.residualModelRowPhase line 272
  19. lemma OAI.CompletedGauss.residualModelRowPhase_norm_le_one line 276
  20. theorem OAI.CompletedGauss.residual_coefficient_eq_canonical line 283
  21. def OAI.CompletedGauss.FreeReflection.pool line 318
  22. lemma OAI.CompletedGauss.FreeReflection.pool_subset line 321
  23. lemma OAI.CompletedGauss.FreeReflection.pool_maximal line 323
  24. lemma OAI.CompletedGauss.FreeReflection.pool_good line 325
  25. lemma OAI.CompletedGauss.FreeReflection.pool_odd line 327
  26. lemma OAI.CompletedGauss.FreeReflection.pool_divides line 329
  27. lemma OAI.CompletedGauss.FreeReflection.pool_nonresidual line 331
  28. lemma OAI.CompletedGauss.FreeReflection.pool_free line 333
  29. lemma OAI.CompletedGauss.FreeReflection.pool_eq_on_fiber line 336
  30. def OAI.CompletedGauss.FreeReflection.reflectionChoiceValue line 348
  31. def OAI.CompletedGauss.FreeReflection.reflectionActivePool line 352
  32. lemma OAI.CompletedGauss.FreeReflection.reflectionActivePool_subset line 355
  33. lemma OAI.CompletedGauss.FreeReflection.mem_reflectionActivePool line 358
  34. lemma OAI.CompletedGauss.FreeReflection.reflectionActivePool_encode line 365
  35. def OAI.CompletedGauss.FreeReflection.reflectionActiveLabel line 379
  36. def OAI.CompletedGauss.FreeReflection.sixReflectedBranch line 383
  37. def OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspBranch line 418
  38. lemma OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspBranch_primes line 428
  39. lemma OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspBranch_amplitude line 436
  40. lemma OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspBranch_scale line 450
  41. def OAI.CompletedGauss.FreeReflection.reflectionInactiveStratumWeight line 473
  42. lemma OAI.CompletedGauss.FreeReflection.reflectionInactiveStratumWeight_norm_le_one line 478
  43. def OAI.CompletedGauss.FreeReflection.reflectionSixInactiveWeight line 495
  44. lemma OAI.CompletedGauss.FreeReflection.reflectionSixInactiveWeight_norm_le_one line 498
  45. lemma OAI.CompletedGauss.FreeReflection.sum_reflectionSixInactiveWeight_unpad line 505
  46. abbrev OAI.CompletedGauss.FreeReflection.SixReflectionIndex line 518
  47. def OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspFiber line 526
  48. theorem OAI.CompletedGauss.FreeReflection.sixPhaseFixedCuspFiber_value line 547