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 961 to 980 of 1,644 declarations.
lemma
norm_tail_quotient_le
The fixed-window tail quotient is bounded by an integrable translate.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:673
theorem
integrable_tail_quotient_of_integrable
The fixed-window tail quotient is integrable for every integrable source.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:705
lemma
tail_indicator_sin_div_eq_sin_smul_quotient
Pointwise tail algebra for the sine kernel.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:731
theorem
tendsto_sin_div_kernel_tail_of_integrable
The fixed-window tail of the sine kernel tends to zero for integrable sources.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:758
theorem
norm_sin_div_kernel_tail_le_integral_norm
Uniform fixed-window tail bound for the sine kernel. Outside (-R, R],
the denominator gives a 1 / (π R) bound, independent of the height and
translation.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:807
theorem
intervalIntegral_sin_div_kernel_split
Finite symmetric-window split for the sin (T * u) / (π * u) kernel.
This is the valid algebraic surface for the principal-value mass term before
taking an improper limit.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:896
theorem
intervalIntegral_sin_div_kernel_scalar_mass_eq_scaled
Scaling reduces the finite-window mass of sin (T * u) / (π * u) to the
normalized symmetric sine integral at height T * R.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:967
theorem
intervalIntegrable_sin_div_kernel
The sine-over-argument kernel is interval-integrable on finite intervals;
the value at zero is irrelevant by the removable singularity of Real.sinc.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1003
theorem
intervalIntegrable_scaled_sin_div_kernel
The scaled sine kernel is interval-integrable on finite intervals; its value at zero is again irrelevant.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1018
theorem
norm_fourierInvTrunc_le_of_windowed_sin_div_bounds
Windowed bound for finite-height Fourier inversion. The mass term, local principal-value window, and far-field tail are separated so applications can supply uniform bounds for the first two and use the built-in tail estimate.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1053
theorem
intervalIntegral_sin_div_kernel_neg_zero_eq_zero_to
The negative half of the finite sine integral equals the positive half.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1115
theorem
intervalIntegral_sin_div_kernel_symmetric_eq_two_mul_zero_to
The symmetric finite sine integral is twice its positive half.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1132
theorem
tendsto_intervalIntegral_sin_div_kernel_scalar_mass_of_dirichlet
A normalized symmetric Dirichlet integral limit gives the scalar finite-window mass at every positive radius.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1174
theorem
intervalIntegral_sinc_tail_eq_ibp
Integration by parts for the positive sinc tail on a finite interval.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1278
theorem
intervalIntegral_inv_sq_of_pos
The finite inverse-square integral on a positive interval.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1323
theorem
norm_intervalIntegral_sinc_tail_le
Uniform finite-tail control for the one-sided sinc integral.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1343
theorem
cauchySeq_intervalIntegral_real_sinc_atTop
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1404
theorem
intervalIntegral_exp_neg_mul_const_mul_self
Exact integral of the derivative of -exp (-a * x) on a finite interval.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1471
theorem
norm_intervalIntegral_exp_neg_mul_sinc_tail_le
Uniform finite-tail control for the damped one-sided sinc integral.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1489
theorem
integral_Ioi_exp_neg_mul_sin
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1706
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.