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 241 to 260 of 1,644 declarations.
theorem
CH2.varphi_fourier_ident
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3027
lemma
CH2.RectangleIntegral_tendsTo_UpperU'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3073
lemma
CH2.tendsto_contour_shift
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3092
lemma
Complex.norm_le_abs_im_add_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3147
lemma
CH2.phi_sum_norm_le_of_component_bounds
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3160
theorem
CH2.phi_sum_norm_le_linear_halfplane
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3179
theorem
CH2.phi_bound_upwards
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3201
theorem
CH2.phi_bound_downwards
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3209
theorem
CH2.phi_fourier_ray_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3229
lemma
CH2.integrableOn_Phi_circ_m12
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3266
lemma
CH2.integrableOn_Phi_star_m12
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3278
lemma
CH2.integrableOn_Phi_circ_p12
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3290
lemma
CH2.integrableOn_Phi_star_p12
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3302
theorem
CH2.integrable_phi_fourier_ray
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3315
lemma
CH2.tendsto_T_plus_one_mul_exp_atTop_nhds_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3370
lemma
CH2.horizontal_integral_phi_fourier_vanish
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3398
theorem
CH2.shift_upwards
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3443
theorem
CH2.B_affine_periodic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3588
theorem
CH2.phi_star_affine_periodic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3611
theorem
CH2.shift_upwards_phi_diff
At a point z = -1 + i t on the vertical line Re z = -1 (with t ≥ 0), the combination
Φ_circ - Φ_star equals -Φ_star evaluated on the imaginary axis at i t.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3665
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.