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,121 to 1,140 of 1,644 declarations.

theorem

Complex.Hadamard.hadamard_factorization_of_order

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:176

theorem

Complex.Hadamard.hadamard_factorization_of_order_reindex

Reindexed form of hadamard_factorization_of_order, for any index type equivalent to the nonzero divisor indices.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:206

theorem

Complex.Hadamard.hadamard_factorization_of_order_centered

Centered finite-order Hadamard factorization. This is derived from the origin-centered theorem by translating f by c; the product indexes zeros away from the center in centered coordinates.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:253

theorem

Complex.Hadamard.hadamard_factorization_of_order_centered_reindex

Reindexed centered finite-order Hadamard factorization, for any index type equivalent to the centered nonzero divisor indices.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Order.lean:283

lemma

Complex.Hadamard.exists_r0_le_norm_divisorZeroIndex₀_val

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:109

lemma

Complex.Hadamard.card_ball_le_divisorMassClosedBall₀

The number of divisor indices in a closed ball is bounded by the divisor mass there.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:236

lemma

Complex.Hadamard.card_subtype_le_divisorMassClosedBall₀_of_norm_le

A finite family of divisor indices contained in a closed ball has cardinality bounded by the divisor mass of that ball.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:334

lemma

Complex.Hadamard.finite_divisorZeroIndex₀_dyadicShell

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/HadamardFactorization/Summability.lean:381

theorem

TendstoUniformlyOn.mul_left_bounded

On K, uniform convergence is preserved when multiplying on the left by a bounded function.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/LocallyUniformLimit.lean:24

lemma

Complex.norm_inv_pow_le_one_of_one_le_norm

If ‖u‖ ≥ 1, then inverse powers of u have norm at most one.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Norm.lean:44

lemma

Complex.norm_cos_le_exp_abs_im

‖cos z‖ is controlled by exp |im z|.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Trigonometric.lean:16

lemma

Function.locallyFinsuppWithin.massClosedBall₀_mono

The nonzero mass in closed balls is monotone in the radius for non-negative functions.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean:70

theorem

Function.locallyFinsuppWithin.logCounting_divisor_le_of_log_growth

A logarithmic growth bound on an entire function controls its divisor log-counting on a disk.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Growth.lean:41

theorem

Function.locallyFinsuppWithin.log_two_mul_massClosedBall₀_le_logCounting

For non-negative locally finite support, twice the ball radius gives enough log-weight to dominate log 2 times the mass in the ball (excluding the origin).

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Growth.lean:82

lemma

Complex.hasDerivAt_weierstrassFactor_at_one

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:110

lemma

Complex.hasDerivAt_weierstrassFactor_div_at_self

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/WeierstrassFactor.lean:130

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.