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 861 to 880 of 1,644 declarations.
lemma
ZetaAppendix.lemma_abadsumas_sum_fourier
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2022
lemma
ZetaAppendix.exp_geometric_partial_sums_bounded
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2165
lemma
ZetaAppendix.cauchySeq_exp_over_nat_of_not_int
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2196
lemma
ZetaAppendix.tendsto_exp_over_nat_eq_neg_log_of_not_int
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2271
lemma
ZetaAppendix.tendsto_sine_series_unit_interval
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2380
lemma
ZetaAppendix.tendsto_sine_series_of_not_int
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2428
lemma
ZetaAppendix.tendsto_sine_over_pi_series_of_not_int
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2446
lemma
ZetaAppendix.tendsto_boundary_sine_terms
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2489
lemma
ZetaAppendix.hasDerivAt_sine_antideriv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2513
lemma
ZetaAppendix.cosine_integral_by_parts_cpow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2538
lemma
ZetaAppendix.hasSum_cos_over_pi_sq_unit_raw
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2613
lemma
ZetaAppendix.hasDerivAt_deriv_ofReal_cpow_neg
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2697
lemma
ZetaAppendix.hasDerivAt_cos_antideriv
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2749
lemma
ZetaAppendix.deriv_kernel_integral_by_parts_cpow
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2777
lemma
ZetaAppendix.deriv_kernel_partial_sum_second_ibp
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2836
lemma
ZetaAppendix.cos_antideriv_norm_bound
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2891
lemma
ZetaAppendix.summable_one_div_two_pi_sq_nat_add_one_sq
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2907
lemma
ZetaAppendix.hasSum_second_ibp_integral_series
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2923
lemma
ZetaAppendix.tendsto_deriv_kernel_second_ibp_limit
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2977
lemma
ZetaAppendix.B1_eq_sub_nat_sub_half_of_mem_Ioo
Open the record for the exact Lean statement and complete source.
PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:3016
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.