Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-04
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The completed zeta function has its Mellin-theta integral representation on Res>1

Statement

If Res>1, then

πs/2Γ(s/2)ζ(s)=120(θ(t)1)ts/21dt.

Facts & Assumptions

Given: A complex number s with Res>1.

[L1]

On Res>1, ζ(s)=n1ns (The Riemann zeta function on the half-plane Res>1).

[L2]

For t>0, θ(t)1=2n1eπn2t (The Jacobi theta function θ(t)=nZeπn2t for t>0).

[L3]

On Rez>0, Γ(z)=0euuz1du (Euler's Gamma function on the right half-plane).

[L4]

Tonelli's theorem permits swapping a nonnegative sum and integral on a sigma-finite product (Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

Proof

technique · direct
1.1

Write σ:=Res. By [L2], 120(θ(t)1)ts/21dt=n10eπn2tts/21dt, provided the interchange is justified. Since ts/21=tσ/21 and σ>1, the summands are absolutely integrable and nonnegative after taking absolute values, so [L4] applies to the absolute-value kernel.

givenL2L4algebra
1.2

For each n1, substitute u=πn2t. Then 0eπn2tts/21dt=πs/2ns0euus/21du=πs/2Γ(s/2)ns by [L3].

L3algebra
2.1

Summing the identity of step 1.2 over n and using [L1] yields 120(θ(t)1)ts/21dt=πs/2Γ(s/2)n1ns=πs/2Γ(s/2)ζ(s). This is the claimed Mellin representation.

step 1.1step 1.2L1algebra

Depends on

Used by

Dependency tree · two levels

11 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources