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,441 to 1,460 of 1,644 declarations.
lemma
hardy_diff_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:193
lemma
hardy_k_ratio_bounded
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:226
theorem
hardy_tauberian
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:242
theorem
hardy_tauberian_theorem
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:261
theorem
fourier_partial_sum_eq_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:312
theorem
fejer_sum_eq_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:337
theorem
dirichlet_kernel_closed_form
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:357
theorem
fejer_kernel_closed_form
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:370
theorem
fejer_kernel_nonneg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:389
theorem
fejer_kernel_integral_one
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:406
theorem
fejer_kernel_le_linear
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:425
theorem
fejer_kernel_le_quadratic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:437
theorem
fejer_kernel_uniform_limit_zero
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:454
theorem
uniform_continuity_shift
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:478
theorem
integral_periodic_shift
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:512
theorem
fejer_sum_eq_integral_alt
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:596
theorem
fejer_integrand_periodic
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:620
theorem
fejer_sum_sub_f_eq_integral
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:641
theorem
fejer_kernel_tail_mass_vanishes
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:871
lemma
fejer_central_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.Unused.Fejer_I_know_this_is_dirty_but_it_typechecks · PrimeNumberTheoremAnd/Unused/Fejer_I_know_this_is_dirty_but_it_typechecks.lean:895
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.