Arithmetic Dirichlet Series

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

TheoremA negative-power Abel bound#

Suppose every index has N-value at least 1, and the partial sums of a real weight w are at most C * t ^ β on [1, x]. Twisting the weight by (N i) ^ (-α) with α ≥ 0 gives partial sums at most C x ^ (β - α) + α C (x ^ (β - α) - 1) / (β - α).

For β > α this is O(x ^ (β - α)), and for β < α it is bounded uniformly in x. No sign condition is imposed on w: only its partial sums are controlled.

TauCeti.summatory_mul_rpow_neg_le.{u_1} {ι : Type u_1} (N : ι → ℕ) [Northcott N]
  (hN : ∀ (i : ι), 1 ≤ ↑(N i)) (w : ι → ℝ) {C α β x : ℝ} (hα : 0 ≤ α) (hβα : β ≠ α) (hx : 1 ≤ x)
  (hC : ∀ t ∈ Set.Icc 1 x, TauCeti.summatory N w t ≤ C * t ^ β) :
  TauCeti.summatory N (fun i => w i * ↑(N i) ^ (-α)) x ≤
    C * x ^ (β - α) + α * C * ((x ^ (β - α) - 1) / (β - α))

Lean

Formalized in Tau Ceti as TauCeti.summatory_mul_rpow_neg_le.

Sources

• Tau Ceti documentation: TauCeti.summatory_mul_rpow_neg_le
• Source of TauCeti.summatory_mul_rpow_neg_le in TauCeti/NumberTheory/ArithmeticDirichletSeries/AbelSummation.lean

LeanTauCeti.summatory_mul_rpow_neg_le

Used by 1

Used byMertens' first theorem for a number field

TheoremA one-sided Abel bound#

Let every index have N-value at least the cutoff a ≥ 0, and let g be nonincreasing on [a, x] with 0 ≤ g x. If the summatory function of a real weight w is at most C at every cutoff in [a, x], then the summatory function at x of the twisted weight i ↦ w i * g (N i) is at most C * g a.

No sign condition is imposed on w or on C: only the partial sums of w are controlled.

TauCeti.summatory_mul_le_of_summatory_le.{u_1} {ι : Type u_1} (N : ι → ℕ) [Northcott N] {a : ℝ}
  (ha : 0 ≤ a) (hN : ∀ (i : ι), a ≤ ↑(N i)) (w : ι → ℝ) {g : ℝ → ℝ} {C x : ℝ} (hx : a ≤ x)
  (hC : ∀ t ∈ Set.Icc a x, TauCeti.summatory N w t ≤ C)
  (hg_diff : ∀ t ∈ Set.Icc a x, DifferentiableAt ℝ g t)
  (hg_int : MeasureTheory.IntegrableOn (deriv g) (Set.Icc a x) MeasureTheory.volume)
  (hg_deriv : ∀ t ∈ Set.Icc a x, deriv g t ≤ 0) (hg_nonneg : 0 ≤ g x) :
  TauCeti.summatory N (fun i => w i * g ↑(N i)) x ≤ C * g a

Lean

Formalized in Tau Ceti as TauCeti.summatory_mul_le_of_summatory_le.

Other forms

A one-sided Abel bound for the full series. Formalized in Tau Ceti as TauCeti.tsum_mul_le_of_summatory_le.

TauCeti.tsum_mul_le_of_summatory_le.{u_1} {ι : Type u_1} (N : ι → ℕ) [Northcott N] {a : ℝ}
  (ha : 0 ≤ a) (hN : ∀ (i : ι), a ≤ ↑(N i)) (w : ι → ℝ) {g : ℝ → ℝ} {C : ℝ}
  (hC : ∀ (t : ℝ), a ≤ t → TauCeti.summatory N w t ≤ C)
  (hg_diff : ∀ (t : ℝ), a ≤ t → DifferentiableAt ℝ g t)
  (hg_int :
    ∀ (x : ℝ), a ≤ x → MeasureTheory.IntegrableOn (deriv g) (Set.Icc a x) MeasureTheory.volume)
  (hg_deriv : ∀ (t : ℝ), a ≤ t → deriv g t ≤ 0) (hg_nonneg : ∀ (t : ℝ), a ≤ t → 0 ≤ g t)
  (hsum : Summable fun i => w i * g ↑(N i)) : ∑' (i : ι), w i * g ↑(N i) ≤ C * g a

