Documentation Verification Report

Modules

61 modules

ModuleDefinitionsTheoremsSorry
PrimeNumberTheoremAnd/Auxiliary.lean 0 13
PrimeNumberTheoremAnd/BKLNW.lean 17 37 3
PrimeNumberTheoremAnd/BKLNW_a2_bounds.lean 0 13
PrimeNumberTheoremAnd/BKLNW_app.lean 22 15 11
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 8 24 14
PrimeNumberTheoremAnd/Chebyshev.lean 5 19 3
PrimeNumberTheoremAnd/Consequences.lean 2 80
PrimeNumberTheoremAnd/CostaPereira.lean 0 10
PrimeNumberTheoremAnd/Defs.lean 25 4
PrimeNumberTheoremAnd/DerivativeBound.lean 0 2 1
PrimeNumberTheoremAnd/Dusart.lean 4 36 34
PrimeNumberTheoremAnd/Erdos392.lean 21 96 1
PrimeNumberTheoremAnd/FKS2.lean 15 34 17
PrimeNumberTheoremAnd/FioriKadiriSwidinsky.lean 31 29 25
PrimeNumberTheoremAnd/Fourier.lean 2 11
PrimeNumberTheoremAnd/GeneralMeromorphic.lean 1 3
PrimeNumberTheoremAnd/Goldbach.lean 2 12 5
PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean 6 14 8
PrimeNumberTheoremAnd/KLN.lean 35 0
PrimeNumberTheoremAnd/Lcm.lean 14 55 3
PrimeNumberTheoremAnd/Li2Bounds.lean 3 18
PrimeNumberTheoremAnd/LogTables.lean 0 24
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/PerronFormula.lean 1 45
PrimeNumberTheoremAnd/PrimeInInterval.lean 0 7
PrimeNumberTheoremAnd/Ramanujan.lean 12 18 18
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 1
PrimeNumberTheoremAnd/SecondarySummary.lean 2 18 16
PrimeNumberTheoremAnd/SmoothExistence.lean 0 2
PrimeNumberTheoremAnd/Sobolev.lean 30 35
PrimeNumberTheoremAnd/StrongPNT.lean 9 24 7
PrimeNumberTheoremAnd/Tactic/AdditiveCombination.lean 3 3
PrimeNumberTheoremAnd/Wiener.lean 18 191 2
PrimeNumberTheoremAnd/ZetaAppendix.lean 2 45 3
PrimeNumberTheoremAnd/ZetaBounds.lean 2 165
PrimeNumberTheoremAnd/ZetaBoundsUnused.lean 0 1
PrimeNumberTheoremAnd/ZetaConj.lean 0 9
PrimeNumberTheoremAnd/ZetaDefinitions.lean 18 1
PrimeNumberTheoremAnd/ZetaSummary.lean 0 6 6
PrimeNumberTheoremAnd/eSHP.lean 0 20 5
PrimeNumberTheoremAnd/eSHP_tables.lean 2 0