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 1,381 to 1,400 of 1,644 declarations.
lemma
divisor_support_rectangle_finite
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:264
theorem
rectangleIntegral_logDeriv_eq_sum_meromorphicOrderAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:276
theorem
rectangle_argumentChange_eq_two_pi_sum_meromorphicOrderAt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.RectangleArgumentPrinciple · PrimeNumberTheoremAnd/RectangleArgumentPrinciple.lean:341
lemma
DiffVertRect_eq_UpperLowerUs
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:112
theorem
RectangleBorderIntegrable.add
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:210
lemma
RectangleIntegralHSplit
Given x₀ a x₁ : ℝ, and y₀ y₁ : ℝ and a function
f : ℂ → ℂ so that both (t : ℝ) ↦ f(t + y₀ * I) and
(t : ℝ) ↦ f(t + y₁ * I) are integrable over both
t ∈ Icc x₀ a and t ∈ Icc a x₁, we have that
RectangleIntegral f (x₀ + y₀ * I) (x₁ + y₁ * I) is the sum of
RectangleIntegral f (x₀ + y₀ * I) (a + y₁ * I) and
RectangleIntegral f (a + y₀ * I) (x₁ + y₁ * I).
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:256
lemma
RectangleIntegralVSplit
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:307
lemma
RectanglePullToNhdOfPole'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:336
lemma
integral_self_div_sq_add_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:497
lemma
integral_const_div_self_add_im
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:520
lemma
integral_const_div_re_add_self
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:543
lemma
ResidueTheoremAtOrigin'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:561
theorem
ResidueTheoremInRectangle
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:583
lemma
ResidueTheoremOnRectangleWithSimplePole
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:609
lemma
IsBigO_to_BddAbove
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:661
theorem
BddAbove_on_rectangle_of_bdd_near
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:680
theorem
ResidueTheoremOnRectangleWithSimplePole'
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:712
lemma
simplePole_sub_residue_isBigO_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:784
lemma
verticalPath_not_eventuallyConst
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:882
lemma
RectangleIntegral'_eq_sumResiduesIn
The Residue Theorem on a rectangle for functions with simple poles.
PrimeNumberTheoremAnd.ResidueCalcOnRectangles · PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean:1189
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.