Skip to main content
therefore
Sign inSign up
Open navigation
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.

Research project325 GitHub starsApache-2.09 indexed versionsRepositoryFull 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 1,021 to 1,040 of 1,644 declarations.

lemma

Complex.CartanBound.intervalIntegrable_phi_dyadic

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:450

lemma

Complex.CartanBound.intervalIntegrable_phi_div

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:465

lemma

Complex.CartanBound.integral_phi_le_Cφ_mul_small

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:487

lemma

Complex.CartanBound.integral_phi_le_Cφ_mul_large

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:509

lemma

Complex.CartanBound.integral_phi_le_Cφ_mul

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:570

lemma

Complex.CartanBound.integral_phi_div_le_Cφ_mul

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:624

lemma

Complex.Hadamard.max_one_norm_div_pow_le_one_add_rpow

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanInverseFactorBound.lean:40

lemma

Complex.Hadamard.norm_inv_weierstrassFactor_le_exp_near

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanInverseFactorBound.lean:69

lemma

Complex.Hadamard.norm_inv_weierstrassFactor_le_exp_far

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanInverseFactorBound.lean:116

lemma

Complex.Hadamard.cartanProductConstant_nonneg

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanMajorantBound.lean:67

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.