statlib/Statlib.lean at main · stat-lib/statlib · 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
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
import Statlib.Causal.PotentialResponse
import Statlib.Contiguity.Def
import Statlib.Divergence.BretagnolleHuber
import Statlib.Divergence.Chernoff
import Statlib.Divergence.Chernoff.Prod
import Statlib.Divergence.Chernoff.Properties
import Statlib.Divergence.FDiv.Basic
import Statlib.Divergence.FDiv.Binary
import Statlib.Divergence.FDiv.CompProd
import Statlib.Divergence.FDiv.CondFDiv
import Statlib.Divergence.FDiv.Conj
import Statlib.Divergence.FDiv.Convex
import Statlib.Divergence.FDiv.DivFunction.Basic
import Statlib.Divergence.FDiv.DivFunction.CompAffine
import Statlib.Divergence.FDiv.DivFunction.Conj
import Statlib.Divergence.FDiv.DivFunction.CurvatureMeasure
import Statlib.Divergence.FDiv.DivFunction.DerivAtTop
import Statlib.Divergence.FDiv.DivFunction.OfReal
import Statlib.Divergence.FDiv.DivFunction.RightDerivStieltjes
import Statlib.Divergence.FDiv.Estimation
import Statlib.Divergence.FDiv.IntegralRepresentation
import Statlib.Divergence.FDiv.Measurable
import Statlib.Divergence.FDiv.SupRatio
import Statlib.Divergence.FDiv.Trim
import Statlib.Divergence.FDiv.TrimApprox
import Statlib.Divergence.Hellinger.Basic
import Statlib.Divergence.Hellinger.CondHellinger
import Statlib.Divergence.Hellinger.HellingerDivFun
import Statlib.Divergence.Hellinger.HellingerFun
import Statlib.Divergence.Hellinger.Prod
import Statlib.Divergence.Hellinger.Renyi
import Statlib.Divergence.Hellinger.TotalVariation
import Statlib.Divergence.JensenShannon.Basic
import Statlib.Divergence.JensenShannon.Hellinger
import Statlib.Divergence.JensenShannon.Variational
import Statlib.Divergence.KullbackLeibler.Basic
import Statlib.Divergence.KullbackLeibler.CondKL
import Statlib.Divergence.KullbackLeibler.Estimation
import Statlib.Divergence.KullbackLeibler.Event
import Statlib.Divergence.KullbackLeibler.KLDivFun
import Statlib.Divergence.MutualInformation.Basic
import Statlib.Divergence.MutualInformation.Bool
import Statlib.Divergence.MutualInformation.Estimation
import Statlib.Divergence.MutualInformation.LeftRight
import Statlib.Divergence.Renyi.Basic
import Statlib.Divergence.Renyi.Bernoulli
import Statlib.Divergence.Renyi.ChainRule
import Statlib.Divergence.Renyi.CondRenyi
import Statlib.Divergence.Renyi.DataProcessing
import Statlib.Divergence.Renyi.Order
import Statlib.Divergence.Renyi.Order.Limits
import Statlib.Divergence.Renyi.Prod
import Statlib.Divergence.Renyi.ProdCountable
import Statlib.Divergence.Renyi.Variational
import Statlib.Divergence.StatInfo.Basic
import Statlib.Divergence.StatInfo.CurvatureMeasure
import Statlib.Divergence.StatInfo.Event
import Statlib.Divergence.StatInfo.FDiv
import Statlib.Divergence.StatInfo.StatInfoDivFun
import Statlib.Divergence.StatInfo.StatInfoFun
import Statlib.Divergence.TotalVariation
import Statlib.Divergence.TotalVariation.Event
import Statlib.Divergence.TotalVariation.Integral
import Statlib.EValues.Bernoulli
import Statlib.EValues.DPI
import Statlib.EValues.Divergence
import Statlib.EValues.EVarClass
import Statlib.EValues.EVariable
import Statlib.EValues.LowerBound
import Statlib.EValues.Numeraire
import Statlib.EValues.NumeraireExistence
import Statlib.EValues.Product
import Statlib.EValues.RIPr
import Statlib.EValues.Utility.Basic
import Statlib.EValues.Utility.Log
import Statlib.ForMathlib.Analysis.Calculus.LocalExtr.Basic
import Statlib.ForMathlib.Analysis.Convex.Deriv
import Statlib.ForMathlib.Analysis.Convex.DerivAtTop
import Statlib.ForMathlib.Analysis.SpecialFunctions.Log.Basic
import Statlib.ForMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.Deriv
import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.NNReal
import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.Real
import Statlib.ForMathlib.Convex
import Statlib.ForMathlib.ENNReal
import Statlib.ForMathlib.EReal
import Statlib.ForMathlib.ISup
import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Basic
import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Bernoulli
import Statlib.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
import Statlib.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
import Statlib.ForMathlib.InformationTheory.KullbackLeibler.EIntegral
import Statlib.ForMathlib.MeasureTheory.Constructions.Pi
import Statlib.ForMathlib.MeasureTheory.Function.ConditionalLExpectation
import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Bochner
import Statlib.ForMathlib.MeasureTheory.Integral.EReal.EIntegrable
import Statlib.ForMathlib.MeasureTheory.Integral.EReal.EIntegral
import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Kernel
import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Prod
import Statlib.ForMathlib.MeasureTheory.Integral.Layercake
import Statlib.ForMathlib.MeasureTheory.Integral.MeanInequalities
import Statlib.ForMathlib.MeasureTheory.Integral.Pi
import Statlib.ForMathlib.MeasureTheory.Komlos
import Statlib.ForMathlib.MeasureTheory.MeasurableSpace.Basic
import Statlib.ForMathlib.MeasureTheory.Measure.Bool
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.Hahn
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.IntegralRPowRNDeriv
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivTrim
import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
import Statlib.ForMathlib.MeasureTheory.Measure.ERealStieltjes
import Statlib.ForMathlib.MeasureTheory.Measure.Lebesgue.Basic
import Statlib.ForMathlib.MeasureTheory.Measure.LogLikelihoodRatio
import Statlib.ForMathlib.MeasureTheory.Measure.Prod
import Statlib.ForMathlib.MeasureTheory.Measure.Real
import Statlib.ForMathlib.MeasureTheory.Measure.Trim
import Statlib.ForMathlib.MeasureTheory.Measure.Typeclasses.Probability
import Statlib.ForMathlib.MeasureTheory.Measure.Typeclasses.SFinite
import Statlib.ForMathlib.MeasureTheory.Order.Group.Lattice
import Statlib.ForMathlib.Probability.Decision.BayesEstimator
import Statlib.ForMathlib.Probability.Decision.Risk.Basic
import Statlib.ForMathlib.Probability.Decision.Risk.RiskIncrease
import Statlib.ForMathlib.Probability.Decision.ZeroOneLoss
import Statlib.ForMathlib.Probability.Distributions.Bernoulli
import Statlib.ForMathlib.Probability.Kernel.Basic
import Statlib.ForMathlib.Probability.Kernel.Composition.Lemmas
import Statlib.ForMathlib.Probability.Kernel.Composition.MeasureCompProd
import Statlib.ForMathlib.Probability.Kernel.Composition.RadonNikodym
import Statlib.ForMathlib.Probability.Kernel.Posterior
import Statlib.ForMathlib.Probability.Moments.Variance
import Statlib.ForMathlib.Probability.Process.Filtration
import Statlib.ForMathlib.Probability.Process.PartitionFiltration
import Statlib.ForMathlib.Probability.Process.Stopping
import Statlib.ForMathlib.Probability.ProductMeasure
import Statlib.ForMathlib.Probability.StrongLaw
import Statlib.ForMathlib.Topology.Order.MonotoneConvergence
import Statlib.Inference.Inference
import Statlib.Inference.QMD
import Statlib.Testing.Binary
import Statlib.Testing.BinaryRenyi
import Statlib.Testing.ChangeMeasure
import Statlib.Testing.ChangeMeasureMoments
import Statlib.Testing.ChangeMeasureRisk
import Statlib.Testing.Chernoff
import Statlib.Testing.Fano
import Statlib.Testing.Hellinger
import Statlib.Testing.RenyiChangeMeasure
import Statlib.Testing.SampleComplexity
import Statlib.Testing.SampleComplexityBounds
import Statlib.Testing.Sequential.Basic
import Statlib.Testing.Sequential.KLDiv
import Statlib.Testing.Sequential.Renyi
import Statlib.Testing.Sequential.Wald