OAI/NumberTheory/DirichletL/RowCompletion/PeriodicRows.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CanonicalRowCompletion.numeratorBadTwist_zero_of_not_supported line 82
  2. lemma OAI.CanonicalRowCompletion.rowTwist_zero_of_not_supported line 92
  3. def OAI.CanonicalRowCompletion.actualPeriodicRow line 102
  4. lemma OAI.CanonicalRowCompletion.actualPeriodicRow_norm line 106
  5. lemma OAI.CanonicalRowCompletion.actualPeriodicRow_periodic line 117
  6. theorem OAI.CanonicalRowCompletion.rowTwist_eq_actualPeriodicRow_primary line 133
  7. theorem OAI.CanonicalRowCompletion.exists_actual_periodic_row line 148
  8. def OAI.CompletedGauss.completedReflectionPool line 176
  9. lemma OAI.CompletedGauss.mem_completedReflectionPool line 179
  10. lemma OAI.CompletedGauss.completedReflectionPool_maximal line 186
  11. lemma OAI.CompletedGauss.completedReflectionPool_good line 193
  12. lemma OAI.CompletedGauss.completedReflectionPool_odd line 196
  13. lemma OAI.CompletedGauss.completedReflectionPool_nonresidual line 199
  14. lemma OAI.CompletedGauss.completedReflectionPool_divides line 202
  15. lemma OAI.CompletedGauss.completedReflectionPool_coprime line 206
  16. theorem OAI.CompletedGauss.completedReflectionPool_eq_on_fiber line 212
  17. lemma OAI.CompletedGauss.completedReflectionPool_exponent_eq line 227
  18. theorem OAI.CompletedGauss.completedBranchScale_eq_on_fiber line 237
  19. def OAI.CompletedGauss.reflectionSixActive line 252
  20. def OAI.CompletedGauss.reflectionSixLabel line 254
  21. def OAI.CompletedGauss.reflectionSixValid line 256
  22. def OAI.CompletedGauss.encodeReflectionSix line 261
  23. def OAI.CompletedGauss.reflectionSixSupport line 264
  24. def OAI.CompletedGauss.decodeReflectionSix line 267
  25. lemma OAI.CompletedGauss.reflectionSixActive_encode line 271
  26. lemma OAI.CompletedGauss.encodeReflectionSix_valid line 278
  27. lemma OAI.CompletedGauss.reflectionSixSupport_encode line 286
  28. lemma OAI.CompletedGauss.encodeReflectionSix_injective line 292
  29. lemma OAI.CompletedGauss.encode_decodeReflectionSix line 309
  30. lemma OAI.CompletedGauss.decode_encodeReflectionSix line 325
  31. def OAI.CompletedGauss.reflectionSixEquiv line 329
  32. theorem OAI.CompletedGauss.sum_active_exceptional_eq_six line 335
  33. def OAI.CompletedGauss.reflectionStratumWeight line 371
  34. lemma OAI.CompletedGauss.reflectionStratumWeight_norm_le_one line 379
  35. def OAI.CompletedGauss.reflectionSixWeight line 402
  36. lemma OAI.CompletedGauss.reflectionSixWeight_norm_le_one line 408
  37. theorem OAI.CompletedGauss.sum_reflectionStratumWeight_eq_six line 418
  38. theorem OAI.CompletedGauss.stratum_weighted_brackets_eq_branches line 431
  39. theorem OAI.CompletedGauss.sum_reflectionSixWeight_unpad line 447
  40. def OAI.CompletedGauss.reflectionChoiceValue line 467
  41. def OAI.CompletedGauss.reflectionActivePool line 471
  42. lemma OAI.CompletedGauss.reflectionActivePool_subset line 474
  43. lemma OAI.CompletedGauss.mem_reflectionActivePool line 477
  44. lemma OAI.CompletedGauss.reflectionActivePool_encode line 484
  45. def OAI.CompletedGauss.reflectionActiveLabel line 498
  46. def OAI.CompletedGauss.sixReflectedBranch line 502
  47. def OAI.CompletedGauss.sixFixedCuspBranch line 531
  48. lemma OAI.CompletedGauss.sixFixedCuspBranch_primes line 539
  49. lemma OAI.CompletedGauss.sixFixedCuspBranch_scale line 546
  50. def OAI.CompletedGauss.reflectionInactiveStratumWeight line 566
  51. lemma OAI.CompletedGauss.reflectionInactiveStratumWeight_norm_le_one line 571
  52. def OAI.CompletedGauss.reflectionSixInactiveWeight line 588
  53. lemma OAI.CompletedGauss.reflectionSixInactiveWeight_norm_le_one line 591
  54. lemma OAI.CompletedGauss.sum_reflectionSixInactiveWeight_unpad line 598
  55. abbrev OAI.CompletedGauss.SixReflectionIndex line 611
  56. def OAI.CompletedGauss.sixFixedCuspFiber line 614
  57. theorem OAI.CompletedGauss.sixFixedCuspFiber_value line 633