L Functions

Results named in Tau Ceti's TauCeti.NumberTheory.LFunctions modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremChebyshev's identity for a number field#

Summing log N𝔞 = ∑_{𝔟 ∣ 𝔞} Λ_K(𝔟) over the nonzero integral ideals of norm at most x and exchanging the order of summation, ∑_{N𝔞 ≤ x} log N𝔞 = ∑_{N(𝔭 ^ k) ≤ x} log N𝔭 · #{𝔞 : N𝔞 ≤ x / N(𝔭 ^ k)}.

TauCeti.LFunctions.idealSummatory_log_absNorm_eq.{u_1} (K : Type u_1) [Field K] [NumberField K]
  (x : ℝ) :
  TauCeti.idealSummatory K (fun I => Real.log ↑(Ideal.absNorm ↑I)) x =
    TauCeti.primePowerSummatory K
      (fun A => TauCeti.primePowerWeight A * ↑(TauCeti.idealsLE K (x / ↑(Ideal.absNorm ↑↑A))).card)
      x

Lean

Formalized in Tau Ceti as TauCeti.LFunctions.idealSummatory_log_absNorm_eq.

Sources

• Tau Ceti documentation: TauCeti.LFunctions.idealSummatory_log_absNorm_eq
• Source of TauCeti.LFunctions.idealSummatory_log_absNorm_eq in TauCeti/NumberTheory/LFunctions/Mertens.lean

LeanTauCeti.LFunctions.idealSummatory_log_absNorm_eq

Uses 1 · Used by 1

Proof usesThe analytic Euler product

Used byMertens' first theorem for a number field

TheoremMertens' first theorem for a number field#

The sum of log N𝔭 / N𝔭 over the nonzero prime ideals 𝔭 of 𝓞 K of norm at most x is log x + O(1).

TauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log.{u_1} (K : Type u_1) [Field K]
  [NumberField K] :
  (fun x =>
      TauCeti.primeSummatory K
          (fun v => Real.log ↑(Ideal.absNorm v.asIdeal) / ↑(Ideal.absNorm v.asIdeal)) x -
        Real.log x) =O[Filter.atTop]
    fun x => 1

Lean

Formalized in Tau Ceti as TauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log.

Other forms

Mertens' first theorem for a number field, prime-power form. Formalized in Tau Ceti as TauCeti.LFunctions.isBigO_primePowerSummatory_div_sub_log.

TauCeti.LFunctions.isBigO_primePowerSummatory_div_sub_log.{u_1} (K : Type u_1) [Field K]
  [NumberField K] :
  (fun x =>
      TauCeti.primePowerSummatory K (fun A => TauCeti.primePowerWeight A / ↑(Ideal.absNorm ↑↑A)) x -
        Real.log x) =O[Filter.atTop]
    fun x => 1

Sources

• Tau Ceti documentation: TauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log
• Source of TauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log in TauCeti/NumberTheory/LFunctions/Mertens.lean

LeanTauCeti.LFunctions.isBigO_primeSummatory_log_absNorm_div_sub_log · TauCeti.LFunctions.isBigO_primePowerSummatory_div_sub_log

Uses 3 · Used by 1

Proof usesA negative-power Abel bound · Chebyshev's identity for a number field · The prime ideal theorem

Used byMertens' second theorem for a number field

TheoremMertens' second theorem for a number field#

The sum of 1 / N𝔭 over the nonzero prime ideals 𝔭 of 𝓞 K of norm at most x is log log x + B_K + O(1 / log x), where B_K = mertensConstant K.

TauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant.{u_1}
  (K : Type u_1) [Field K] [NumberField K] :
  (fun x =>
      TauCeti.primeSummatory K (fun v => (↑(Ideal.absNorm v.asIdeal))⁻¹) x - Real.log (Real.log x) -
        TauCeti.LFunctions.mertensConstant K) =O[Filter.atTop]
    fun x => (Real.log x)⁻¹

Lean

Formalized in Tau Ceti as TauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant.

Other forms

Mertens' second theorem for a number field, limit form. Formalized in Tau Ceti as TauCeti.LFunctions.tendsto_primeSummatory_inv_absNorm_sub_log_log.

TauCeti.LFunctions.tendsto_primeSummatory_inv_absNorm_sub_log_log.{u_1} (K : Type u_1) [Field K]
  [NumberField K] :
  Filter.Tendsto
    (fun x =>
      TauCeti.primeSummatory K (fun v => (↑(Ideal.absNorm v.asIdeal))⁻¹) x - Real.log (Real.log x))
    Filter.atTop (nhds (TauCeti.LFunctions.mertensConstant K))

Sources

• Tau Ceti documentation: TauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant
• Source of TauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant in TauCeti/NumberTheory/LFunctions/Mertens.lean

LeanTauCeti.LFunctions.isBigO_primeSummatory_inv_absNorm_sub_log_log_sub_mertensConstant · TauCeti.LFunctions.tendsto_primeSummatory_inv_absNorm_sub_log_log

Uses 1

Proof usesMertens' first theorem for a number field

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.