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 181 to 200 of 1,644 declarations.
theorem
CH2.lemma_5_1_c
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2125
lemma
CH2.conj_intVSeg_of_antisymm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2178
lemma
CH2.conj_intHSeg_of_antisymm
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2196
theorem
CH2.lemma_5_1_d
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2212
theorem
CH2.lemma_5_1_e
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2407
theorem
CH2.lemma_5_1_g
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2534
theorem
CH2.lemma_5_1_h
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:2575
theorem
CH2.norm_Phi_lambda_one_add_I_mul_le_of_pos
For positive λ, Phi_lambda on 1 + i y is bounded by y.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3294
theorem
CH2.norm_Phi_lambda_neg_one_add_I_mul_le_of_pos
For positive λ, Phi_lambda on -1 + i y is bounded by y.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3307
theorem
CH2.norm_Phi_lambda_one_add_I_mul_le_of_neg
For negative λ, Phi_lambda on 1 + i y is bounded by y away from the downward pole.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3326
theorem
CH2.norm_Phi_lambda_neg_one_add_I_mul_le_of_neg
For negative λ, Phi_lambda on -1 + i y is bounded by y away from the downward pole.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3347
theorem
CH2.Phi_star_conj_neg
Conjugation symmetry of Φ^\star: Φ^\star(-\overline{w}) = -\overline{Φ^\star(w)}. This is the
complex-argument generalization of Phi_star_conj_symm.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3426
lemma
CH2.IsBoundedNoPolesOn.analytic_mul
Multiplying a bounded-with-no-poles function by an analytic factor that is uniformly bounded on
the set preserves IsBoundedNoPolesOn.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3460
lemma
CH2.IsBoundedNoPolesOn.linear_mul
Multiplying a bounded-with-no-poles function h by an analytic factor φ whose growth is
controlled by a weight w - ‖φ‖ ≤ C(‖w‖+1) - preserves IsBoundedNoPolesOn, provided the
weighted product w · h is itself bounded with no poles. (Used for the Φ^\star = O(|z|) factors:
the linear growth is absorbed by the extra decay of w · h = z(s) · F · x₀^s.)
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3492
lemma
CH2.meromorphicOrderAt_nonneg_of_eventually_bounded
If f is bounded on a punctured neighborhood of z, its meromorphic order there is ≥ 0.
(If f is not meromorphic at z the order is the junk value 0; otherwise a negative order would
force f → ∞, contradicting the bound.)
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3510
theorem
CH2.integral_Iic_one_eq_integral_Ioi_one_sub
Change variables from the left ray (-∞, 1] to the positive half-line by t = 1-r.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3719
theorem
CH2.prop_5_2_a
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:3986
theorem
CH2.prop_5_2_b
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2.lean:4094
lemma
CH2.summable_nterm_of_log_weight
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:41
lemma
CH2.fourier_scale_div_noscalar
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:72
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.