OAI/NumberTheory/CubicMoment/Estimates/ShortMoebiusProducts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The short Möbius identity remains valid inside any fixed product of prime-weight factors. This is the algebraic replacement before smoothing.

  1. def OAI.CubicFirstMoment.NormLocalEq line 12
  2. lemma OAI.CubicFirstMoment.NormLocalEq.refl line 15
  3. lemma OAI.CubicFirstMoment.NormLocalEq.mul line 18
  4. lemma OAI.CubicFirstMoment.NormLocalEq.prod line 31
  5. def OAI.CubicFirstMoment.shortVonMangoldt line 42
  6. def OAI.CubicFirstMoment.shortTwoFactor line 45
  7. def OAI.CubicFirstMoment.shortFourFactor line 47
  8. lemma OAI.CubicFirstMoment.shortVonMangoldt_two_four line 50
  9. lemma OAI.CubicFirstMoment.shortVonMangoldt_local line 55
  10. theorem OAI.CubicFirstMoment.shortVonMangoldt_product line 61

    Source documentation

    Every product of von Mangoldt factors can be replaced in the same sharp norm range, with no analytic error term.

    theorem shortVonMangoldt_product {ι : Type*} [Fintype ι]
    {F : ℝ} (hF : 0 ≤ F) (ν : EisensteinIdealExponent) (hν : idealExponentNorm ν ≤ F) :
    MvPowerSeries.coeff ν (∏ _i : ι, idealVonMangoldt) =
      MvPowerSeries.coeff ν (∏ _i : ι, shortVonMangoldt F) :=
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.shortVonMangoldt

  11. theorem OAI.CubicFirstMoment.shortVonMangoldt_product_expansion line 70

    Source documentation

    The exact finite expansion, leaving only two- and four-factor short convolutions for the already proved moment bounds.

    theorem shortVonMangoldt_product_expansion {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : ℝ} (hF : 0 ≤ F) (ν : EisensteinIdealExponent) (hν : idealExponentNorm ν ≤ F) :
    MvPowerSeries.coeff ν (∏ _i : ι, idealVonMangoldt) =
      MvPowerSeries.coeff ν (∑ S ∈ (Finset.univ : Finset ι).powerset,
        (-1 : EisensteinArithmeticFunction)^S.card *
          (∏ _i ∈ S, shortFourFactor F)*
            ∏ _i ∈ Finset.univ\S, 2*shortTwoFactor F) := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.idealVonMangoldt, OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.shortFourFactor, OAI.CubicFirstMoment.shortTwoFactor