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,041 to 1,060 of 1,644 declarations.

lemma

Complex.Hadamard.cartan_majorant_four_term_bound

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

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

lemma

Complex.Hadamard.cartan_card_small_le

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

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

lemma

Complex.Hadamard.cartan_rpow_mul_le

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

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

lemma

hasProd_inv_unconditional

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:52

lemma

hasProd_norm_inv_unconditional

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:70

lemma

hasProd_norm_inv_le_exp_of_pointwise_le_exp

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanProductBound.lean:81

theorem

Complex.Hadamard.eventually_exists_analyticAt_eq_pow_smul_divisorComplementPartialProduct

At a nonzero divisor index, the canonical product has the same multiplicity as the original function. -/ theorem analyticOrderAt_divisorCanonicalProduct_at_index (m : ℕ) {f : ℂ → ℂ} (hf : Differentiable ℂ f) (h_sum : Summable (fun p : divisorZeroIndex₀ f (Set.univ : Set ℂ) => ‖divisorZeroIndex₀_val p‖⁻¹ ^ (m + 1))) (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) : analyticOrderAt (divisorCanonicalProduct m f (Set.univ : Set ℂ)) (divisorZeroIndex₀_val p) = (analyticOrderNatAt f (divisorZeroIndex₀_val p) : ℕ∞) := by have horder := analyticOrderAt_divisorCanonicalProduct_eq_fiber_card (m := m) (f := f) (h_sum := h_sum) (z₀ := divisorZeroIndex₀_val p) have hfiber : (divisorZeroIndex₀_fiberFinset (f := f) (divisorZeroIndex₀_val p)).card = analyticOrderNatAt f (divisorZeroIndex₀_val p) := divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt (hf := hf) (z₀ := divisorZeroIndex₀_val p) p.property simpa [hfiber] using horder

/-!

Refining the factorization: factoring out (z - z₀)^k using the fiber-only product

When s contains the fiber finset, we can write the partial product as

divisorPartialProduct s = (z - z₀)^k • (divisorComplementPartialProduct s * u)

where u is the analytic quotient coming from the fiber-only product.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Divisor.lean:309

lemma

Complex.Hadamard.divisorComplementFactor_def

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:62

theorem

Complex.Hadamard.differentiable_divisorPartialProduct

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

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:102

theorem

Complex.Hadamard.hasProdUniformlyOn_divisorComplementCanonicalProduct_univ

The infinite product over indices not in the fiber over z₀ (the “complement” canonical product). -/ noncomputable def divisorComplementCanonicalProduct (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ) (z : ℂ) : ℂ := ∏' p : divisorZeroIndex₀ f (Set.univ : Set ℂ), divisorComplementFactor m f z₀ p z

/-!

Convergence/holomorphy of the complement canonical product

This is the same M-test argument as for divisorCanonicalProduct, but with finitely many factors replaced by 1. We keep the same summability hypothesis.

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorComplement.lean:190

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.