OAI/NumberTheory/CubicMoment/Estimates/ShortConvolutionExpansion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Each term of the short Möbius product expansion is an actual finite family of the three permitted arithmetic factors.

  1. abbrev OAI.CubicFirstMoment.shortBranchIndex line 14
  2. instance OAI.CubicFirstMoment.shortBranchIndex_fintype line 16
  3. instance OAI.CubicFirstMoment.shortBranchIndex_decidableEq line 19
  4. def OAI.CubicFirstMoment.shortBranchFactor line 22
  5. lemma OAI.CubicFirstMoment.shortBranchFactor_spec line 26
  6. lemma OAI.CubicFirstMoment.shortBranchFactor_product line 32
  7. theorem OAI.CubicFirstMoment.short_prime_product_expansion line 41

    Source documentation

    Explicit finite short-factor expansion on each primary norm ball.

    theorem short_prime_product_expansion {F : ℝ} (hF : 0 ≤ F)
    (ν : EisensteinIdealExponent) (hν : idealExponentNorm ν ≤ F) :
    MvPowerSeries.coeff ν (∏ _i : ι, idealVonMangoldt) =
      ∑ S ∈ (Finset.univ : Finset ι).powerset,
        (-1 : ℝ)^S.card * 2^(Fintype.card ι-S.card) *
          MvPowerSeries.coeff ν (∏ i, shortBranchFactor F S i) := by
…

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