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 221 to 240 of 1,644 declarations.
theorem
CH2.Phi_cancel
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:1923
lemma
CH2.h_comp
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2001
theorem
CH2.Phi_star.contDiff_real
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2009
theorem
CH2.Phi_circ.contDiff_real
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2020
theorem
CH2.Phi_star.continuousAt_imag
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2042
lemma
CH2.sinh_ne_zero_of_not_pole
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2072
theorem
CH2.Phi_circ.analyticAt_of_not_pole
Phi_circ is analytic whenever we are away from the poles.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2096
theorem
CH2.Phi_star.analyticAt_of_not_pole_nz
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2137
theorem
CH2.ϕ_c2_left
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2195
theorem
CH2.ϕ_c2_right
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2221
theorem
CH2.ϕ_continuous
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2257
theorem
CH2.ϕ_pm_zero_boundary
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2332
theorem
CH2.ϕ_circ_bound_right
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2349
theorem
CH2.ϕ_circ_bound_left
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2419
theorem
CH2.ϕ_star_bound_right
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2474
theorem
CH2.ϕ_star_bound_left
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2541
theorem
CH2.B_plus_mono
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2617
theorem
CH2.B_minus_mono
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2699
theorem
CH2.norm_Phi_star_I_mul_le
On the upward imaginary axis, Phi_star is bounded by the height.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2922
theorem
CH2.norm_Phi_star_neg_I_mul_le
On the downward imaginary axis, Phi_star is bounded by the height.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:2950
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.