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 281 to 300 of 1,644 declarations.
lemma
CH2.Inu_bounds_pos
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5133
lemma
CH2.Inu_bounds_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5165
theorem
CH2.varphi_deriv_integ
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5214
lemma
CH2.varphi_ftc_out
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5255
lemma
CH2.varphi_ftc
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5290
theorem
CH2.varphi_abs
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5332
lemma
CH2.ϕ_pm_deriv_Iic_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5368
lemma
CH2.ϕ_pm_deriv_Ici_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5424
theorem
CH2.varphi_deriv_tv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5580
theorem
CH2.varphi_fourier_decay
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5615
theorem
CH2.varphi_fourier_minus_error
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5672
theorem
CH2.varphi_fourier_plus_error
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5712
lemma
CH2.deriv_z_coth_z_bound_boundary
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5852
theorem
CH2.CH2_lemma_4_2a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:6235
theorem
CH2.CH2_lemma_4_2b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:6425
theorem
Chebyshev.T.le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:32
theorem
Chebyshev.T.ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:71
theorem
Chebyshev.T.weighted_eq_sum
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:126
theorem
Chebyshev.E_nu_eq_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:211
theorem
Chebyshev.E_nu_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Chebyshev · PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean:245
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.