OAI/NumberTheory/CubicMoment/Estimates/IdealMoebiusBounds.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.finiteIdealMoebius line 12
2. lemma OAI.CubicFirstMoment.coeff_mul_one_sub_X line 15
3. lemma OAI.CubicFirstMoment.tsub_single_away line 23
4. lemma OAI.CubicFirstMoment.coeff_zeta_finiteIdealMoebius line 32

   Source documentation

   Multiplying the zeta series by a finite Euler product excludes precisely the prime divisors occurring in that product.

   lemma coeff_zeta_finiteIdealMoebius (S : Finset EisensteinIdealPrime)
       (ν : EisensteinIdealExponent) :
       MvPowerSeries.coeff ν (idealZeta * finiteIdealMoebius S) =
         if ∀ p ∈ S, ν p = 0 then 1 else 0 := by
   …

   Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealZeta, OAI.CubicFirstMoment.finiteIdealMoebius

5. lemma OAI.CubicFirstMoment.coeff_idealMoebiusSeries_eq_finite line 53

   Source documentation

   For a coefficient whose prime support lies in S, the genuine Dirichlet inverse is computed by the finite Euler product over S.

   lemma coeff_idealMoebiusSeries_eq_finite (S : Finset EisensteinIdealPrime)
       (ν : EisensteinIdealExponent) (hν : ν.support ⊆ S) :
       MvPowerSeries.coeff ν idealMoebiusSeries =
         MvPowerSeries.coeff ν (finiteIdealMoebius S) := by
   …

   Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealMoebiusSeries, OAI.CubicFirstMoment.finiteIdealMoebius

6. lemma OAI.CubicFirstMoment.finiteIdealMoebius_coeff_outside line 83
7. lemma OAI.CubicFirstMoment.finiteIdealMoebius_coeff_repeated line 108
8. lemma OAI.CubicFirstMoment.idealMoebiusSeries_repeated line 140
9. lemma OAI.CubicFirstMoment.finiteIdealMoebius_coeff_squarefree line 146
10. lemma OAI.CubicFirstMoment.idealMoebiusSeries_squarefree line 190
11. lemma OAI.CubicFirstMoment.finiteIdealMoebius_coeff_abs_le_one line 196
12. lemma OAI.CubicFirstMoment.idealMoebiusSeries_abs_le_one line 215

    Source documentation

    The actual Dirichlet-inverse Möbius coefficients have amplitude at most one.

    lemma idealMoebiusSeries_abs_le_one (ν : EisensteinIdealExponent) :
        |MvPowerSeries.coeff ν idealMoebiusSeries| ≤ 1 := by
    …

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealMoebiusSeries

13. lemma OAI.CubicFirstMoment.shortIdealMoebius_abs_le_one line 220
14. lemma OAI.CubicFirstMoment.idealPrimeFactors_normalized line 229

    Source documentation

    Normalized prime representatives identify the exponent multiset with the existing normalized factorization of an Eisenstein element.

    lemma idealPrimeFactors_normalized (a : Eisenstein) :
        (Associates.factors' a).map (fun p => p.val.out) =
          UniqueFactorizationMonoid.normalizedFactors a := by
    …

    Mentions: OAI.CubicFirstMoment.Eisenstein

15. lemma OAI.CubicFirstMoment.idealExponentOf_squarefree_iff line 240
16. lemma OAI.CubicFirstMoment.idealExponentOf_support_card line 250
17. lemma OAI.CubicFirstMoment.idealMoebiusSeries_at_element line 262

    Source documentation

    The Dirichlet-inverse definition agrees with the repository's arithmetic Möbius function on every nonzero Eisenstein ideal.

    lemma idealMoebiusSeries_at_element {a : Eisenstein} (ha : a ≠ 0) :
        MvPowerSeries.coeff (idealExponentOf a) idealMoebiusSeries = (idealMoebius a : ℝ) := by
    …

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.idealMoebiusSeries, OAI.CubicFirstMoment.idealMoebius

18. lemma OAI.CubicFirstMoment.shortIdealMoebius_at_element line 275
19. lemma OAI.CubicFirstMoment.shortIdealMoebius_support line 281