Repository navigation
Expand file tree
/
Copy pathCycleCutoff.lean
More file actions
146 lines (145 loc) · 7.15 KB
/
Copy pathCycleCutoff.lean
File metadata and controls
146 lines (145 loc) · 7.15 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
module -- shake: keep-all --deprecated_module: ignore
public import CycleCutoff.Attr
public import CycleCutoff.BernoulliLaplace.Defs
public import CycleCutoff.BernoulliLaplace.Lsi
public import CycleCutoff.BernoulliLaplace.LsiBalanced
public import CycleCutoff.BernoulliLaplace.Marginal
public import CycleCutoff.BernoulliLaplace.PhiSupersolution
public import CycleCutoff.BernoulliLaplace.Recursion
public import CycleCutoff.Cutoff.Defs
public import CycleCutoff.Cutoff.EntropyAtWindow
public import CycleCutoff.Cutoff.LowerBound
public import CycleCutoff.Cutoff.LowerTv
public import CycleCutoff.Cutoff.Main
public import CycleCutoff.Cutoff.TotalError
public import CycleCutoff.Cutoff.TvSmallAfterWindow
public import CycleCutoff.Cutoff.UpperBound
public import CycleCutoff.Cutoff.WilsonEigenfunction
public import CycleCutoff.Cutoff.WilsonIncrement
public import CycleCutoff.Cutoff.WilsonMean
public import CycleCutoff.Cutoff.WilsonStationaryMean
public import CycleCutoff.Cutoff.WilsonStationaryVariance
public import CycleCutoff.Cutoff.WilsonVarianceBound
public import CycleCutoff.Cycle.CosineSum
public import CycleCutoff.Cycle.CycleEntropyDecay
public import CycleCutoff.Cycle.CycleLsi
public import CycleCutoff.Cycle.Defs
public import CycleCutoff.Cycle.DnSymmetry
public import CycleCutoff.Cycle.LambdaLower
public import CycleCutoff.Cycle.LambdaUpper
public import CycleCutoff.Cycle.MuPositive
public import CycleCutoff.Definitions
public import CycleCutoff.Exposure.ChainRule
public import CycleCutoff.Exposure.Defs
public import CycleCutoff.Exposure.EntropyError
public import CycleCutoff.Exposure.ExposureBound
public import CycleCutoff.Exposure.LogZBound
public import CycleCutoff.Exposure.PredErrorExpansion
public import CycleCutoff.FiniteProbability.CondExpPullOut
public import CycleCutoff.FiniteProbability.CondExpResidualBound
public import CycleCutoff.FiniteProbability.CondExpTower
public import CycleCutoff.FiniteProbability.CondVarOnEvent
public import CycleCutoff.FiniteProbability.Defs
public import CycleCutoff.FiniteProbability.EntChainRule
public import CycleCutoff.FiniteProbability.EntVarBound
public import CycleCutoff.FiniteProbability.Hypergeometric
public import CycleCutoff.FiniteProbability.Pinsker
public import CycleCutoff.FiniteProbability.PinskerPointwise
public import CycleCutoff.FiniteProbability.PsiPointwise
public import CycleCutoff.FiniteProbability.PushforwardEntropy
public import CycleCutoff.FiniteProbability.PushforwardExpectation
public import CycleCutoff.FiniteProbability.PushforwardVariance
public import CycleCutoff.FiniteProbability.SampleSumMean
public import CycleCutoff.FiniteProbability.SampleSumVariance
public import CycleCutoff.FiniteProbability.SizeBias
public import CycleCutoff.FiniteProbability.UnnormalizedKL
public import CycleCutoff.FiniteProbability.VarDecomposition
public import CycleCutoff.Generator.CanonicalPath
public import CycleCutoff.Generator.ConeInvariance
public import CycleCutoff.Generator.CorrelationDecay
public import CycleCutoff.Generator.CorrelationIntegrable
public import CycleCutoff.Generator.CorrelationRepresentation
public import CycleCutoff.Generator.Defs
public import CycleCutoff.Generator.DirichletFormula
public import CycleCutoff.Generator.DirichletTransport
public import CycleCutoff.Generator.HMinusOne
public import CycleCutoff.Generator.HMinusOneAttained
public import CycleCutoff.Generator.HMinusOneDualBound
public import CycleCutoff.Generator.HMinusOneVariational
public import CycleCutoff.Generator.LieTrotter
public import CycleCutoff.Generator.LogMeanIneq
public import CycleCutoff.Generator.LsiEntropyDecay
public import CycleCutoff.Generator.LsiImpliesPoincare
public import CycleCutoff.Generator.LsiTensorization
public import CycleCutoff.Generator.Lumping
public import CycleCutoff.Generator.PoincareVarianceDecay
public import CycleCutoff.Generator.PoissonSolvable
public import CycleCutoff.Generator.RelEntMonotone
public import CycleCutoff.Generator.SemigroupDeriv
public import CycleCutoff.Generator.SemigroupLower
public import CycleCutoff.Generator.SemigroupRowsum
public import CycleCutoff.Generator.SemigroupSymmetric
public import CycleCutoff.Integrated.CoincidenceCorrelation
public import CycleCutoff.Integrated.CoincidenceIntegrable
public import CycleCutoff.Integrated.CorrectorIdentity
public import CycleCutoff.Integrated.Defs
public import CycleCutoff.Integrated.IntegratedError
public import CycleCutoff.Integrated.PaperErrorIntegrable
public import CycleCutoff.Integrated.ReturnIntegral
public import CycleCutoff.Integrated.RwIntegral
public import CycleCutoff.Integrated.SeparationGenerator
public import CycleCutoff.Integrated.SeparationLaw
public import CycleCutoff.Integrated.SourceOrthogonal
public import CycleCutoff.LocalGap.BetweenSector
public import CycleCutoff.LocalGap.CanonicalPaths
public import CycleCutoff.LocalGap.CycleTwoCopyPoincare
public import CycleCutoff.LocalGap.Defs
public import CycleCutoff.LocalGap.LocalGap
public import CycleCutoff.LocalGap.SharedComparison
public import CycleCutoff.LocalGap.WithinSector
public import CycleCutoff.Multiscale.BlockDual
public import CycleCutoff.Multiscale.BlockFibrePoincare
public import CycleCutoff.Multiscale.BlockMeanCondExp
public import CycleCutoff.Multiscale.BlockSecondMoment
public import CycleCutoff.Multiscale.Defs
public import CycleCutoff.Multiscale.IncrementCentered
public import CycleCutoff.Multiscale.IncrementSecondMoment
public import CycleCutoff.Multiscale.LeafDualBound
public import CycleCutoff.Multiscale.LevelDepth
public import CycleCutoff.Multiscale.LevelDualBound
public import CycleCutoff.Multiscale.LevelStructure
public import CycleCutoff.Multiscale.LevelTelescope
public import CycleCutoff.Multiscale.MatchingDualBound
public import CycleCutoff.Multiscale.Resolvent
public import CycleCutoff.Multiscale.SplitBalance
public import CycleCutoff.OneCard.BBound
public import CycleCutoff.OneCard.BIntegrable
public import CycleCutoff.OneCard.BIntegrandNonneg
public import CycleCutoff.OneCard.BTail
public import CycleCutoff.OneCard.Defs
public import CycleCutoff.OneCard.DeltaInvolution
public import CycleCutoff.OneCard.EigenvalueLower
public import CycleCutoff.OneCard.EigenvalueRatio
public import CycleCutoff.OneCard.HeatDeviation
public import CycleCutoff.OneCard.HeatEntropy
public import CycleCutoff.OneCard.HeatFourier
public import CycleCutoff.OneCard.HeatSup
public import CycleCutoff.OneCard.HeatTranslation
public import CycleCutoff.OneCard.HeatUniform
public import CycleCutoff.OneCard.OneCard
public import CycleCutoff.OneCard.S2Bound
public import CycleCutoff.OneCard.S2Integrable
public import CycleCutoff.PathShuffle.BisectionBetween
public import CycleCutoff.PathShuffle.BisectionWithin
public import CycleCutoff.PathShuffle.ColoredPoincare
public import CycleCutoff.PathShuffle.Defs
public import CycleCutoff.PathShuffle.Lsi
public import CycleCutoff.PathShuffle.Poincare
public import CycleCutoff.PathShuffle.TranspositionComparison
public import CycleCutoff.TwoCopy.BlackMarginal
public import CycleCutoff.TwoCopy.BlackOneCopyLumping
public import CycleCutoff.TwoCopy.BlackProjection
public import CycleCutoff.TwoCopy.BlackPsd
public import CycleCutoff.TwoCopy.CoincidenceDomination
public import CycleCutoff.TwoCopy.Defs
public import CycleCutoff.TwoCopy.ErrorDomination