OAI/NumberTheory/DirichletL/PrimeRows/IdealGenerators.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ConcretePrimeRowBridge.idealGenerator_ne_zero line 60
  2. theorem OAI.ConcretePrimeRowBridge.tsum_ideal_eq_tsum_generator line 67
  3. theorem OAI.ActualEisensteinCubic.tsum_rowCoprimeMask_subsets line 97
  4. def OAI.ActualEisensteinCubic.primeSubsetGenerator line 121
  5. theorem OAI.ActualEisensteinCubic.primeSubsetGenerator_ne_zero line 125
  6. theorem OAI.ActualEisensteinCubic.tsum_rowCoprimeMask_dilations line 132
  7. theorem OAI.ActualEisensteinCubic.tsum_masked_radial_dilations line 160
  8. theorem OAI.ActualEisensteinCubic.primeSubset_reducedScale_pos line 192
  9. theorem OAI.ActualEisensteinCubic.canonical_masked_radial_dilations line 199
  10. theorem OAI.ActualEisensteinCubic.canonical_masked_radial_poisson line 219
  11. theorem OAI.ActualEisensteinCubic.canonical_masked_radial_poisson_collected line 251
  12. theorem OAI.ActualEisensteinCubic.canonical_masked_compact_radial_poisson_collected line 292
  13. theorem OAI.GeneralPrimitiveTrace.complex_exp_trace_integer line 324
  14. theorem OAI.GeneralPrimitiveTrace.phase_integer line 338
  15. theorem OAI.GeneralPrimitiveTrace.omega_conj line 343
  16. theorem OAI.GeneralPrimitiveTrace.reconstruction line 352
  17. theorem OAI.GeneralPrimitiveTrace.in_coordinate_lattice_of_two_phases line 366
  18. theorem OAI.GeneralPrimitiveTrace.eisTraceModChar_breveE_primitive line 383
  19. theorem OAI.IdealGaussCRT.coordinateAddChar_isPrimitive line 423
  20. theorem OAI.IdealGaussCRT.norm_gauss_finite_crt_sq line 453
  21. theorem OAI.ActualEisensteinCubic.norm_canonicalGaussSum line 478
  22. theorem OAI.ActualEisensteinCubic.norm_canonicalNormalizedGauss line 513
  23. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_norm_le_one line 526
  24. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_pair_radial_summable line 542
  25. theorem OAI.ActualEisensteinCubic.norm_sq_finite_row_sum line 565
  26. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_smoothed_mean_square_summable line 578
  27. theorem OAI.ActualEisensteinCubic.finiteSquarefreeRow_smoothed_mean_square_expand line 599