Repository navigation
Expand file tree
/
Copy pathPrimeGapsTheory.lean
More file actions
233 lines (232 loc) · 13 KB
/
Copy pathPrimeGapsTheory.lean
File metadata and controls
233 lines (232 loc) · 13 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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
module -- shake: keep-all --deprecated_module: ignore
public import PrimeGapsTheory.Analysis.IntegralOperators
public import PrimeGapsTheory.Analysis.SieveTruncation
public import PrimeGapsTheory.Analysis.Simplex
public import PrimeGapsTheory.Analysis.SingularSeries
public import PrimeGapsTheory.Analysis.SpecificSums
public import PrimeGapsTheory.Analysis.Tonelli.EuclideanLemmas
public import PrimeGapsTheory.Analysis.Tonelli.L1Euclidean
public import PrimeGapsTheory.Analysis.Tonelli.L1General
public import PrimeGapsTheory.Analysis.Tonelli.LpEuclidean
public import PrimeGapsTheory.Analysis.Tonelli.LpGeneral
public import PrimeGapsTheory.Analysis.Zeta
public import PrimeGapsTheory.Arithmetic.BDefect
public import PrimeGapsTheory.Arithmetic.ConstantsAB
public import PrimeGapsTheory.Arithmetic.ConvergentSums
public import PrimeGapsTheory.Arithmetic.DivisorTails
public import PrimeGapsTheory.Arithmetic.EulerProducts
public import PrimeGapsTheory.Arithmetic.GStarLeadingCoeff
public import PrimeGapsTheory.Arithmetic.GammaDensity
public import PrimeGapsTheory.Arithmetic.GammaLogSum
public import PrimeGapsTheory.Arithmetic.HAsymptotic
public import PrimeGapsTheory.Arithmetic.HAsymptotic.Assembly
public import PrimeGapsTheory.Arithmetic.HAsymptotic.ConvForm
public import PrimeGapsTheory.Arithmetic.HAsymptotic.Helpers
public import PrimeGapsTheory.Arithmetic.HAsymptotic.Summability
public import PrimeGapsTheory.Arithmetic.LogDivSq
public import PrimeGapsTheory.Arithmetic.MaynardWeight
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeDensity
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeDensity.Asymptotic
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeDensity.DyadicTail
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeDensity.GKernel
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeDensity.PartialBounds
public import PrimeGapsTheory.Arithmetic.Mertens.CoprimeHarmonic
public import PrimeGapsTheory.Arithmetic.Mertens.ReciprocalW
public import PrimeGapsTheory.Arithmetic.Mertens.Shared
public import PrimeGapsTheory.Arithmetic.Mertens.TauK
public import PrimeGapsTheory.Arithmetic.Mertens.W
public import PrimeGapsTheory.Arithmetic.MobiusLcm
public import PrimeGapsTheory.Arithmetic.PartialSummation
public import PrimeGapsTheory.Arithmetic.PrimeIndicator
public import PrimeGapsTheory.Arithmetic.RemovedPrimes
public import PrimeGapsTheory.Arithmetic.RestrictedReciprocalSum
public import PrimeGapsTheory.Arithmetic.SingularSeries
public import PrimeGapsTheory.Arithmetic.TdDecomposition
public import PrimeGapsTheory.Arithmetic.TdDecomposition.Decomp
public import PrimeGapsTheory.Arithmetic.TdDecomposition.Eval
public import PrimeGapsTheory.Arithmetic.TdDecomposition.SizeHyp
public import PrimeGapsTheory.Arithmetic.TdDecomposition.Summands
public import PrimeGapsTheory.Arithmetic.Totient.Basic
public import PrimeGapsTheory.Arithmetic.Totient.Lcm
public import PrimeGapsTheory.ArithmeticFunction.Basic
public import PrimeGapsTheory.ArithmeticFunction.Estimates
public import PrimeGapsTheory.ArithmeticFunction.FunctionG
public import PrimeGapsTheory.ArithmeticFunction.LYTransform.Basic
public import PrimeGapsTheory.ArithmeticFunction.LYTransform.Estimate
public import PrimeGapsTheory.ArithmeticFunction.LYTransform.Specialized
public import PrimeGapsTheory.ArithmeticFunction.ProdPrimePower
public import PrimeGapsTheory.ArithmeticFunction.Rpow
public import PrimeGapsTheory.ArithmeticFunction.Tau
public import PrimeGapsTheory.ArithmeticFunction.Totient
public import PrimeGapsTheory.Auxiliary.Floor
public import PrimeGapsTheory.Auxiliary.UnionBound
public import PrimeGapsTheory.Discrete.FinMulAntidiag
public import PrimeGapsTheory.Discrete.MaxRealAbs
public import PrimeGapsTheory.Endgame.Main
public import PrimeGapsTheory.Endgame.MainProp
public import PrimeGapsTheory.Endgame.ManyPrimes
public import PrimeGapsTheory.ForMathlib.Algebra.BigOperators.Finsupp.Basic
public import PrimeGapsTheory.ForMathlib.Algebra.Order.Field.Basic
public import PrimeGapsTheory.ForMathlib.Analysis.Asymptotics.Defs
public import PrimeGapsTheory.ForMathlib.Analysis.SpecialFunctions.Gamma.Beta
public import PrimeGapsTheory.ForMathlib.Analysis.SpecialFunctions.Log.Summable
public import PrimeGapsTheory.ForMathlib.Combinatorics.Enumerative.Composition
public import PrimeGapsTheory.ForMathlib.Data.Finsupp.Basic
public import PrimeGapsTheory.ForMathlib.Data.Nat.Choose.Basic
public import PrimeGapsTheory.ForMathlib.Data.Nat.Squarefree
public import PrimeGapsTheory.ForMathlib.IsMultiplicativeOn
public import PrimeGapsTheory.ForMathlib.LinearAlgebra.Finsupp.Supported
public import PrimeGapsTheory.ForMathlib.NumberTheory.ArithmeticFunction.Defs
public import PrimeGapsTheory.ForMathlib.NumberTheory.ArithmeticFunction.Moebius
public import PrimeGapsTheory.ForMathlib.NumberTheory.Divisors
public import PrimeGapsTheory.ForMathlib.Topology.Algebra.InfiniteSum.Defs
public import PrimeGapsTheory.ForMathlib.Topology.Algebra.InfiniteSum.ENNReal
public import PrimeGapsTheory.Foundations.AdmissibleCardinality
public import PrimeGapsTheory.Foundations.MaynardSieveDatum
public import PrimeGapsTheory.Foundations.SieveDatum
public import PrimeGapsTheory.Gap246.Endgame.Main
public import PrimeGapsTheory.Gap246.Endgame.Mollify
public import PrimeGapsTheory.Gap246.Endgame.ThetaBV
public import PrimeGapsTheory.Gap246.Endgame.Witness
public import PrimeGapsTheory.Gap246.Sieve.Certificate.Abstract
public import PrimeGapsTheory.Gap246.Sieve.Certificate.Explicit
public import PrimeGapsTheory.Gap246.Sieve.Certificate.ExplicitToAbstract
public import PrimeGapsTheory.Gap246.Sieve.Certificate.Hypothesis
public import PrimeGapsTheory.Gap246.Sieve.Certificate.Witness
public import PrimeGapsTheory.Gap246.Sieve.PositivityWindow
public import PrimeGapsTheory.Gap246.Sieve.Retained
public import PrimeGapsTheory.Gap246.Sieve.S1
public import PrimeGapsTheory.Gap246.Sieve.S2
public import PrimeGapsTheory.Gap246.Sieve.S2.Core
public import PrimeGapsTheory.Gap246.Sieve.S2.Cutoff
public import PrimeGapsTheory.Gap246.Sieve.S2.DiagonalApproximation
public import PrimeGapsTheory.Gap246.Sieve.S2.ErrorAbsorption
public import PrimeGapsTheory.Gap246.Sieve.S2.InverseForms
public import PrimeGapsTheory.Gap246.Sieve.S2.LowerBound
public import PrimeGapsTheory.Gap246.Sieve.S2.ProfileDefinitions
public import PrimeGapsTheory.Gap246.Sieve.S2.RetainedCRT
public import PrimeGapsTheory.Gap246.Sieve.S2.WeightBounds
public import PrimeGapsTheory.Gap246.Sieve.SupportSplit
public import PrimeGapsTheory.Gap246.Sieve.Weight
public import PrimeGapsTheory.Gap246.Tuple.H50
public import PrimeGapsTheory.Gap246.Variational.EnlargedSimplex
public import PrimeGapsTheory.Gap246.Variational.Marginal
public import PrimeGapsTheory.NumberTheory.Admissible
public import PrimeGapsTheory.NumberTheory.BombieriVinogradov
public import PrimeGapsTheory.NumberTheory.Compatibility
public import PrimeGapsTheory.NumberTheory.DyadicPNT
public import PrimeGapsTheory.NumberTheory.LevelOfDistribution
public import PrimeGapsTheory.NumberTheory.PNT
public import PrimeGapsTheory.NumberTheory.PrimeCountingInterval
public import PrimeGapsTheory.NumberTheory.PrimeCountingSubset
public import PrimeGapsTheory.NumberTheory.PrimeCountingZMod
public import PrimeGapsTheory.NumberTheory.PrimeSumEstimates
public import PrimeGapsTheory.Sieve.BombieriVinogradov
public import PrimeGapsTheory.Sieve.CRT
public import PrimeGapsTheory.Sieve.Certificate.Explicit
public import PrimeGapsTheory.Sieve.Certificate.Fast
public import PrimeGapsTheory.Sieve.Common.Decoupling
public import PrimeGapsTheory.Sieve.Common.Expansion
public import PrimeGapsTheory.Sieve.Common.PrimeWindow
public import PrimeGapsTheory.Sieve.Common.S2mEvalAssembly
public import PrimeGapsTheory.Sieve.Common.SieveDatumEval
public import PrimeGapsTheory.Sieve.Common.SieveDatumEval.KFold
public import PrimeGapsTheory.Sieve.Common.SieveDatumEval.LayerG
public import PrimeGapsTheory.Sieve.Common.SieveDatumEval.Lipschitz
public import PrimeGapsTheory.Sieve.Common.SieveDatumEval.PartialSummation
public import PrimeGapsTheory.Sieve.Common.SijD0.Basic
public import PrimeGapsTheory.Sieve.Common.SijD0.FirstMoment
public import PrimeGapsTheory.Sieve.Common.SijOne
public import PrimeGapsTheory.Sieve.Common.Substitution.Basic
public import PrimeGapsTheory.Sieve.Common.Substitution.FirstMoment
public import PrimeGapsTheory.Sieve.Common.SumOverDivisors
public import PrimeGapsTheory.Sieve.MaynardG
public import PrimeGapsTheory.Sieve.PNT
public import PrimeGapsTheory.Sieve.PermissibleSupport.Basic
public import PrimeGapsTheory.Sieve.PermissibleSupport.FunctionD0
public import PrimeGapsTheory.Sieve.PermissibleSupport.FunctionW
public import PrimeGapsTheory.Sieve.PowerSum
public import PrimeGapsTheory.Sieve.S1.ApplyPartialSum
public import PrimeGapsTheory.Sieve.S1.CRT
public import PrimeGapsTheory.Sieve.S1.DecoupleLcm
public import PrimeGapsTheory.Sieve.S1.Decoupling
public import PrimeGapsTheory.Sieve.S1.DropUij
public import PrimeGapsTheory.Sieve.S1.Expansion
public import PrimeGapsTheory.Sieve.S1.ExpansionBinomial
public import PrimeGapsTheory.Sieve.S1.FromY
public import PrimeGapsTheory.Sieve.S1.RemoveAutomatic
public import PrimeGapsTheory.Sieve.S1.RestrictSij
public import PrimeGapsTheory.Sieve.S1.SijCoprimeToW
public import PrimeGapsTheory.Sieve.S1.SijDichotomy
public import PrimeGapsTheory.Sieve.S1.SijOne
public import PrimeGapsTheory.Sieve.S1.Smoothing
public import PrimeGapsTheory.Sieve.S1.SubstituteSmoothY
public import PrimeGapsTheory.Sieve.S2m.Bilinear
public import PrimeGapsTheory.Sieve.S2m.CRT
public import PrimeGapsTheory.Sieve.S2m.DecouplePhiLcm
public import PrimeGapsTheory.Sieve.S2m.DmEmOne
public import PrimeGapsTheory.Sieve.S2m.Error
public import PrimeGapsTheory.Sieve.S2m.Error.Basic
public import PrimeGapsTheory.Sieve.S2m.Error.Main
public import PrimeGapsTheory.Sieve.S2m.Error.TauFourSums
public import PrimeGapsTheory.Sieve.S2m.Error.TauGrowth
public import PrimeGapsTheory.Sieve.S2m.Error.WindowError
public import PrimeGapsTheory.Sieve.S2m.Eval
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.Blocks
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.Collision
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.Drop
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.Expand
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.GSumBounds
public import PrimeGapsTheory.Sieve.S2m.ExpandDrop.Main
public import PrimeGapsTheory.Sieve.S2m.Expansion
public import PrimeGapsTheory.Sieve.S2m.GCoord
public import PrimeGapsTheory.Sieve.S2m.MainCRT
public import PrimeGapsTheory.Sieve.S2m.Mobius
public import PrimeGapsTheory.Sieve.S2m.QFactor
public import PrimeGapsTheory.Sieve.S2m.SecondMoment
public import PrimeGapsTheory.Sieve.S2m.SijD0
public import PrimeGapsTheory.Sieve.S2m.SijD0.GTail
public import PrimeGapsTheory.Sieve.S2m.SijD0.Main
public import PrimeGapsTheory.Sieve.S2m.SijD0.MertensFactorG
public import PrimeGapsTheory.Sieve.S2m.SijD0.PairMasterG
public import PrimeGapsTheory.Sieve.S2m.SijOne
public import PrimeGapsTheory.Sieve.S2m.Smooth
public import PrimeGapsTheory.Sieve.S2m.Substitution
public import PrimeGapsTheory.Sieve.SieveTruncation
public import PrimeGapsTheory.Sieve.Sums
public import PrimeGapsTheory.Sieve.Transforms.YFromLambda
public import PrimeGapsTheory.Sieve.Transforms.YmAjNeRj
public import PrimeGapsTheory.Sieve.Transforms.YmAjNeRj.Harmonic
public import PrimeGapsTheory.Sieve.Transforms.YmAjNeRj.Kernel
public import PrimeGapsTheory.Sieve.Transforms.YmAjNeRj.Main
public import PrimeGapsTheory.Sieve.Transforms.YmFromY
public import PrimeGapsTheory.Sieve.Transforms.YmRearrange
public import PrimeGapsTheory.Sieve.Transforms.YmSubstitute
public import PrimeGapsTheory.Sieve.Transforms.YmSubstituteSmooth
public import PrimeGapsTheory.Tactic.PaperTag
public import PrimeGapsTheory.Tactic.Utils
public import PrimeGapsTheory.Variational.BasisBd
public import PrimeGapsTheory.Variational.Integration.Beta
public import PrimeGapsTheory.Variational.Integration.Simplex
public import PrimeGapsTheory.Variational.M016Asymp.EkDiagonalTruncation
public import PrimeGapsTheory.Variational.M016Asymp.EtaLowerBound
public import PrimeGapsTheory.Variational.M016Asymp.GPositive
public import PrimeGapsTheory.Variational.M016Asymp.IkTensorUpperBound
public import PrimeGapsTheory.Variational.M016Asymp.MuClosedForm
public import PrimeGapsTheory.Variational.M016Asymp.TUpperBound
public import PrimeGapsTheory.Variational.M105
public import PrimeGapsTheory.Variational.Marginal.DecoupledSeparate
public import PrimeGapsTheory.Variational.Marginal.Gk
public import PrimeGapsTheory.Variational.Marginal.Infra
public import PrimeGapsTheory.Variational.Marginal.PinCoordReindex
public import PrimeGapsTheory.Variational.Marginal.YdiscApprox
public import PrimeGapsTheory.Variational.MkApprox
public import PrimeGapsTheory.Variational.MkRatio
public import PrimeGapsTheory.Variational.MkVerified
public import PrimeGapsTheory.Variational.PartitionCounts
public import PrimeGapsTheory.Variational.PolynomialF
public import PrimeGapsTheory.Variational.PosDef
public import PrimeGapsTheory.Variational.QuadForms
public import PrimeGapsTheory.Variational.Rayleigh
public import PrimeGapsTheory.Variational.SmoothApprox