-
Notifications
You must be signed in to change notification settings - Fork 3
/
Copy pathTestingLowerBounds.lean
55 lines (55 loc) · 2.55 KB
/
TestingLowerBounds.lean
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
import TestingLowerBounds.CompProd
import TestingLowerBounds.Convex
import TestingLowerBounds.CurvatureMeasure
import TestingLowerBounds.DerivAtTop
import TestingLowerBounds.Divergences.Chernoff
import TestingLowerBounds.Divergences.CondHellinger
import TestingLowerBounds.Divergences.CondRenyi
import TestingLowerBounds.Divergences.DeGroot
import TestingLowerBounds.Divergences.EGamma
import TestingLowerBounds.Divergences.Hellinger
import TestingLowerBounds.Divergences.KullbackLeibler.CondKL
import TestingLowerBounds.Divergences.KullbackLeibler.KullbackLeibler
import TestingLowerBounds.Divergences.Renyi
import TestingLowerBounds.Divergences.StatInfo.DPI
import TestingLowerBounds.Divergences.StatInfo.StatInfo
import TestingLowerBounds.Divergences.StatInfo.StatInfoFun
import TestingLowerBounds.Divergences.StatInfo.fDivStatInfo
import TestingLowerBounds.Divergences.TotalVariation
import TestingLowerBounds.ErealLLR
import TestingLowerBounds.FDiv.Basic
import TestingLowerBounds.FDiv.CompProd.CompProd
import TestingLowerBounds.FDiv.CompProd.EqTopIff
import TestingLowerBounds.FDiv.CondFDiv
import TestingLowerBounds.FDiv.CondFDivCompProdMeasure
import TestingLowerBounds.FDiv.DPIJensen
import TestingLowerBounds.FDiv.IntegralRnDerivSingularPart
import TestingLowerBounds.FDiv.Measurable
import TestingLowerBounds.FDiv.Trim
import TestingLowerBounds.FindAxioms
import TestingLowerBounds.ForMathlib.AbsolutelyContinuous
import TestingLowerBounds.ForMathlib.CountableOrCountablyGenerated
import TestingLowerBounds.ForMathlib.EReal
import TestingLowerBounds.ForMathlib.Integrable
import TestingLowerBounds.ForMathlib.KernelFstSnd
import TestingLowerBounds.ForMathlib.LeftRightDeriv
import TestingLowerBounds.ForMathlib.LogLikelihoodRatioCompProd
import TestingLowerBounds.ForMathlib.MaxMinEqAbs
import TestingLowerBounds.ForMathlib.RNDerivEqCondexp
import TestingLowerBounds.ForMathlib.RadonNikodym
import TestingLowerBounds.ForMathlib.RnDeriv
import TestingLowerBounds.IntegrableFRNDeriv
import TestingLowerBounds.Kernel.BayesInv
import TestingLowerBounds.Kernel.Deterministic
import TestingLowerBounds.Kernel.DeterministicComp
import TestingLowerBounds.Kernel.ParallelComp
import TestingLowerBounds.MeasureCompProd
import TestingLowerBounds.Sorry.ByParts
import TestingLowerBounds.Sorry.Jensen
import TestingLowerBounds.SqHellinger
import TestingLowerBounds.Testing.Binary
import TestingLowerBounds.Testing.BoolMeasure
import TestingLowerBounds.Testing.ChangeMeasure
import TestingLowerBounds.Testing.RenyiChangeMeasure
import TestingLowerBounds.Testing.Risk
import TestingLowerBounds.Testing.TwoHypKernel