Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unconditional integrated explicit formula

Abstract

Unconditional integrated explicit formula

For every real y>0, the complete actual zero occurrence series equals U(exp(y))-log(2pi) plus the full trivial zero correction. The residual is literally zero on y<=0 and damped by exp(-2y) on y>0. Its L1 Fourier transform vanishes at nonzero frequencies by the actual Laplace suppliers. Continuity of that transform gives frequency zero without applying the digamma series at integer one. Pointwise inversion uses continuity only at the requested positive y. This formula makes no RH, Robin positivity or positive U peak claim. Integer 5040, all integer endpoints N>=2, every prime-power endpoint and the literal exponential-over-denominator form are checked only by transient anonymous applications.

Theorem 1.1 (explicitDiscrepancy line integrable).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitDiscrepancy_line_integrable

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitDiscrepancy_line_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.2 (explicitDiscrepancy line zero).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitDiscrepancy_line_zero

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitDiscrepancy_line_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.3 (explicitFourierResidual integrable).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_integrable

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_integrable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.4 (explicitFourierResidual continuousAt).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_continuousAt

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_continuousAt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.5 (explicitFourierResidual fourier).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_fourier

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_fourier (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.6 (explicitFourierResidual fourier zero).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_fourier_zero

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.explicitFourierResidual_fourier_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

Theorem 1.7 (actual integrated explicit formula).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.actual_integrated_explicit_formula

Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/WholeFormula.actual_integrated_explicit_formula (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.

References