Documentation Verification Report

Modules

68 modules

ModuleDefinitionsTheoremsSorry
PrimeNumberTheoremAnd/Auxiliary.lean 0 13
PrimeNumberTheoremAnd/BKLNW.lean 17 37 2
PrimeNumberTheoremAnd/BKLNW_a2_bounds.lean 0 13
PrimeNumberTheoremAnd/BKLNW_app.lean 22 15 7
PrimeNumberTheoremAnd/BKLNW_app_tables.lean 4 66
PrimeNumberTheoremAnd/BKLNW_tables.lean 4 7
PrimeNumberTheoremAnd/BorelCaratheodory.lean 2 7
PrimeNumberTheoremAnd/BrunTitchmarsh.lean 2 32
PrimeNumberTheoremAnd/Buthe.lean 1 6 6
PrimeNumberTheoremAnd/CH2.lean 9 70 28
PrimeNumberTheoremAnd/Chebyshev.lean 6 26
PrimeNumberTheoremAnd/Consequences.lean 2 79
PrimeNumberTheoremAnd/CostaPereira.lean 0 10
PrimeNumberTheoremAnd/Defs.lean 32 4
PrimeNumberTheoremAnd/DerivativeBound.lean 0 2 1
PrimeNumberTheoremAnd/Dusart.lean 4 36 30
PrimeNumberTheoremAnd/Erdos392.lean 21 100
PrimeNumberTheoremAnd/EulerMascheroniBounds.lean 3 11
PrimeNumberTheoremAnd/FKS2.lean 15 70 10
PrimeNumberTheoremAnd/FioriKadiriSwidinsky.lean 31 29 23
PrimeNumberTheoremAnd/Fourier.lean 2 11
PrimeNumberTheoremAnd/GeneralMeromorphic.lean 1 3
PrimeNumberTheoremAnd/Goldbach.lean 2 12 2
PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean 8 26 8
PrimeNumberTheoremAnd/KLN.lean 35 0
PrimeNumberTheoremAnd/Lcm.lean 14 55
PrimeNumberTheoremAnd/Li2Bounds.lean 3 18
PrimeNumberTheoremAnd/LiSeries.lean 0 16
PrimeNumberTheoremAnd/LnFactorialSeries.lean 0 2
PrimeNumberTheoremAnd/LogTables.lean 0 29
PrimeNumberTheoremAnd/Mathlib/Algebra/Notation/Support.lean 0 2
PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Asymptotics.lean 0 5
PrimeNumberTheoremAnd/Mathlib/Analysis/Asymptotics/Uniformly.lean 0 12
PrimeNumberTheoremAnd/Mathlib/Analysis/SpecialFunctions/Log/Basic.lean 0 1
PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean 0 19
PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean 10 17
PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean 4 19
PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean 1 21
PrimeNumberTheoremAnd/MediumPNT.lean 15 43
PrimeNumberTheoremAnd/MellinCalculus.lean 3 60
PrimeNumberTheoremAnd/MobiusLemma.lean 4 11
PrimeNumberTheoremAnd/PVIdentity.lean 0 11
PrimeNumberTheoremAnd/PerronFormula.lean 1 45
PrimeNumberTheoremAnd/PrimeInInterval.lean 0 7
PrimeNumberTheoremAnd/PrimeTables.lean 0 34
PrimeNumberTheoremAnd/RSPrimeLower.lean 0 5
PrimeNumberTheoremAnd/Ramanujan.lean 12 25 3
PrimeNumberTheoremAnd/Rectangle.lean 2 41
PrimeNumberTheoremAnd/ResidueCalcOnRectangles.lean 12 45
PrimeNumberTheoremAnd/RosserSchoenfeldPrime.lean 4 27 1
PrimeNumberTheoremAnd/RosserSchoenfeldPrime_tables.lean 1 0
PrimeNumberTheoremAnd/RosserSchoenfeldZeta.lean 0 1 1
PrimeNumberTheoremAnd/SecondaryDefinitions.lean 0 9
PrimeNumberTheoremAnd/SecondarySummary.lean 2 12 7
PrimeNumberTheoremAnd/SmoothExistence.lean 0 2
PrimeNumberTheoremAnd/Sobolev.lean 30 35
PrimeNumberTheoremAnd/StrongPNT.lean 8 24 6
PrimeNumberTheoremAnd/TMEEMT.lean 6 76 60
PrimeNumberTheoremAnd/Tactic/AdditiveCombination.lean 3 3
PrimeNumberTheoremAnd/Tactic/Simprocs.lean 2 3
PrimeNumberTheoremAnd/Wiener.lean 18 191 2
PrimeNumberTheoremAnd/ZetaAppendix.lean 3 56 1
PrimeNumberTheoremAnd/ZetaBounds.lean 2 164
PrimeNumberTheoremAnd/ZetaConj.lean 0 9
PrimeNumberTheoremAnd/ZetaDefinitions.lean 18 11
PrimeNumberTheoremAnd/ZetaSummary.lean 0 6 6
PrimeNumberTheoremAnd/eSHP.lean 0 20 5
PrimeNumberTheoremAnd/eSHP_tables.lean 2 0