Inclusive Mangoldt ramps and complete Mertens transform
Abstract
Inclusive Mangoldt ramps and complete Mertens transform
The function U is the existing CompleteMertensPeak.U, with inclusive Chebyshev psi and the actual Euler constant. The locally finite positive-part ramp is zero when an integer term enters, so continuity includes every prime-power endpoint. Positive Tonelli and the complete Mangoldt LSeries at two pay the infinite arithmetic exchange before the complex integral is evaluated. The Fourier line is s=2+2pii*t.
Theorem 1.1 (mangoldtRamp nonneg).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_nonneg
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_nonneg (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.2 (mangoldtRamp continuous).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_continuous
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_continuous (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.3 (mangoldtRamp at entry).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_at_entry
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_at_entry (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.4 (mangoldtPart summable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_summable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_summable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.5 (U eq complete ramps).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_eq_complete_ramps
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_eq_complete_ramps (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.6 (Exact finite arithmetic localization).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_eq_range
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_eq_range (✓ std3). ∎
Source. Repository-derived.
Commentary.
For real t>=0 and natural N with t<N, mangoldtPart(t) is exactly the sum of mangoldtRamp(n,t) over n<N. The ActualKernelPrefixPerturbation proof applies this identity only on its fixed compact window. Each ramp vanishes at entry, and the terms at zero and one vanish. No global arithmetic truncation is asserted.
Theorem 1.7 (U continuousAt pos).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_continuousAt_pos
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_continuousAt_pos (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.8 (U exp continuous).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_exp_continuous
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_exp_continuous (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.9 (complete mangoldt endpoint).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.complete_mangoldt_endpoint
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.complete_mangoldt_endpoint (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.10 (transformLine re).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.transformLine_re
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.transformLine_re (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.11 (mangoldtRamp laplace).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.12 (mangoldtRamp laplace integrable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_integrable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_integrable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.13 (mangoldtRamp laplace norm).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_norm
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_norm (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.14 (mangoldtRamp norm integrals summable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_norm_integrals_summable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_norm_integrals_summable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.15 (mangoldtPart line integrable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_integrable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_integrable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.16 (mangoldtPart line laplace).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_laplace
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_laplace (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.17 (first exp moment).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.first_exp_moment
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.first_exp_moment (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.18 (U line integrable).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_integrable
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_integrable (✓ std3). ∎
Source. Repository-derived.
Commentary.
The exact hypotheses, occurrence indices and endpoint quantifiers are given by the Lean declaration.
Theorem 1.19 (U line laplace).
Lean statement: D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_laplace
Proof. Machine-checked in Lean as D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_laplace (✓ 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/CompleteMangoldtLaplace.U_continuousAt_pos - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_eq_complete_ramps - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_exp_continuous - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_integrable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.U_line_laplace - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.complete_mangoldt_endpoint - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.first_exp_moment - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_eq_range - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_integrable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_line_laplace - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtPart_summable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_at_entry - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_continuous - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_integrable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_laplace_norm - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_nonneg - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.mangoldtRamp_norm_integrals_summable - Truth anchor:
D5/S3/Weil/Mertens/IntegratedExplicit/CompleteMangoldtLaplace.transformLine_re - Dependency: D5/S3/Arith/Robin/CompleteMertensPeak
- Dependency: D5/S3/Weil/Mertens/IntegratedExplicit/TrivialZeroLaplace