OAI/NumberTheory/CubicGram/Mobius.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Ideal Moebius weights and exact prime-factor subset identities.

  1. def OAI.CubicFirstMoment.idealMoebius line 15
  2. lemma OAI.CubicFirstMoment.idealMoebius_sq line 17
  3. theorem OAI.CubicFirstMoment.norm_gauss_eq_moebius_sq line 25
  4. lemma OAI.CubicFirstMoment.idealMoebius_mul line 29
  5. lemma OAI.CubicFirstMoment.idealMoebius_primaryPrime line 33
  6. lemma OAI.CubicFirstMoment.idealMoebius_prod_primaryPrimes line 36
  7. lemma OAI.CubicFirstMoment.norm_primaryNormalize line 52
  8. lemma OAI.CubicFirstMoment.roughProduct_primary_factors line 56
  9. theorem OAI.CubicFirstMoment.roughProduct_moebius_subsets line 61