Skip to main content

Sign in Sign up

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.

Research project325 GitHub starsApache-2.09 indexed versionsRepository Full history on Reservoir

Head version

a93551347dce

a93551347dce924b1db75d40218841bf085a465f

Toolchain: leanprover/lean4:v4.32.0
Revision date: 22 Jul 2026
Dependencies: 13
Versions: 9

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

Package history

Showing 261 to 280 of 1,644 declarations.

theorem

CH2.shift_upwards_phi_sum

At a point z = 1 + i t on the vertical line Re z = +1 (with t ≥ 0), the combination Φ_circ + Φ_star equals Φ_star evaluated on the imaginary axis at i t.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3680

theorem

CH2.shift_downwards_phi_diff

Away from the pole on the downward line, Φ_circ - Φ_star at -1 - i t equals -Φ_star at -i t.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3695

theorem

CH2.shift_downwards_phi_sum

Away from the pole on the downward line, Φ_circ + Φ_star at 1 - i t equals Φ_star at -i t.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3724

theorem

CH2.shift_upwards_simplified

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3832

lemma

CH2.tendsto_contour_shift_downwards

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3867

lemma

CH2.horizontal_integral_phi_fourier_vanish_downwards

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:3917

lemma

CH2.Phi_diff_bounded_near_pole

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4030

lemma

CH2.Phi_fourier_holo_left

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4039

lemma

CH2.Phi_add_bounded_near_pole

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4092

lemma

CH2.Phi_fourier_holo_right

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4101

lemma

CH2.first_contour_bottom_vanishes

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4355

lemma

CH2.first_contour_integrand_holomorphicOn

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4423

theorem

CH2.first_contour_limit

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4443

lemma

CH2.second_contour_integrand_holomorphicOn

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4632

theorem

CH2.second_contour_limit

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4653

lemma

CH2.third_contour_integrand_holomorphicOn

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4738

theorem

CH2.third_contour_limit

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4756

theorem

CH2.shift_downwards_simplified

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:4826

theorem

CH2.fourier_real

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5015

lemma

CH2.Inu_bounds_neg

Open the record for the exact Lean statement and complete source.

PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1 · PrimeNumberTheoremAnd/IEANTN/CH2/CH2_part1.lean:5109

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.