Laplace transform of every actual zero occurrence
Abstract
Laplace transform of every actual zero occurrence
The coefficient is 1/(rho*(1-rho)) at each actual analytic multiplicity occurrence, with both imaginary signs. The existing normalized xi resolvent supplies the exact mass, conjugation supplies reality, and absolute coefficient bounds pay the integral exchange. No symmetry, mass, transform or RH assumption is added. These analytic suppliers are consumed by the complete integrated explicit formula.
Theorem 1.1 (actual complete H package).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_complete_H_package
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_complete_H_package (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.2 (actualCoeff hasSum).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualCoeff_hasSum
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualCoeff_hasSum (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.3 (actualH summable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_summable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_summable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.4 (actualH bound).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_bound
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.5 (actualH continuous).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_continuous
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_continuous (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.6 (xiReading ne zero right).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xiReading_ne_zero_right
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xiReading_ne_zero_right (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.7 (actual normalized resolvent).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_normalized_resolvent
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_normalized_resolvent (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.8 (actual resolvent hasSum).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_resolvent_hasSum
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_resolvent_hasSum (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.9 (actualH laplace integrable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace_integrable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace_integrable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.10 (actualH laplace).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.11 (xi logDeriv right).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xi_logDeriv_right
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xi_logDeriv_right (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
References
- Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualCoeff_hasSum - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_bound - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_continuous - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_laplace_integrable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actualH_summable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_complete_H_package - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_normalized_resolvent - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.actual_resolvent_hasSum - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xiReading_ne_zero_right - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/ActualZeroLaplace.xi_logDeriv_right - Dependency: D5/S3/Weil/ZeroData/ActualReciprocalSquareBounds