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 341 to 360 of 1,644 declarations.
lemma
Erdos392.Params.initial.sum_valuation_le
The sum of valuations in the initial factorization is bounded by M times the sum of
valuations in the interval. This is because the initial factorization is a subset of M copies
of the interval.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1335
theorem
Erdos392.Params.initial.balance_small_prime_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1355
lemma
Erdos392.Params.initial.smooth_of_dvd_small_prime
If p is a small prime (L < p ≤ √n) and m is in the
initial interval and divisible by p,
then m is (n/L)-smooth.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1428
lemma
Erdos392.Params.initial.sum_valuation_eq_small
For a small prime p, the sum of p-adic valuations in the initial factorization equals M
times the sum over k of the count of multiples of p^k in the interval.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1455
lemma
Erdos392.Params.initial.balance_ge_neg_M_mul_log
The balance of a small prime p is at least -M * floor(log_p n).
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1514
theorem
Erdos392.Params.initial.balance_small_prime_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1529
lemma
Erdos392.Params.initial_full_sum_valuation_eq
The sum of valuations in [n - n/M, n) equals
∑ k ∈ [1, log_p n], #{m ∈ I | p^k ∣ m}.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1602
lemma
Erdos392.Params.initial_full_balance_ge
The balance of initial_full is at least -M · log n / log 2.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1625
lemma
Erdos392.Params.initial_balance_eq
The balance of initial equals that of initial_full minus M times the sum of valuations
in rough_set.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1658
lemma
Erdos392.Params.valuation_eq_one_of_large_prime
If a prime q ≥ n / L divides m < n, then its valuation in m is 1.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1697
lemma
Erdos392.Params.rough_set_structure
Any m in the rough set can be written as q * k where q is a prime ≥ n / L and
k ≤ L, with m.factorization q = 1.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1709
lemma
Erdos392.Params.rough_set_card_le
The cardinality of rough_set is at most π(n) * L.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1748
lemma
Erdos392.Params.rough_valuation_eq_k_valuation
For m ∈ rough_set and p ≤ L, vₚ(m) = vₚ(k).
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1777
lemma
Erdos392.Params.rough_valuation_le_log
For m ∈ rough_set and p ≤ L, vₚ(m) ≤ logₚ L.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1798
lemma
Erdos392.Params.primeCounting_ge_log
π(n) ≥ log n for n ≥ 2.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1826
theorem
Erdos392.Params.initial.balance_tiny_prime_ge
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:1898
theorem
Erdos392.Params.initial.bound_score_1
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2364
theorem
Erdos392.Params.initial.bound_score_2
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2403
theorem
Erdos392.Params.initial.bound_score_3
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2494
lemma
Erdos392.prod_one_sub_one_div_prime_tendsto_zero
The product ∏ p ≤ n, (1 - 1/p) over primes tends to zero as n → ∞.
PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:2581
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.