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 361 to 380 of 1,644 declarations.
lemma
Erdos392.exists_phi_div_self_lt
For any ε > 0, there exists a ≠ 0 with φ(a)/a < ε.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2610
lemma
Erdos392.primeCounting_is_o_id
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2626
lemma
Erdos392.large_prime_sum_split
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2676
lemma
Erdos392.boundary_term_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2689
theorem
Erdos392.Params.initial.bound_score_4
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2729
lemma
Erdos392.primeCounting_le_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2788
lemma
Erdos392.tendsto_primeCounting_div_id_zero
The ratio π(n) / n → 0 as n → ∞.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2851
theorem
Erdos392.Params.initial.bound_score_5
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2871
theorem
Erdos392.Params.initial.score
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2914
theorem
Erdos392.Solution_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3008
lemma
Erdos392.pairProd_bound
If all elements of l are at most n, then all elements of pairProd l are at most n².
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3106
theorem
Erdos392.Solution_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:3124
theorem
FKS2.lemma_10_substep
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:48
theorem
FKS2.lemma_10_substep_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:78
theorem
FKS2.lemma_10a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:99
theorem
FKS2.lemma_10b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:121
theorem
FKS2.lemma_10c
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:157
lemma
FKS2.deriv_dawson
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:221
lemma
FKS2.filter_tendsto_dawson_at_top_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:251
lemma
FKS2.dawson_eq_integral
Substituted form: dawson z = ∫₀^z exp (u² − 2zu) du.
PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:306
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.