OAI/NumberTheory/DirichletL/Eisenstein/PrimitiveRows.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.levelThree_of_entries line 77
  2. lemma OAI.CubicEisenstein.row_coprime line 92
  3. lemma OAI.CubicEisenstein.exists_matrix_of_primitive_row line 101
  4. def OAI.CubicEisenstein.PrimitiveRow line 125
  5. def OAI.CubicEisenstein.cosetPrimitiveRow line 128
  6. lemma OAI.CubicEisenstein.cosetPrimitiveRow_bijective line 134
  7. def OAI.CubicEisenstein.primitiveRowEquiv line 148
  8. lemma OAI.CubicEisenstein.inverse_character_eq_row_symbol line 152
  9. lemma OAI.CubicEisenstein.inverse_cosetCharacter_eq_row_symbol line 180
  10. def OAI.CubicEisenstein.primitiveRowPhase line 184
  11. lemma OAI.CubicEisenstein.primitiveRowEquiv_val line 187
  12. lemma OAI.CubicEisenstein.primitiveRowEquiv_symm_row line 189
  13. theorem OAI.CubicEisenstein.upperEisenstein_eq_primitive_rows line 193
  14. theorem OAI.CubicEisenstein.primitive_rows_summable_norm line 206
  15. lemma OAI.CubicEisenstein.primitiveRow_zero_left line 216
  16. def OAI.TruncatedPrincipalPoisson.radialSource line 229
  17. def OAI.TruncatedPrincipalPoisson.radialDual line 232
  18. theorem OAI.TruncatedPrincipalPoisson.radialSource_summable line 235
  19. theorem OAI.TruncatedPrincipalPoisson.radialSource_poisson line 244
  20. def OAI.TruncatedPrincipalPoisson.subsetNorm line 266
  21. def OAI.TruncatedPrincipalPoisson.subsetMobius line 269
  22. def OAI.TruncatedPrincipalPoisson.smallDivisors line 272
  23. def OAI.TruncatedPrincipalPoisson.largeDivisors line 275
  24. theorem OAI.TruncatedPrincipalPoisson.subsetNorm_pos line 278
  25. theorem OAI.TruncatedPrincipalPoisson.sum_small_add_large line 283
  26. theorem OAI.TruncatedPrincipalPoisson.masked_radialSource_dilations line 290
  27. theorem OAI.TruncatedPrincipalPoisson.masked_radialSource_truncated line 311
  28. theorem OAI.TruncatedPrincipalPoisson.masked_radialSource_truncated_euler line 332
  29. def OAI.TruncatedPrincipalPoisson.middleDivisors line 358
  30. def OAI.TruncatedPrincipalPoisson.dualNear line 361
  31. def OAI.TruncatedPrincipalPoisson.dualFar line 365
  32. theorem OAI.TruncatedPrincipalPoisson.radialDual_summable line 369
  33. theorem OAI.TruncatedPrincipalPoisson.radialDual_near_add_far line 376
  34. theorem OAI.TruncatedPrincipalPoisson.sum_small_add_middle line 391
  35. theorem OAI.TruncatedPrincipalPoisson.masked_radialSource_five_pieces line 409
  36. theorem OAI.EisensteinSchwartzPoisson.radial_source_nonzero_lattice_decay line 448
  37. theorem OAI.TruncatedPrincipalPoisson.zero_removed_tsum line 502
  38. theorem OAI.TruncatedPrincipalPoisson.radialSource_inverse_decay line 512
  39. theorem OAI.TruncatedPrincipalPoisson.radialDual_decay line 529
  40. theorem OAI.TruncatedPrincipalPoisson.subsetMobius_norm_le_one line 553
  41. theorem OAI.TruncatedPrincipalPoisson.scale_tail_bound line 556
  42. theorem OAI.TruncatedPrincipalPoisson.norm_sum_subsets_le line 570
  43. theorem OAI.TruncatedPrincipalPoisson.small_divisor_dual_tail line 584
  44. theorem OAI.TruncatedPrincipalPoisson.large_divisor_source_tail line 616