Repository navigation
Expand file tree
/
Copy pathPrimeNumberTheoremAnd.lean
More file actions
135 lines (134 loc) · 9.1 KB
/
Copy pathPrimeNumberTheoremAnd.lean
File metadata and controls
135 lines (134 loc) · 9.1 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
module -- shake: keep-all --deprecated_module: ignore
public import PrimeNumberTheoremAnd.Auxiliary
public import PrimeNumberTheoremAnd.Backlund.ZeroCountCrude
public import PrimeNumberTheoremAnd.BorelCaratheodory
public import PrimeNumberTheoremAnd.BrunTitchmarsh
public import PrimeNumberTheoremAnd.Consequences
public import PrimeNumberTheoremAnd.Defs
public import PrimeNumberTheoremAnd.EulerMaclaurin
public import PrimeNumberTheoremAnd.Fourier
public import PrimeNumberTheoremAnd.GeneralMeromorphic
public import PrimeNumberTheoremAnd.HadamardFactorization
public import PrimeNumberTheoremAnd.HoffsteinLockhart
public import PrimeNumberTheoremAnd.IEANTN.BKLNW.BKLNW_app_tables
public import PrimeNumberTheoremAnd.IEANTN.CH2.CH2
public import PrimeNumberTheoremAnd.IEANTN.CH2.CH2_part1
public import PrimeNumberTheoremAnd.IEANTN.FKS2Cor24TrustedNumerics
public import PrimeNumberTheoremAnd.IEANTN.FKS2TrustedNumerics
public import PrimeNumberTheoremAnd.IEANTN.HadamardLogDerivative
public import PrimeNumberTheoremAnd.IEANTN.KLN
public import PrimeNumberTheoremAnd.IEANTN.Kadiri
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq11Base
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq11Reduction
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq12Foundations
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq13
public import PrimeNumberTheoremAnd.IEANTN.KadiriEq14
public import PrimeNumberTheoremAnd.IEANTN.KadiriSupport
public import PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting
public import PrimeNumberTheoremAnd.IEANTN.LiSeries
public import PrimeNumberTheoremAnd.IEANTN.LnFactorialSeries
public import PrimeNumberTheoremAnd.IEANTN.Mertens
public import PrimeNumberTheoremAnd.IEANTN.MobiusLemma
public import PrimeNumberTheoremAnd.IEANTN.PVIdentity
public import PrimeNumberTheoremAnd.IEANTN.PrimaryDefinitions
public import PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldPrime_tables
public import PrimeNumberTheoremAnd.IEANTN.RosserSchoenfeld.RosserSchoenfeldZeta
public import PrimeNumberTheoremAnd.IEANTN.ZetaAppendix
public import PrimeNumberTheoremAnd.IEANTN.ZetaDefinitions
public import PrimeNumberTheoremAnd.IEANTN.ZetaSummary
public import PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP
public import PrimeNumberTheoremAnd.IEANTN.eSHP.eSHP_tables
public import PrimeNumberTheoremAnd.IwaniecKowalskiCh1
public import PrimeNumberTheoremAnd.LaplaceInversion
public import PrimeNumberTheoremAnd.Mathlib.Algebra.Notation.Support
public import PrimeNumberTheoremAnd.Mathlib.Algebra.Order.Floor.Ring
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Asymptotics
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Asymptotics.Uniformly
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.AbsMax
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Basic
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.BorelCaratheodory
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalDecomposition
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CanonicalProduct
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanInverseFactorBound
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanMajorantBound
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanProductBound
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CauchyIntegral
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Convex
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Divisor
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorComplement
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorConvergence
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorIndex
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorPartialProductFactor
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientConvergence
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorQuotientRemovable
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ExpPoly.Growth
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Growth
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Order
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.HadamardFactorization.Summability
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.LocallyUniformLimit
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Trigonometric
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Growth
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.WeierstrassFactor
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorHolomorphic
public import PrimeNumberTheoremAnd.Mathlib.Analysis.Meromorphic.DivisorSupport
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.CompletedXi
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Exp
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.CriticalLineDecay
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.DigammaSeries
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.GammaStirlingAux
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.IntegralBounds
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Gamma.StripBounds
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.GammaBounds
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Basic
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.Dyadic
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.ExpGrowth
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Log.PosLog
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Deriv
public import PrimeNumberTheoremAnd.Mathlib.Analysis.SpecialFunctions.Pow.Real
public import PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntegrableOn
public import PrimeNumberTheoremAnd.Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.AbelSummation
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.Chebyshev
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelContinuation
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaHadamard
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaPartialSum
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaStripBound
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaValues
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFiniteOrder
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.ZetaFunctionalEquation
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.AuxResults
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Basic
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.Selberg
public import PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds
public import PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Annulus
public import PrimeNumberTheoremAnd.Mathlib.Topology.MetricSpace.Cauchy
public import PrimeNumberTheoremAnd.MediumPNT
public import PrimeNumberTheoremAnd.MellinCalculus
public import PrimeNumberTheoremAnd.PerronFormula
public import PrimeNumberTheoremAnd.Rectangle
public import PrimeNumberTheoremAnd.RectangleArgumentPrinciple
public import PrimeNumberTheoremAnd.ResidueCalcOnRectangles
public import PrimeNumberTheoremAnd.SincKernelErrorBounds
public import PrimeNumberTheoremAnd.SmoothExistence
public import PrimeNumberTheoremAnd.Sobolev
public import PrimeNumberTheoremAnd.StrongPNT
public import PrimeNumberTheoremAnd.Tactic.AdditiveCombination
public import PrimeNumberTheoremAnd.Tactic.Simprocs
public import PrimeNumberTheoremAnd.Unused.ZetaBoundsUnused
public import PrimeNumberTheoremAnd.Wiener
public import PrimeNumberTheoremAnd.ZetaBounds
public import PrimeNumberTheoremAnd.ZetaConj