OAI/NumberTheory/DirichletL/GaussSum/LocalProductAssembly.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.canonicalSextic_inverse_eq_conj_on_units line 24
  2. theorem OAI.ActualEisensteinCubic.breveLocalG_eq_conjugate line 34
  3. theorem OAI.FourierBridge.coupled_double_log_separation line 54
  4. theorem OAI.AnalyticBridge.double_weighted_fourier_minkowski line 130
  5. theorem OAI.FourierBridge.logPhase_norm line 182
  6. theorem OAI.FourierBridge.logPhase_continuous_left line 186
  7. theorem OAI.AnalyticBridge.bounded_separated_double_integrable line 196
  8. theorem OAI.PowerExtraction.from_finite_sixth_power_rows line 265
  9. def OAI.ActualEisensteinCubic.localA5Kernel line 299
  10. theorem OAI.ActualEisensteinCubic.localA5Kernel_zero line 310
  11. theorem OAI.ActualEisensteinCubic.localA5Kernel_active_eq_raw line 317
  12. def OAI.ActualEisensteinCubic.localA5Output line 338
  13. theorem OAI.ActualEisensteinCubic.localA5Kernel_active_eq_output line 356
  14. theorem OAI.ActualEisensteinCubic.actual_local_product_assembly line 375
  15. theorem OAI.ActualEisensteinCubic.actual_crt_product_assembly line 430
  16. def OAI.ActualEisensteinCubic.crtIntersectionFintype line 487
  17. theorem OAI.ActualEisensteinCubic.actual_crt_product_assembly_finite line 502
  18. theorem OAI.ActualEisensteinCubic.canonicalSextic_sixth_power_mask line 542
  19. def OAI.PoissonFirstLocal.localA line 557
  20. def OAI.PoissonFirstLocal.localC line 558
  21. def OAI.PoissonFirstLocal.localCorrectionE line 560
  22. def OAI.PoissonFirstLocal.localS line 562
  23. def OAI.PoissonFirstLocal.localJ2 line 563
  24. theorem OAI.PoissonFirstLocal.first_poisson_local_scale_identity line 566
  25. theorem OAI.PoissonFirstLocal.first_poisson_global_scale_identity line 580