Head version
a93551347dce
a93551347dce924b1db75d40218841bf085a465f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 22 Jul 2026
- Dependencies
- 13
- Versions
- 9
All packages
AlexKontorovich/PrimeNumberTheoremAnd
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
Therefore indexed 1,644 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
External build observation
Exact head commit and toolchain
No Reservoir build observation was found for this exact commit and toolchain. This is not evidence of failure.
Pin this source in lakefile.lean
require PrimeNumberTheoremAnd from git "https://github.com/AlexKontorovich/PrimeNumberTheoremAnd.git" @ "a93551347dce924b1db75d40218841bf085a465f"
Source declarations
1,644 indexed proofs
Showing 601 to 620 of 1,644 declarations.
lemma
Kadiri.kadiri_laplace_shifted_vertical_segment_continuousOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:136
lemma
Kadiri.kadiri_laplace_line_weight_differentiable
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:163
lemma
Kadiri.kadiri_laplace_line_local_quotient_integrable
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:173
lemma
Kadiri.kadiri_laplace_positive_line_pv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:320
theorem
Kadiri.kadiri_thm_3_1_q1_eq_13_core
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:418
lemma
Kadiri.kadiri_laplace_positive_vertical_segment_continuousOn
Continuity of the bilateral Laplace integral on the positive vertical line
re s = a, obtained by reflecting the shifted contour statement.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:105
lemma
Kadiri.kadiri_thm_3_1_q1_I_2_eq_reflected_interval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:280
lemma
Kadiri.kadiri_thm_3_1_q1_eq_14_of_uniform_laplace_trunc_cpow_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:527
lemma
Kadiri.kadiri_thm_3_1_q1_eq_14_of_uniform_fourier_inv_trunc_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:570
lemma
Kadiri.kadiri_thm_3_1_q1_eq_14_of_windowed_fourier_source_bounds
Kadiri-side bridge from windowed Fourier bounds to equation (14). It leaves
only a source bound and a local principal-value window bound as application
inputs; the mass and far-field tail are handled by LaplaceInversion.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:618
theorem
Kadiri.kadiri_thm_3_1_q1_eq_14_core
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriEq14 · PrimeNumberTheoremAnd/IEANTN/KadiriEq14.lean:757
lemma
Kadiri.kadiri_laplace_neg_line_weight_norm_eq
Norm shape of the weighted source: peeling off the exp (x/2) factor.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:68
lemma
Kadiri.kadiri_laplace_neg_line_weight_isBigO_atBot
On atBot, the weighted source is O(exp ((b - σ) x)); no constraint on σ.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:87
lemma
Kadiri.kadiri_laplace_neg_line_weight_isBigO_atTop
On atTop, the weighted source is O(exp (-(1 + b + σ) x)); no constraint on σ.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:114
lemma
Kadiri.kadiri_laplace_neg_line_weight_bounded_of_continuous
Global boundedness of the weighted source for -(1+b) < σ < b.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:141
lemma
Kadiri.kadiri_laplace_neg_line_weight_integrable_of_continuous
Integrability of the weighted source for -(1+b) < σ < b: the σ ↦ -σ instance of
kadiri_laplace_full_strip_weight_integrable_of_continuous.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:158
lemma
Kadiri.kadiri_laplace_neg_line_weight_deriv_bounded
Global bound for the derivative of the weighted source for -(1+b) < σ < b.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:185
lemma
Kadiri.kadiri_laplace_exp_hasDerivAt_zero
Derivative of the two-sided Laplace transform at 0: the s0 = 0 instance of the
full-strip derivative formula.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:256
theorem
Kadiri.sin_div_error_pointwise_bound_of_convex
Convex-set version of sin_div_error_pointwise_bound: the mean-value estimate only
needs differentiability and the derivative bound on a convex set containing both
points.
PrimeNumberTheoremAnd.IEANTN.KadiriSupport · PrimeNumberTheoremAnd/IEANTN/KadiriSupport.lean:304
lemma
Kadiri.riemannZeta_eventually_ne_zero_punctured_nontrivialZero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:65
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.