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 121 to 140 of 1,644 declarations.
theorem
BKLNW_app.bklnw_eq_A_13
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:182
theorem
BKLNW_app.bklnw_thm_15
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:254
theorem
BKLNW_app.bklnw_lemma_15
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:541
theorem
BKLNW_app.bklnw_cor_15_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:628
lemma
BKLNW_app.continuous_besselI0
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:833
lemma
BKLNW_app.η_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:861
lemma
BKLNW_app.integrable_η
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:879
lemma
BKLNW_app.μ_antitoneOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:911
lemma
BKLNW_app.integrable_μ
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1009
lemma
BKLNW_app.ν_abs_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1027
lemma
BKLNW_app.besselI0_sub_partial_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1045
theorem
BKLNW_app.bklnw_cor_15_1'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app.lean:1185
lemma
BKLNW_app.table_8_ε_le_of_row
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_app_tables.lean:756
theorem
BKLNW.table_10_next_cert_24000
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_next · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_next.lean:2298
lemma
BKLNW.table_10_next_eq_of_adjacent
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:66
lemma
BKLNW.table_10_next_get
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:78
lemma
BKLNW.expTd_hasDerivAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:116
lemma
BKLNW.Gp'_hasDerivAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:143
lemma
BKLNW.Gp''_nonneg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:155
lemma
BKLNW.Gp_convexOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_table10_rows_core · PrimeNumberTheoremAnd/IEANTN/BKLNW/BKLNW_table10_rows_core.lean:174
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.