Problems / erdos-1094 / erdos-1094--h3--h3--h1--h1--h1--h1
Wiener–Ikehara Tauberian theorem
erdos-1094--h3--h3--h1--h1--h1--h1
open
Hole h_wi of erdos-1094--h3--h3--h1--h1--h1 (split by 20261018T200210Z-t1018-e-partial.lean).
$$f\ge0$, $\sum f(n)n^{-s}$ converges for $\Re s>1$ and $F(s)-A/(s-1)$ extends continuously to $\Re s\ge1$ $\Rightarrow$ $\frac1N\sum_{n<N}f(n)\to A$$
Wiener (1932), Ikehara (1931); continuous-boundary form: Korevaar, Bull. AMS 39 (2002), Thm 4.2 / Tauberian Theory (2004) III.4.
Lean
theorem erdos_1094__h3__h3__h1__h1__h1__h1 : ∀ (f : ℕ → ℝ) (A : ℝ),
(∀ (n : ℕ), (0 : ℝ) ≤ f n) →
(∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) →
(∃ (G : ℂ → ℂ),
ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧
∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) →
Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A) := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Open. A direct proof closes it.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
import Nodes.«erdos-1094--h3--h3--h1--h1--h1--h1».Context
open scoped Nat
/-! Hole `h_wi` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_1094__h3__h3__h1__h1__h1__h1 : ∀ (f : ℕ → ℝ) (A : ℝ),
(∀ (n : ℕ), (0 : ℝ) ≤ f n) →
(∀ (s : ℂ), (1 : ℝ) < s.re → LSeriesSummable (fun (n : ℕ) => (↑(f n) : ℂ)) s) →
(∃ (G : ℂ → ℂ),
ContinuousOn G {s : ℂ | (1 : ℝ) ≤ s.re} ∧
∀ (s : ℂ), (1 : ℝ) < s.re → G s = LSeries (fun (n : ℕ) => (↑(f n) : ℂ)) s - (↑A : ℂ) / (s - (1 : ℂ))) →
Filter.Tendsto (fun (N : ℕ) => (∑ n ∈ Finset.range N, f n) / (↑N : ℝ)) Filter.atTop (nhds A) := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by t1018-e, drafted with claude-opus-5-5, 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$$f\ge0$, $\sum f(n)n^{-s}$ converges for $\Re s>1$ and $F(s)-A/(s-1)$ extends continuously to $\Re s\ge1$ $\Rightarrow$ $\frac1N\sum_{n<N}f(n)\to A$$
Wiener (1932), Ikehara (1931); continuous-boundary form: Korevaar, Bull. AMS 39 (2002), Thm 4.2 / Tauberian Theory (2004) III.4.
Rendered from gloss/43a1a97a1858….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h3--h1--h1--h1--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
c51a63716ae9.import Mathlib
open scoped Nat
theorem witness : ∃ (f : ℕ → ℝ) (A : ℝ), (∀ n, 0 ≤ f n) ∧
(∀ s : ℂ, 1 < s.re → LSeriesSummable (fun n => (f n : ℂ)) s) ∧
(∃ G : ℂ → ℂ, ContinuousOn G {s | 1 ≤ s.re} ∧
∀ s : ℂ, 1 < s.re → G s = LSeries (fun n => (f n : ℂ)) s - A / (s - 1)) :=
⟨fun _ => 0, 0, fun _ => le_rfl, fun s _ => by simp only [Complex.ofReal_zero]; exact LSeriesSummable_zero,
⟨fun _ => 0, continuousOn_const, fun s _ => by simp only [Complex.ofReal_zero, zero_div, sub_zero]; exact (congrFun LSeries_zero s).symm⟩⟩No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).