OAI/NumberTheory/DirichletL/GaussSum/ActiveConductor.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.activeSupport_nonempty_of_ne line 69
  2. theorem OAI.ActualEisensteinCubic.activeRow_zero_of_ne line 78
  3. theorem OAI.ActualEisensteinCubic.finiteSexticRow_of_isEmpty line 88
  4. theorem OAI.ActualEisensteinCubic.finitePrimeModulus_norm_of_isEmpty line 94
  5. theorem OAI.ActualEisensteinCubic.canonicalGaussSum_of_isEmpty line 100
  6. theorem OAI.ActualEisensteinCubic.canonicalNormalizedGauss_of_isEmpty line 120
  7. def OAI.ActualEisensteinCubic.squarefreePairPoissonZeroMode line 128
  8. theorem OAI.ActualEisensteinCubic.squarefreePairPoissonZeroMode_eq_zero_of_ne line 144
  9. theorem OAI.ActualEisensteinCubic.squarefreePairPoissonZeroMode_diag line 152
  10. theorem OAI.ActualEisensteinCubic.primeSubset_moebius_norm_sum line 178
  11. theorem OAI.ActualEisensteinCubic.primeDensity_nonneg_le_one line 191
  12. theorem OAI.ActualEisensteinCubic.squarefreePairPoissonZeroMode_diag_product line 207
  13. theorem OAI.ActualEisensteinCubic.norm_squarefreePairPoissonZeroMode_diag_le line 216
  14. def OAI.ConcretePrimeRowBridge.idealPairPoissonZeroMode line 237
  15. theorem OAI.ConcretePrimeRowBridge.weighted_idealPairPoissonZeroMode_eq_zero_of_ne line 247
  16. theorem OAI.ConcretePrimeRowBridge.idealRowSum_zeroMode_diagonal line 269
  17. theorem OAI.ConcretePrimeRowBridge.norm_idealRowSum_zeroMode_le line 291
  18. theorem OAI.ActualEisensteinCubic.activeRow_norm_le_one line 323
  19. theorem OAI.ActualEisensteinCubic.activeRow_paperFourier_summable line 335
  20. theorem OAI.ActualEisensteinCubic.activeRow_paperFourier_zero_split line 349
  21. def OAI.ActualEisensteinCubic.squarefreePairPoissonNonzeroMode line 369
  22. theorem OAI.ActualEisensteinCubic.squarefreePairPoissonKernel_zero_split line 387
  23. def OAI.ConcretePrimeRowBridge.idealPrimeDensity line 414
  24. theorem OAI.ConcretePrimeRowBridge.idealPrimeDensity_mem_Icc line 417
  25. theorem OAI.ConcretePrimeRowBridge.idealPairPoissonZeroMode_diag line 423
  26. theorem OAI.ConcretePrimeRowBridge.idealRowSum_zeroMode_formula line 441
  27. def OAI.ConcretePrimeRowBridge.idealPairPoissonNonzeroMode line 460
  28. theorem OAI.ConcretePrimeRowBridge.idealPairPoissonKernel_zero_split line 470
  29. theorem OAI.ConcretePrimeRowBridge.idealRowSum_smoothed_poisson_zero_split line 483
  30. theorem OAI.ShortDraftHeckeBridge.norm_baseChangeWeight_le_one line 508
  31. theorem OAI.ConcretePrimeRowBridge.norm_idealRowSum_zeroMode_le_test_mass line 524
  32. theorem OAI.ConcretePrimeRowBridge.idealSupport_image_eq_factors line 545
  33. theorem OAI.ConcretePrimeRowBridge.idealSupport_product_eq line 558
  34. theorem OAI.ActualEisensteinCubic.activeSupport_product_mul_common_sq line 578
  35. theorem OAI.ActualEisensteinCubic.activePrimeModulus_norm_sq line 595
  36. theorem OAI.ConcretePrimeRowBridge.idealSupport_active_conductor_mul_common_sq line 608
  37. theorem OAI.ConcretePrimeRowBridge.idealPairPoisson_conductor_norm_sq line 616
  38. theorem OAI.ConcretePrimeRowBridge.idealPairPoisson_conductor_norm_sq_of_weight_ne_zero line 628