OAI/NumberTheory/JointDickman/Arithmetic/RoughLeadingCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The leading coefficient after the roughness cutoff

Mertens' product theorem and the convergent squarefree Euler factor give the precise constant exp(-γ z) / Gamma(z).

  1. def OAI.JointDickman.roughLeadingCoefficient line 19
  2. theorem OAI.JointDickman.roughLeadingCoefficient_identity line 22
  3. theorem OAI.JointDickman.roughLeadingCoefficient_tendsto line 52

    Source documentation

    Only the cited Mertens product input is used in this normalization.

    theorem roughLeadingCoefficient_tendsto
    (hM : PublishedInputs.PrimeProductMertensInput) {z : ℝ}
    (hz : 0 < z) (hz1 : z ≤ 1) :
    Tendsto (fun P => roughLeadingCoefficient z P * (Real.log P) ^ z) atTop
      (𝓝 (Real.exp (-Real.eulerMascheroniConstant * z) / Real.Gamma z)) := by
…

    Mentions: OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.roughLeadingCoefficient