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,341 to 1,360 of 1,644 declarations.
lemma
Smooth1MellinConvergent
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1490
lemma
Smooth1MellinDifferentiable
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.MellinCalculus · PrimeNumberTheoremAnd/MellinCalculus.lean:1513
lemma
RectangleIntegral_tendsTo_VerticalIntegral
Obvious. -/) (latexEnv := "lemma")] lemma zeroTendstoDiff (L₁ L₂ : ℂ) (f : ℝ → ℂ) (h : ∀ᶠ T in atTop, f T = 0) (h' : Tendsto f atTop (𝓝 (L₂ - L₁))) : L₁ = L₂ := by rw [← zero_add L₁, ← @eq_sub_iff_add_eq] exact tendsto_nhds_unique (EventuallyEq.tendsto h) h'
/- TODO: Move this to general section.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:38
lemma
verticalIntegral_eq_verticalIntegral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:67
lemma
verticalIntegral_sub_verticalIntegral_eq_squareIntegral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:79
theorem
tendsto_truncated_vertical_shift_with_simple_pole
Truncated contour shift through a simple pole. The left vertical side stays as the symmetric truncation; only the right vertical side is required to be Bochner integrable.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:110
theorem
tendsto_truncated_vertical_shift_with_simple_pole_Ioo
Set-integral form of tendsto_truncated_vertical_shift_with_simple_pole, normalized
as (2π)⁻¹ ∫ f(σ + it) dt.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:191
lemma
RectangleIntegral_tendsTo_UpperU
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:209
lemma
RectangleIntegral_tendsTo_LowerU
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:240
lemma
limitOfConstant
TODO : Move to general section
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:293
lemma
limitOfConstantLeft
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:315
lemma
tendsto_rpow_atTop_nhds_zero_of_norm_gt_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:352
lemma
Perron.f_mul_eq_f
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:389
lemma
Perron.isHolomorphicOn
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:403
lemma
Perron.integralPosAux'_of_le
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:441
lemma
Perron.vertIntBound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:490
lemma
Perron.vertIntBoundLeft
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:534
theorem
Perron.isTheta_uniformlyOn_uIcc
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:598
lemma
Perron.isIntegrable
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:634
theorem
Perron.horizontal_integral_isBigO
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.PerronFormula · PrimeNumberTheoremAnd/PerronFormula.lean:664
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.