Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Complete trivial zero correction

Abstract

Complete trivial zero correction

The natural index n represents j=n+1. The full coefficient series has mass 1-log(2), and uniform absolute bounds give continuity on the nonnegative half-axis. Damping pays the complete Laplace exchange for Re(s)>0. No finite truncation replaces the correction. The digamma series at one half is within its integer-complement domain.

Theorem 1.1 (trivialCoeff nonneg).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialCoeff_nonneg

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

Source. Repository-derived.

Commentary.

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

Theorem 1.2 (trivialCoeff hasSum).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialCoeff_hasSum

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

Source. Repository-derived.

Commentary.

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

Theorem 1.3 (trivialT summable).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_summable

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

Source. Repository-derived.

Commentary.

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

Theorem 1.4 (trivialT nonneg).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_nonneg

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

Source. Repository-derived.

Commentary.

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

Theorem 1.5 (trivialT le mass).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_le_mass

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

Source. Repository-derived.

Commentary.

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

Theorem 1.6 (trivialT continuousOn).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_continuousOn

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

Source. Repository-derived.

Commentary.

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

Theorem 1.7 (trivialT continuousAt).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_continuousAt

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

Source. Repository-derived.

Commentary.

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

Theorem 1.8 (trivialT laplace integrable).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_laplace_integrable

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

Source. Repository-derived.

Commentary.

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

Theorem 1.9 (trivialT laplace hasSum).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivialT_laplace_hasSum

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

Source. Repository-derived.

Commentary.

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

Theorem 1.10 (trivial partial fraction).

Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace.trivial_partial_fraction

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

Source. Repository-derived.

Commentary.

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

References