Sources

• Tau Ceti documentation: TauCeti.summatory_mul_le_of_summatory_le
• Source of TauCeti.summatory_mul_le_of_summatory_le in TauCeti/NumberTheory/ArithmeticDirichletSeries/AbelSummation.lean

LeanTauCeti.summatory_mul_le_of_summatory_le · TauCeti.tsum_mul_le_of_summatory_le

Used by 1

Used byDirichlet's theorem on primes in arithmetic progressions, with Dirichlet density

TheoremAn imaginary-power Abel bound#

Suppose every index has N-value at least 1, and the partial sums of w are bounded by C * t ^ θ on [1, x] for a positive exponent θ. Twisting the weight by (N i) ^ (-z) with Re z = 0 preserves that exponent, at the cost of the explicit factor 1 + ‖z‖ / θ.

TauCeti.norm_summatory_mul_cpow_le_of_summatory_le.{u_1} {ι : Type u_1} (N : ι → ℕ) [Northcott N]
  (hN : ∀ (i : ι), 1 ≤ ↑(N i)) (w : ι → ℂ) {C θ x : ℝ} (hx : 1 ≤ x) (hθ : 0 < θ) (z : ℂ)
  (hz : z.re = 0) (hC : ∀ t ∈ Set.Icc 1 x, ‖TauCeti.summatory N w t‖ ≤ C * t ^ θ) :
  ‖TauCeti.summatory N (fun i => w i * ↑(N i) ^ (-z)) x‖ ≤ C * (1 + ‖z‖ / θ) * x ^ θ

Lean

Formalized in Tau Ceti as TauCeti.norm_summatory_mul_cpow_le_of_summatory_le.

Sources

• Tau Ceti documentation: TauCeti.norm_summatory_mul_cpow_le_of_summatory_le
• Source of TauCeti.norm_summatory_mul_cpow_le_of_summatory_le in TauCeti/NumberTheory/ArithmeticDirichletSeries/AbelSummation.lean

LeanTauCeti.norm_summatory_mul_cpow_le_of_summatory_le

TheoremThe arithmetic Perron formula for ideal sums#

Where the L-series of the norm coefficients of f converges absolutely on the line Re s = c, the truncated Perron integral tends, as the height grows, to the ideal sum ∑_{N(I) ≤ x} f(I) in which each ideal of norm exactly x carries half weight. The two readings of this limit are TauCeti.perronFormula_of_forall_absNorm_ne and TauCeti.perronFormula_natCast.

TauCeti.perronFormula.{u_1} {K : Type u_1} [Field K] [NumberField K]
  {f : TauCeti.IdealArithmeticFunction K} {x c : ℝ} (hx : 0 < x) (hc : 0 < c)
  (h : LSeriesSummable ⇑((TauCeti.normCoeff K) f) ↑c) :
  Filter.Tendsto
    (fun T =>
      (↑(2 * Real.pi))⁻¹ *
        ∫ (t : ℝ) in -T..T,
          LSeries (⇑((TauCeti.normCoeff K) f)) (↑c + ↑t * Complex.I) *
            TauCeti.perronIntegrand x c t)
    Filter.atTop
    (nhds (∑ I ∈ TauCeti.idealsLE K x, f I * TauCeti.perronStep (x / ↑(Ideal.absNorm ↑I))))

Lean

Formalized in Tau Ceti as TauCeti.perronFormula.

Other forms

The arithmetic Perron formula at an integer endpoint. Formalized in Tau Ceti as TauCeti.tendsto_truncatedPerron_LSeries_natCast.

TauCeti.tendsto_truncatedPerron_LSeries_natCast {f : ℕ → ℂ} {c : ℝ} {N : ℕ} (hN : 0 < N)
  (hc : 0 < c) (h : LSeriesSummable f ↑c) :
  Filter.Tendsto
    (fun T =>
      (↑(2 * Real.pi))⁻¹ *
        ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * TauCeti.perronIntegrand (↑N) c t)
    Filter.atTop (nhds (∑ n ∈ Finset.Ico 1 N, f n + f N / 2))

