Repository navigation
Expand file tree
/
Copy pathLibrary.lean
More file actions
281 lines (281 loc) · 13.7 KB
/
Copy pathLibrary.lean
File metadata and controls
281 lines (281 loc) · 13.7 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
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
import Library.Numerics.Arithmetic.Gcd.Module
import Library.Numerics.Arithmetic.Gcd.Program
import Library.Numerics.Arithmetic.Gcd.Verify
import Library.Random.Lcg.Jump
import Library.Random.Lcg.Lattice
import Library.Random.Lcg.Period
import Library.Random.Lcg.Program
import Library.Random.Lcg.Spectral
import Library.Numerics.Statistics.Mean.Module
import Library.Numerics.Statistics.Mean.Program
import Library.Numerics.Statistics.Mean.Verify
import Library.Random.Orbit.Basic
import Library.Random.ParkMiller.Period
import Library.Random.ParkMiller.Program
import Library.Numerics.Arithmetic.PrimeFactors.Program
import Library.Numerics.Arithmetic.PrimeFactors.Verify
import Library.Random.SplitMix64.Verify
import Library.Numerics.Statistics.SumSquares.Module
import Library.Numerics.Statistics.SumSquares.Program
import Library.Numerics.Statistics.SumSquares.Verify
import Library.Random.Xorshift.Columns
import Library.Random.Xorshift.Jump
import Library.Random.Xorshift.Period
import Library.Random.Xorshift.Program
import Library.Numerics.Float64.Trig.Compiled
import Library.Numerics.Fourier.Compiled
import Library.Random.Lcg.Verified
import Library.Random.ParkMiller.Verified
import Library.Random.Xorshift.Verified
import Library.Numerics.Float64.Exp.Compiled
import Library.Numerics.Float64.Tanh.Compiled
import Library.Numerics.Float64.Log.Compiled
import Library.Numerics.Float64.Log1p.Compiled
import Library.Numerics.Float64.Atan.Compiled
import Library.Numerics.Float64.Asin.Compiled
import Library.Numerics.Float64.Tan.Compiled
import Library.Numerics.Float64.Sinh.Compiled
import Library.Numerics.Float64.Asinh.Compiled
import Library.Numerics.Float64.Exp2.Compiled
import Library.Numerics.Float64.Log2.Compiled
import Library.Numerics.Float64.Log10.Compiled
import Library.Numerics.Float64.Pow.Compiled
import Library.Numerics.Float64.Sinpi.Compiled
import Library.Numerics.Float64.Erf.Compiled
import Library.Numerics.Float64.Trig.TrigTheorem
import Library.Numerics.Float64.Log2.Log2Theorem
import Library.Numerics.Float64.Log2.Log2Power
import Library.Numerics.Float64.Log10.Log10Theorem
import Library.Numerics.Float64.Tanh.TanhBytes
import Library.Numerics.Float64.Tanh.Expm1Near
import Library.Numerics.Float64.Erf.ErfTheorem
import Library.Numerics.Float64.Log1p.Log1pBytes
import Library.Numerics.Float64.Atan.AtanBytes
import Library.Numerics.Float64.Atan.AtanTwoSpecial
import Library.Numerics.Float64.Atan.AtanTwoNaN
import Library.Numerics.Float64.Asin.AsinBytes
import Library.Numerics.Float64.Tan.TanTheorem
import Library.Numerics.Float64.Sinh.SinhBytes
import Library.Numerics.Float64.Sinpi.SinpiTheorem
import Library.Numerics.Float64.Asinh.AsinhBytes
import Library.Numerics.Float64.Tgamma.TgammaApprox
import Library.Numerics.Float64.Tgamma.Compiled
import Library.Numerics.Float64.Lgamma.Compiled
import Library.Numerics.Float64.Bessel.Compiled
import Library.Numerics.Float64.Erfc.Compiled
import Library.Numerics.Arithmetic.Fma.FmaSpec
import Library.Numerics.Float64.Bessel.BesselJ0Theorem
import Library.Numerics.Float64.Bessel.BesselJ1Theorem
import Library.Numerics.Float64.Bessel.BesselY0Theorem
import Library.Numerics.Float64.Bessel.BesselY1Theorem
import Library.Numerics.Float64.Bessel.BesselBytes
import Library.Numerics.Float64.Tgamma.TgammaBytes
import Library.Numerics.Float64.Erfc.ErfcBytes
import Library.Numerics.Float64.Erfc.ErfcNonfinite
import Library.Numerics.Arithmetic.Fma.FmaSpecTheorem
import Library.Numerics.Float64.Lgamma.LgammaApprox
import Library.Numerics.Float64.Lgamma.LgammaSpecial
import Library.Numerics.Float64.Tgamma.TgammaMul
import Library.Numerics.Float64.Tgamma.TgammaSmallPath
import Library.Numerics.Float64.Erfc.ErfcFastPath
import Library.Numerics.Float64.Erfc.ErfcTrack3
import Library.Numerics.Float64.Tgamma.GammaPi
import Library.Numerics.Float64.Lgamma.LgammaSign
import Library.Numerics.Float64.Lgamma.LgammaWalk
import Library.Numerics.Float64.Lgamma.LgammaFastTiny
import Library.Numerics.Float64.Lgamma.LgammaPolyFst
import Library.Numerics.Float64.Lgamma.LgammaFastSmall
import Library.Numerics.Float64.Lgamma.LgammaPiecePoly
import Library.Numerics.Float64.Lgamma.LgammaPieceIdx
import Library.Numerics.Float64.Lgamma.LgammaFastPiece
import Library.Numerics.Float64.Lgamma.LgammaFastMid
import Library.Numerics.Float64.Lgamma.LgammaRecip
import Library.Numerics.Float64.Lgamma.LgammaStirSeries
import Library.Numerics.Float64.Lgamma.LgammaStir
import Library.Numerics.Float64.Lgamma.LgammaFastPos
import Library.Numerics.Float64.Lgamma.LgammaSinpiAbs
import Library.Numerics.Float64.Lgamma.LgammaReflCore
import Library.Numerics.Float64.Lgamma.LgammaReflTail
import Library.Numerics.Float64.Lgamma.LgammaReflMid
import Library.Numerics.Float64.Lgamma.LgammaReflWin
import Library.Numerics.Float64.Lgamma.LgammaFastWalk
import Library.Numerics.Float64.Lgamma.LgammaLeaf
import Library.Numerics.Float64.Lgamma.LgammaPolyDD
import Library.Numerics.Float64.Lgamma.LgammaPolyDDSteps
import Library.Numerics.Float64.Lgamma.LgammaPolyIv
import Library.Numerics.Float64.Lgamma.LgammaAccPoly
import Library.Numerics.Float64.Lgamma.LgammaLogdOne
import Library.Numerics.Float64.Lgamma.LgammaLogdAcc
import Library.Numerics.Float64.Lgamma.LgammaLogAccKern
import Library.Numerics.Float64.Lgamma.LgammaLogAccRed
import Library.Numerics.Float64.Lgamma.LgammaLogAccTail
import Library.Numerics.Float64.Lgamma.LgammaSinAcc
import Library.Numerics.Float64.Lgamma.LgammaSinAccKern
import Library.Numerics.Float64.Lgamma.LgammaSinAccRed
import Library.Numerics.Float64.Lgamma.LgammaSinAccTail
import Library.Numerics.Float64.Lgamma.LgammaAsymRecip
import Library.Numerics.Float64.Lgamma.LgammaAsymSeries
import Library.Numerics.Float64.Lgamma.LgammaAsymKern
import Library.Numerics.Float64.Lgamma.LgammaAsymLog
import Library.Numerics.Float64.Lgamma.LgammaAsymProd
import Library.Numerics.Float64.Lgamma.LgammaAsymAcc
import Library.Numerics.Float64.Lgamma.LgammaAccLow
import Library.Numerics.Float64.Lgamma.LgammaAccAdd
import Library.Numerics.Float64.Lgamma.LgammaAccRange
import Library.Numerics.Float64.Lgamma.LgammaAccWin
import Library.Numerics.Float64.Lgamma.LgammaAccWinSmall
import Library.Numerics.Float64.Lgamma.LgammaAccRefl
import Library.Numerics.Float64.Lgamma.LgammaAccNorm
import Library.Numerics.Float64.Lgamma.LgammaRootEval
import Library.Numerics.Float64.Lgamma.LgammaRootPath
import Library.Numerics.Float64.Lgamma.LgammaRootSpec
import Library.Numerics.Float64.Lgamma.LgammaAccCancel
import Library.Numerics.Float64.Lgamma.LgammaAccFinal
import Library.Numerics.Float64.Lgamma.LgammaAccGrowth
import Library.Numerics.Float64.Lgamma.LgammaAccLower
import Library.Numerics.Float64.Lgamma.LgammaAccNeg
import Library.Numerics.Float64.Lgamma.LgammaAccNegAsym
import Library.Numerics.Float64.Lgamma.LgammaAccNegLarge
import Library.Numerics.Float64.Lgamma.LgammaAccPair
import Library.Numerics.Float64.Lgamma.LgammaAccPath
import Library.Numerics.Float64.Lgamma.LgammaAccPos
import Library.Numerics.Float64.Lgamma.LgammaAccRegion
import Library.Numerics.Float64.Lgamma.LgammaAccRoot
import Library.Numerics.Float64.Lgamma.LgammaAccTail
import Library.Numerics.Float64.Lgamma.LgammaAccTests
import Library.Numerics.Float64.Lgamma.LgammaAccWalk
import Library.Numerics.Float64.Lgamma.LgammaRootDom
import Library.Numerics.Float64.Lgamma.LgammaRootKern
import Library.Numerics.Float64.Lgamma.LgammaRootRanges
import Library.Numerics.Float64.Lgamma.LgammaRootSel
import Library.Numerics.Decimal.Shared.StrconvDecode
import Library.Numerics.Decimal.Shared.StrconvInterval
import Library.Numerics.Decimal.Shared.StrconvOfScientific32
import Library.Numerics.Decimal.Shared.StrconvTruncate
import Library.Numerics.Float64.Tgamma.TgammaAsym1
import Library.Numerics.Float64.Tgamma.TgammaAsymFitB
import Library.Numerics.Float64.Tgamma.TgammaAsymFitC
import Library.Numerics.Float64.Tgamma.TgammaExpdSpec
import Library.Numerics.Float64.Tgamma.TgammaInt
import Library.Numerics.Float64.Tgamma.TgammaLogdCheck
import Library.Numerics.Float64.Tgamma.TgammaLogdKernel
import Library.Numerics.Float64.Tgamma.TgammaMainPath
import Library.Numerics.Float64.Tgamma.TgammaPolyMainEdge
import Library.Numerics.Float64.Tgamma.TgammaPolySmallAcc
import Library.Numerics.Float64.Pow.PowBytes
import Library.Numerics.Float64.Pow.PowZeroSign
import Library.Numerics.Float64.Tgamma.TgammaAsym6
import Library.Numerics.Float64.Tgamma.TgammaLogd
import Library.Numerics.Arithmetic.Uscale.UscaleDiv
import Library.Numerics.Float64.Bessel.BesselMillerFinal
import Library.Numerics.Float64.Bessel.BesselJnTheorem
import Library.Numerics.Float64.Bessel.BesselYnSmallReal
import Library.Numerics.Float64.Bessel.BesselYnSteps
import Library.Numerics.Float64.Bessel.BesselYnSmall
import Library.Numerics.Float64.Bessel.BesselYnOrderOne
import Library.Numerics.Float64.Bessel.BesselYnTheorem
import Library.Numerics.Float64.Bessel.BesselNSpecial
import Library.Numerics.Float64.Bessel.BesselOrderHuge
import Library.Numerics.Float64.Erfc.ErfcAccAll
import Library.Numerics.Float64.Erfc.ErfcAsymFast
import Library.Numerics.Float64.Erfc.ErfcAsymRowsA0
import Library.Numerics.Float64.Erfc.ErfcAsymRowsA1
import Library.Numerics.Float64.Erfc.ErfcAccPath
import Library.Numerics.Float64.Erfc.ErfcAsymAccFin
import Library.Numerics.Float64.Erfc.ErfcAsymAccHL
import Library.Numerics.Float64.Erfc.ErfcEAcc
import Library.Numerics.Float64.Erfc.ErfcEAccPoly
import Library.Numerics.Float64.Erfc.ErfcHardAsym
import Library.Numerics.Float64.Erfc.ErfcHardAsym0
import Library.Numerics.Float64.Erfc.ErfcHardAsym1
import Library.Numerics.Float64.Erfc.ErfcHardBase
import Library.Numerics.Float64.Erfc.ErfcHardNeg
import Library.Numerics.Float64.Erfc.ErfcHardPos
import Library.Numerics.Float64.Erfc.ErfcHardRows
import Library.Numerics.Float64.Erfc.ErfcMainPath
import Library.Numerics.Float64.Erfc.ErfcSpecial
import Library.Numerics.Float64.Erfc.ErfcTaccData
import Library.Numerics.Float64.Erfc.ErfcTaccLoop
import Library.Numerics.Float64.Erfc.ErfcTheorem
import Library.Numerics.Float64.Erfc.ErfcTrack5
import Library.Numerics.Float64.Lgamma.LgammaLogd
import Library.Numerics.Float64.Lgamma.LgammaSinpi
import Library.Numerics.Decimal.ParseFloat.ParseFloatBytes
import Library.Numerics.Decimal.PrintFloat.PrintFloatBytes
import Library.Numerics.Float64.Tgamma.TgammaFinal
import Library.Numerics.Float64.Lgamma.LgammaAccMid
import Library.Numerics.Float64.Lgamma.LgammaAccSmall
import Library.Numerics.Float64.Lgamma.LgammaAsymLowA
import Library.Numerics.Float64.Lgamma.LgammaAsymLowB
import Library.Numerics.Float64.Lgamma.LgammaAsymLowC
import Library.Numerics.Float64.Lgamma.LgammaAsymLowD
import Library.Numerics.Float64.Lgamma.LgammaAsymLowE
import Library.Numerics.Float64.Lgamma.LgammaAsymLowF
import Library.Numerics.Float64.Lgamma.LgammaAsymLowG
import Library.Numerics.Float64.Lgamma.LgammaAsymLowH
import Library.Numerics.Float64.Lgamma.LgammaAsymMidA
import Library.Numerics.Float64.Lgamma.LgammaAsymMidB
import Library.Numerics.Float64.Lgamma.LgammaAsymMidC
import Library.Numerics.Float64.Lgamma.LgammaDb
import Library.Numerics.Float64.Lgamma.LgammaPiece10A
import Library.Numerics.Float64.Lgamma.LgammaPiece10B
import Library.Numerics.Float64.Lgamma.LgammaPiece10C
import Library.Numerics.Float64.Lgamma.LgammaPiece10D
import Library.Numerics.Float64.Lgamma.LgammaPiece10E
import Library.Numerics.Float64.Lgamma.LgammaPiece10F
import Library.Numerics.Float64.Lgamma.LgammaPiece10G
import Library.Numerics.Float64.Lgamma.LgammaPiece10H
import Library.Numerics.Float64.Lgamma.LgammaPiece4
import Library.Numerics.Float64.Lgamma.LgammaPiecesA
import Library.Numerics.Float64.Lgamma.LgammaPiecesB
import Library.Numerics.Float64.Lgamma.LgammaPiecesC
import Library.Numerics.Float64.Lgamma.LgammaPiecesD
import Library.Numerics.Float64.Lgamma.LgammaPiecesE
import Library.Numerics.Float64.Lgamma.LgammaRootC
import Library.Numerics.Float64.Lgamma.LgammaRootE
import Library.Numerics.Float64.Lgamma.LgammaRootF
import Library.Numerics.Float64.Lgamma.LgammaSinpiAcc
import Library.Numerics.Float64.Lgamma.LgammaSmallFact
import Library.Numerics.Float64.Lgamma.LgammaStirLarge
import Library.Numerics.Float64.Lgamma.LgammaZeroBase
import Library.Numerics.Float64.Tgamma.TgammaFacts
import Library.Numerics.Float64.Tgamma.TgammaWithin
import Library.Numerics.Float64.Lgamma.LgammaFacts
import Library.Numerics.Float64.Lgamma.LgammaEndCell
import Library.Numerics.Float64.Lgamma.LgammaEndEncl
import Library.Numerics.Float64.Lgamma.LgammaEnds
import Library.Numerics.Float64.Lgamma.LgammaBounds
import Library.Numerics.Float64.Tgamma.TgammaDDTop
import Library.Numerics.Float64.Lgamma.LgammaStirTop
import Library.Numerics.Float64.Lgamma.LgammaFastTop
import Library.Numerics.Float64.Lgamma.LgammaAccTop
import Library.Numerics.Float64.Lgamma.LgammaWithin
import Library.Numerics.Float64.Lgamma.LgammaBytes
import Library.Sorting.Insertion.Compiled
import Library.Arrays.Search.Compiled
import Library.Arrays.Filter.Compiled
import Library.Arrays.Repeat.Compiled
import Library.Arrays.Range.Compiled
import Library.Arrays.Word.Compiled
import Library.Lists.Word.Compiled
import Library.Numerics.Reductions.Word.Compiled
import Library.Numerics.Reductions.Float64.Compiled
import Library.Numerics.LinearAlgebra.Float64.Compiled
import Library.Numerics.LinearAlgebra.Binary32.Compiled
import Library.Numerics.Arithmetic.CeilSqrt.Compiled
import Library.Numerics.Bounds.Compiled
import Library.Numerics.Limiters.Minmod.Compiled
import Library.Trees.WordTree.Compiled
import Library.Numerics.Arithmetic.CeilSqrt.Proof
import Library.Numerics.Bounds.Proof
import Library.Numerics.Limiters.Minmod.Proof
import Library.Arrays.Search.Proof
import Library.Hashing.Sha256.Bytes
import Library.Hashing.Sha512.Bytes
import Library.Hashing.Hmac.Bytes
import Library.Hashing.Sha3.Bytes
import Library.Hashing.Crc.Bytes
import Library.Hashing.SipHash.Bytes
import Library.Hashing.XxHash64.Bytes
import Library.Regex.Bytes
import Library.Hashing.MerkleDamgard