L Series

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

TheoremThe Chebyshev bound#

Nonnegative coefficients whose Dirichlet series is summable on Re s > 1 and has a boundary remainder G = LSeries a - A / (s - 1) continuous on Re s ≥ 1 satisfy ∑_{1 ≤ n ≤ t} ‖a n‖ = O(t).

TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary {a : ℕ → ℂ} {A : ℂ} {G : ℂ → ℂ} (ha : 0 ≤ a)
  (hG : ContinuousOn G {z | 1 ≤ z.re}) (hG' : ∀ (z : ℂ), 1 < z.re → G z = LSeries a z - A / (z - 1))
  (hsum : ∀ (sigma : ℝ), 1 < sigma → LSeriesSummable a ↑sigma) :
  (fun t => ∑ n ∈ Finset.Icc 1 ⌊t⌋₊, ‖a n‖) =O[Filter.atTop] fun t => t

Lean

Formalized in Tau Ceti as TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary.

Sources

• Tau Ceti documentation: TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary
• Source of TauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary in TauCeti/NumberTheory/LSeries/WienerIkehara/Chebyshev.lean

LeanTauCeti.LSeries.isBigO_sum_Icc_norm_id_of_boundary

Uses 1 · Used by 1

Proof usesRiemann--Lebesgue on a vertical line

Used byThe Wiener--Ikehara theorem

TheoremLandau's theorem#

If a has nonnegative values and its abscissa of absolute convergence is the real number σ, then LSeries a has no analytic continuation across σ.

TauCeti.LSeries.landau {a : ℕ → ℂ} (ha : 0 ≤ a) {σ : ℝ} (habs : LSeries.abscissaOfAbsConv a = ↑σ) :
  ¬TauCeti.LSeries.HasAnalyticExtensionAt a σ

Lean

Formalized in Tau Ceti as TauCeti.LSeries.landau.

Other forms

Landau's theorem at the abscissa of ordinary convergence. Formalized in Tau Ceti as TauCeti.LSeries.landau_of_abscissaOfConv.

TauCeti.LSeries.landau_of_abscissaOfConv {a : ℕ → ℂ} (ha : ∀ (n : ℕ), n ≠ 0 → 0 ≤ a n) {σ : ℝ}
  (hconv : TauCeti.LSeries.abscissaOfConv a = ↑σ) : ¬TauCeti.LSeries.HasAnalyticExtensionAt a σ

Landau's theorem, half-plane form. Formalized in Tau Ceti as TauCeti.LSeries.abscissaOfAbsConv_le_of_differentiableOn.

TauCeti.LSeries.abscissaOfAbsConv_le_of_differentiableOn {a : ℕ → ℂ} (ha : 0 ≤ a)
  (hfin : LSeries.abscissaOfAbsConv a ≠ ⊤) {σ₁ : ℝ} {F : ℂ → ℂ}
  (hF : DifferentiableOn ℂ F {s | σ₁ < s.re})
  (hFeq : ∀ (s : ℂ), σ₁ < s.re → LSeries.abscissaOfAbsConv a < ↑s.re → F s = LSeries a s) :
  LSeries.abscissaOfAbsConv a ≤ ↑σ₁

Sources

• Tau Ceti documentation: TauCeti.LSeries.landau
• Source of TauCeti.LSeries.landau in TauCeti/NumberTheory/LSeries/Landau.lean

LeanTauCeti.LSeries.landau · TauCeti.LSeries.landau_of_abscissaOfConv · TauCeti.LSeries.abscissaOfAbsConv_le_of_differentiableOn

Used by 1

Used byMeromorphic form of Landau's theorem

TheoremMeromorphic form of Landau's theorem#

Let F be a meromorphic continuation of a Dirichlet series with nonnegative coefficients to a neighborhood of its finite, actual abscissa of absolute convergence. Then the meromorphic order of F at that abscissa is negative. In particular, the singularity forced by landau is a pole, not a removable singularity.

Meromorphicity and meromorphic order depend only on the punctured germ, so no convention is imposed on the value of F at the centre.

TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries {a : ℕ → ℂ} (ha : 0 ≤ a) {σ r : ℝ}
  (habs : LSeries.abscissaOfAbsConv a = ↑σ) (hr : 0 < r) {F : ℂ → ℂ} (hF : MeromorphicAt F ↑σ)
  (hFeq : ∀ s ∈ Metric.ball (↑σ) r, σ < s.re → F s = LSeries a s) : meromorphicOrderAt F ↑σ < 0

Lean

Formalized in Tau Ceti as TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries.

Sources

• Tau Ceti documentation: TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries
• Source of TauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries in TauCeti/NumberTheory/LSeries/Landau.lean

LeanTauCeti.LSeries.meromorphicOrderAt_lt_zero_of_eq_LSeries

Uses 1

Proof usesLandau's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.