HighDimProb/HighDimProbTest.lean at main · dududuguo/HighDimProb · GitHub

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
import HighDimProbTest.Smoke
import HighDimProbTest.PublicImports
import HighDimProbTest.BranchImports
import HighDimProbTest.ProbabilityObjectAPI
import HighDimProbTest.UnionBoundAPI
import HighDimProbTest.TailAPI
import HighDimProbTest.TailProofsAPI
import HighDimProbTest.LpMomentAPI
import HighDimProbTest.RealInequalitiesAPI
import HighDimProbTest.OrliczAPI
import HighDimProbTest.SubGaussianAPI
import HighDimProbTest.SubExponentialAPI
import HighDimProbTest.ConcentrationAPI
import HighDimProbTest.LayerCakeAPI
import HighDimProbTest.OrliczToTailAPI
import HighDimProbTest.TailToOrliczAPI
import HighDimProbTest.ConcentrationImplicationsAPI
import HighDimProbTest.ScalarConcentrationMilestoneAPI
import HighDimProbTest.MomentImplicationsAPI
import HighDimProbTest.MGFImplicationsAPI
import HighDimProbTest.SubGaussianSumsAPI
import HighDimProbTest.SubExponentialSumsAPI
import HighDimProbTest.BernsteinAPI
import HighDimProbTest.HoeffdingAPI
import HighDimProbTest.RademacherAPI
import HighDimProbTest.RademacherFamilyAPI
import HighDimProbTest.RademacherSumsAPI
import HighDimProbTest.RandomFamilyAPI
import HighDimProbTest.RandomVectorAPI
import HighDimProbTest.CovarianceAPI
import HighDimProbTest.CovarianceProofsAPI
import HighDimProbTest.IsotropicAPI
import HighDimProbTest.IsotropicProofsAPI
import HighDimProbTest.SubGaussianVectorAPI
import HighDimProbTest.RandomMatrixBasicAPI
import HighDimProbTest.RandomMatrixRowsColsAPI
import HighDimProbTest.RandomMatrixActionAPI
import HighDimProbTest.RandomMatrixNormsAPI
import HighDimProbTest.RandomMatrixAssumptionsAPI
import HighDimProbTest.RandomMatrixSampleCovarianceAPI
import HighDimProbTest.RandomMatrixQuadraticFormAPI
import HighDimProbTest.RandomMatrixOperatorNormAPI
import HighDimProbTest.RandomMatrixSpectralAPI
import HighDimProbTest.RandomMatrixTraceExpAPI
import HighDimProbTest.RandomMatrixLaplaceAPI
import HighDimProbTest.RandomMatrixVarianceProxyAPI
import HighDimProbTest.RandomMatrixStatementsAPI
import HighDimProbTest.RandomMatrixConcentrationAPI
import HighDimProbTest.RandomMatrixProofsAPI
import HighDimProbTest.LimitTheoremsAPI
import HighDimProbTest.NetsMetricEntropyAPI
import HighDimProbTest.NetsProofsAPI
import HighDimProbTest.MetricEntropyStatementsAPI
import HighDimProbTest.BookStatements
import HighDimProbTest.NoDeepMathYet
import HighDimProbTest.ExperimentalImports
import HighDimProbTest.ExamplesAPI