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,321 to 1,340 of 1,644 declarations.

lemma

PartialIntegration_of_support_in_Icc

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:229

lemma

MellinConvolutionSymmetric

Let us start with a simple property of the Mellin convolution.

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:293

lemma

support_MellinConvolution_subsets

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:327

lemma

MellinConvolutionTransform

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:357

lemma

MellinOfPsi

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:495

theorem

MellinOfDeltaSpike

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:663

lemma

MellinOfDeltaSpikeAt1_asymp

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:700

lemma

Smooth1_def_ite

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:820

lemma

Smooth1Properties_estimate

Let c:=2ϵ>1c:=2^\epsilon > 1, in terms of which we wish to prove

−1<clog⁡c−c. -1 < c \log c - c .

Letting f(x):=xlog⁡x−xf(x):=x\log x - x, we can rewrite this as f(1)<f(c)f(1) < f(c). Since

ddxf(x)=log⁡x>0, \frac {d}{dx}f(x) = \log x > 0 ,

ff is monotone increasing on [1, \infty), and we are done. -/) (latexEnv := "definition")] noncomputable def Smooth1 (ν : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ := MellinConvolution (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) (DeltaSpike ν ε)

-- This lemma might not be necessary, but the RHS is supported on [0, infinity), which makes -- results like support_MellinConvolution_subsets easier to apply. lemma Smooth1_def_ite {ν : ℝ → ℝ} {ε x : ℝ} (xpos : 0 < x) : Smooth1 ν ε x = MellinConvolution (fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0) (fun x ↦ if x < 0 then 0 else DeltaSpike ν ε x) x := by unfold Smooth1 rw [MellinConvolutionSymmetric _ _ xpos] conv => lhs; rw [MellinConvolutionSymmetric _ _ xpos] unfold MellinConvolution apply MeasureTheory.integral_congr_ae filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ioi] simp +contextual only [mem_Ioi, true_and, ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq, mul_ite, mul_zero] intro y ypos rw [eq_comm, if_neg (by push Not; positivity)]

/-% ** Wrong delimiters on purpose, no need to include this in blueprint \begin{lemma}[Smooth1Properties_estimate]\label{Smooth1Properties_estimate} \lean{Smooth1Properties_estimate}\leanok For ϵ>0\epsilon>0,

log⁡2>1−2−ϵϵ \log2>\frac{1-2^{-\epsilon}}\epsilon

\end{lemma} %

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:844

lemma

Smooth1Properties_below

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:886

lemma

Smooth1Properties_above_aux2

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:989

lemma

Smooth1Properties_above

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1011

lemma

Smooth1LeOne

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1135

lemma

MellinOfSmooth1a

Combining the above, we have the following three Main Lemmata of this section on the Mellin transform of 1ϵ~\widetilde{1_{\epsilon}}.

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1198

lemma

MellinOfSmooth1b

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1325

lemma

MellinOfSmooth1c

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1363

lemma

Smooth1ContinuousAt

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

PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1389

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.