Sources

• Tau Ceti documentation: TauCeti.perronFormula
• Source of TauCeti.perronFormula in TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Ideal.lean

LeanTauCeti.perronFormula · TauCeti.tendsto_truncatedPerron_LSeries_natCast

Uses 1 · Used by 1

Proof usesThe limiting arithmetic Perron formula

Used byThe Perron formula off the norms

TheoremThe limiting arithmetic Perron formula#

As the truncation height grows the integral tends to the series of sharp steps ∑' n, f n * perronStep (x / n). This holds at every positive x, integer endpoints included; TauCeti.tsum_mul_perronStep_natCast evaluates the limit there.

TauCeti.tendsto_truncatedPerron_LSeries {f : ℕ → ℂ} {x c : ℝ} (hx : 0 < x) (hc : 0 < c)
  (h : LSeriesSummable f ↑c) :
  Filter.Tendsto
    (fun T =>
      (↑(2 * Real.pi))⁻¹ *
        ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * TauCeti.perronIntegrand x c t)
    Filter.atTop (nhds (∑' (n : ℕ), f n * TauCeti.perronStep (x / ↑n)))

Lean

Formalized in Tau Ceti as TauCeti.tendsto_truncatedPerron_LSeries.

Sources

• Tau Ceti documentation: TauCeti.tendsto_truncatedPerron_LSeries
• Source of TauCeti.tendsto_truncatedPerron_LSeries in TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Formula.lean

LeanTauCeti.tendsto_truncatedPerron_LSeries

Uses 1 · Used by 1

Proof usesThe truncated Perron formula off the norms

Used byThe arithmetic Perron formula for ideal sums

TheoremThe off-norm arithmetic Perron formula#

When x is not a natural number at which f is nonzero, the truncated integral differs from the sharp partial sum ∑_{n < x} f n by at most the series of the smoothed-step kernel errors, a series that absolute convergence on the line makes summable.

TauCeti.norm_truncatedPerron_LSeries_sub_sum_le {f : ℕ → ℂ} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c)
  (hT : 0 < T) (hoff : ∀ (n : ℕ), f n ≠ 0 → x ≠ ↑n) (h : LSeriesSummable f ↑c) :
  ‖((↑(2 * Real.pi))⁻¹ *
          ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * TauCeti.perronIntegrand x c t) -
        ∑ n ∈ Finset.Ico 1 ⌈x⌉₊, f n‖ ≤
    ∑' (n : ℕ), ‖f n‖ * ((x / ↑n) ^ c / (Real.pi * T * |Real.log (x / ↑n)|))

Informally uses

• The truncated Perron formula off the norms

Lean

Formalized in Tau Ceti as TauCeti.norm_truncatedPerron_LSeries_sub_sum_le.

Sources

• Tau Ceti documentation: TauCeti.norm_truncatedPerron_LSeries_sub_sum_le
• Source of TauCeti.norm_truncatedPerron_LSeries_sub_sum_le in TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Formula.lean

LeanTauCeti.norm_truncatedPerron_LSeries_sub_sum_le

Used by 1

Used byThe truncated Perron formula off the norms

TheoremThe Perron formula off the norms#

If x > 0 is not the absolute norm of a nonzero ideal, the truncated Perron integral tends to the inclusive ideal sum ∑_{N(I) ≤ x} f(I).

TauCeti.perronFormula_of_forall_absNorm_ne.{u_1} {K : Type u_1} [Field K] [NumberField K]
  {f : TauCeti.IdealArithmeticFunction K} {x c : ℝ} (hx : 0 < x) (hc : 0 < c)
  (hoff :
    ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ↑(Ideal.absNorm ↑I) ≠ x)
  (h : LSeriesSummable ⇑((TauCeti.normCoeff K) f) ↑c) :
  Filter.Tendsto
    (fun T =>
      (↑(2 * Real.pi))⁻¹ *
        ∫ (t : ℝ) in -T..T,
          LSeries (⇑((TauCeti.normCoeff K) f)) (↑c + ↑t * Complex.I) *
            TauCeti.perronIntegrand x c t)
    Filter.atTop (nhds (TauCeti.idealSummatory K f x))

Lean

Formalized in Tau Ceti as TauCeti.perronFormula_of_forall_absNorm_ne.

Other forms

The Perron formula at an integer endpoint. Formalized in Tau Ceti as TauCeti.perronFormula_natCast.

TauCeti.perronFormula_natCast.{u_1} {K : Type u_1} [Field K] [NumberField K]
  {f : TauCeti.IdealArithmeticFunction K} {c : ℝ} {N : ℕ} (hN : 0 < N) (hc : 0 < c)
  (h : LSeriesSummable ⇑((TauCeti.normCoeff K) f) ↑c) :
  Filter.Tendsto
    (fun T =>
      (↑(2 * Real.pi))⁻¹ *
        ∫ (t : ℝ) in -T..T,
          LSeries (⇑((TauCeti.normCoeff K) f)) (↑c + ↑t * Complex.I) *
            TauCeti.perronIntegrand (↑N) c t)
    Filter.atTop (nhds (TauCeti.idealSummatory K f ↑N - ((TauCeti.normCoeff K) f) N / 2))

Sources

• Tau Ceti documentation: TauCeti.perronFormula_of_forall_absNorm_ne
• Source of TauCeti.perronFormula_of_forall_absNorm_ne in TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Ideal.lean

LeanTauCeti.perronFormula_of_forall_absNorm_ne · TauCeti.perronFormula_natCast

Uses 1

Proof usesThe arithmetic Perron formula for ideal sums

TheoremThe truncated Perron formula off the norms#

If x > 0 is not the absolute norm of a nonzero ideal, then at every positive height T the truncated Perron integral differs from the inclusive ideal sum ∑_{N(I) ≤ x} f(I) by at most the series of the smoothed-step kernel errors at the ratios x / n.

TauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le.{u_1} {K : Type u_1} [Field K]
  [NumberField K] {f : TauCeti.IdealArithmeticFunction K} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c)
  (hT : 0 < T)
  (hoff :
    ∀ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ↑(Ideal.absNorm ↑I) ≠ x)
  (h : LSeriesSummable ⇑((TauCeti.normCoeff K) f) ↑c) :
  ‖((↑(2 * Real.pi))⁻¹ *
          ∫ (t : ℝ) in -T..T,
            LSeries (⇑((TauCeti.normCoeff K) f)) (↑c + ↑t * Complex.I) *
              TauCeti.perronIntegrand x c t) -
        TauCeti.idealSummatory K f x‖ ≤
    ∑' (n : ℕ), ‖((TauCeti.normCoeff K) f) n‖ * ((x / ↑n) ^ c / (Real.pi * T * |Real.log (x / ↑n)|))

Lean

Formalized in Tau Ceti as TauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le.

Other forms

The truncated Perron formula for an L-series. Formalized in Tau Ceti as TauCeti.truncatedPerron_LSeries.

TauCeti.truncatedPerron_LSeries {f : ℕ → ℂ} {x c T : ℝ} (hx : 0 < x) (hc : 0 < c) (hT : 0 ≤ T)
  (h : LSeriesSummable f ↑c) :
  (↑(2 * Real.pi))⁻¹ *
      ∫ (t : ℝ) in -T..T, LSeries f (↑c + ↑t * Complex.I) * TauCeti.perronIntegrand x c t =
    ∑' (n : ℕ), f n * TauCeti.truncatedPerronKernel (x / ↑n) c T

Sources

• Tau Ceti documentation: TauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le
• Source of TauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le in TauCeti/NumberTheory/ArithmeticDirichletSeries/Perron/Ideal.lean

LeanTauCeti.norm_truncatedPerron_LSeries_normCoeff_sub_idealSummatory_le · TauCeti.truncatedPerron_LSeries

Uses 1 · Used by 1

Proof usesThe off-norm arithmetic Perron formula

Used byThe limiting arithmetic Perron formula

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.