OAI/NumberTheory/CubicMoment/Estimates/IdealDirichletInverse.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

An absolutely convergent Möbius inverse of the complete ideal Hecke series. In particular the actual series has no zeros to the right of one.

  1. lemma OAI.CubicFirstMoment.ideal_cauchy_product line 13
  2. lemma OAI.CubicFirstMoment.idealDirichlet_norm_summable line 22
  3. lemma OAI.CubicFirstMoment.idealDirichlet_weight_add line 28
  4. lemma OAI.CubicFirstMoment.idealMoebius_antidiagonal line 36
  5. lemma OAI.CubicFirstMoment.idealMoebius_twist_summable line 45
  6. lemma OAI.CubicFirstMoment.idealMoebius_twist_convolution line 53
  7. lemma OAI.CubicFirstMoment.idealMoebius_cauchy line 72
  8. lemma OAI.CubicFirstMoment.idealMoebius_tsum_mul line 80
  9. theorem OAI.CubicFirstMoment.idealDirichlet_moebius_mul line 93

    Source documentation

    The literal complete ideal series has its absolutely convergent Möbius-twisted inverse on Re(s)>1.

    theorem idealDirichlet_moebius_mul (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν, ‖χ ν‖ ≤ 1) (hχ0 : χ 0=1)
    (hχadd : ∀ ν κ, χ (ν+κ)=χ ν*χ κ) {s : ℂ} (hs : 1 < s.re) :
    normDirichletSeries (fun ν => ((MvPowerSeries.coeff ν idealMoebiusSeries:ℝ):ℂ)*χ ν)
      idealExponentNorm s * normDirichletSeries χ idealExponentNorm s = 1 := by
…

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

  10. theorem OAI.CubicFirstMoment.idealDirichlet_ne_zero line 104