OAI/NumberTheory/DirichletL/Moments/Active.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentActive.netExponent line 13
  2. theorem OAI.SevenEighths.CenteredMomentActive.local_pair_reduction line 15
  3. def OAI.SevenEighths.CenteredMomentActive.activeSupport line 32
  4. def OAI.SevenEighths.CenteredMomentActive.principalSupport line 35
  5. theorem OAI.SevenEighths.CenteredMomentActive.netExponent_ne_zero line 38
  6. theorem OAI.SevenEighths.CenteredMomentActive.netExponent_lt_six line 42
  7. theorem OAI.SevenEighths.CenteredMomentActive.principal_product_eq_mask line 44
  8. theorem OAI.SevenEighths.CenteredMomentActive.common_ideal_pair_active line 63
  9. theorem OAI.SevenEighths.CenteredMomentActive.activePrimes_pairwise_coprime line 94
  10. theorem OAI.SevenEighths.CenteredMomentActive.active_gauss_norm line 101
  11. theorem OAI.SevenEighths.CenteredMomentActive.common_ideal_pair_poisson line 114