Repository navigation
Expand file tree
/
Copy pathMarkovProcess.lean
More file actions
251 lines (250 loc) · 13.5 KB
/
Copy pathMarkovProcess.lean
File metadata and controls
251 lines (250 loc) · 13.5 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
module
public import MarkovProcess.Analysis.ExpPrimitive
public import MarkovProcess.Analysis.PaleyZygmund
public import MarkovProcess.Continuity.DenseTimeContinuousExtension
public import MarkovProcess.Continuity.DenseTimeContinuousLaw
public import MarkovProcess.Continuity.DenseTimeContinuousSupport
public import MarkovProcess.Continuity.DyadicChaining
public import MarkovProcess.Continuity.DyadicFloor
public import MarkovProcess.Continuity.DyadicIncrements
public import MarkovProcess.Continuity.DyadicPathChaining
public import MarkovProcess.Continuity.GlobalDyadicFloorModification
public import MarkovProcess.Continuity.KolmogorovDenseTimeContinuousSupport
public import MarkovProcess.Continuity.KolmogorovTimeShift
public import MarkovProcess.Continuity.PathModulus
public import MarkovProcess.Continuity.PathTightness
public import MarkovProcess.Continuity.ShiftedUnitModification
public import MarkovProcess.DenseTime.CanonicalDiscreteLaw
public import MarkovProcess.DenseTime.CanonicalDiscretePath
public import MarkovProcess.DenseTime.CemeteryDenseTimeMarginals
public import MarkovProcess.DenseTime.CemeteryExtension
public import MarkovProcess.DenseTime.CemeterySemigroup
public import MarkovProcess.DenseTime.ConditionalKernel
public import MarkovProcess.DenseTime.PhysicalCompactTestTransport
public import MarkovProcess.DenseTime.PhysicalReindex
public import MarkovProcess.DenseTime.PrefixKernel
public import MarkovProcess.DenseTime.PrefixRecursion
public import MarkovProcess.DenseTime.Shift
public import MarkovProcess.DenseTime.Trajectory
public import MarkovProcess.DenseTime.TrajectoryMarginals
public import MarkovProcess.DenseTime.TwoPointMarginals
public import MarkovProcess.Examples.BrownianMotion
public import MarkovProcess.Examples.Drift
public import MarkovProcess.Examples.HeatGenerator
public import MarkovProcess.Examples.HeatSemigroup
public import MarkovProcess.Examples.HeatOnePoint
public import MarkovProcess.Examples.Identity
public import MarkovProcess.Feller.BackwardC0Convergence
public import MarkovProcess.Feller.BackwardC0Integral
public import MarkovProcess.Feller.BackwardC0Recursion
public import MarkovProcess.Feller.CoordinatePolynomialContinuity
public import MarkovProcess.Feller.CoordinateProductContinuity
public import MarkovProcess.Feller.DensePhysicalFiniteSetContinuity
public import MarkovProcess.Feller.FiniteDenseApproximationContinuity
public import MarkovProcess.Feller.FiniteSetCompactTestContinuity
public import MarkovProcess.Feller.FiniteSetConvergence
public import MarkovProcess.Feller.FiniteTimeCompactTestContinuity
public import MarkovProcess.Feller.FiniteTimeContinuityBase
public import MarkovProcess.Feller.FiniteTimeConvergence
public import MarkovProcess.Feller.FiniteTimeJointCompactTestContinuity
public import MarkovProcess.Feller.FiniteTimeKernelContinuity
public import MarkovProcess.Feller.Resolvent
public import MarkovProcess.Feller.Semigroup
public import MarkovProcess.FiniteTime.CoordinateProductActiveReduction
public import MarkovProcess.FiniteTime.CoordinateProductNormalization
public import MarkovProcess.FiniteTime.DenseTimeFiniteSetKernelShift
public import MarkovProcess.FiniteTime.DenseTimeFiniteShift
public import MarkovProcess.FiniteTime.FiniteProductCompactSupportApproximation
public import MarkovProcess.FiniteTime.FiniteProductCoordinateNormalForm
public import MarkovProcess.FiniteTime.FiniteProductStoneWeierstrass
public import MarkovProcess.FiniteTime.FiniteSetKernelCompactTestTransport
public import MarkovProcess.FiniteTime.FiniteSetKernelShift
public import MarkovProcess.FiniteTime.Kernel
public import MarkovProcess.FiniteTime.KernelConcatenation
public import MarkovProcess.FiniteTime.KernelDeletion
public import MarkovProcess.FiniteTime.KernelEquivariance
public import MarkovProcess.FiniteTime.KernelMixedPullback
public import MarkovProcess.FiniteTime.KernelRestriction
public import MarkovProcess.FiniteTime.KernelShift
public import MarkovProcess.FiniteTime.MeasureFiniteRestrictionIdentification
public import MarkovProcess.FiniteTime.ProjectiveFamily
public import MarkovProcess.Kernel.Basic
public import MarkovProcess.Kernel.C0
public import MarkovProcess.Kernel.C0SemigroupJoint
public import MarkovProcess.Kernel.CompProdReindex
public import MarkovProcess.Kernel.ConservativityAE
public import MarkovProcess.Kernel.FiniteRestrictionIdentification
public import MarkovProcess.Kernel.Integral
public import MarkovProcess.Kernel.KernelSemigroup
public import MarkovProcess.Kernel.KolmogorovMoments
public import MarkovProcess.Kernel.Lp
public import MarkovProcess.Kernel.LpConsistency
public import MarkovProcess.Kernel.LpFinite
public import MarkovProcess.Kernel.LpTop
public import MarkovProcess.Kernel.MeasurableRadonFamily
public import MarkovProcess.Kernel.OnePointExtension
public import MarkovProcess.Kernel.OnePointKilled
public import MarkovProcess.Kernel.ConservativeResolvent
public import MarkovProcess.Kernel.OnePointConservative
public import MarkovProcess.Kernel.OnePointKolmogorov
public import MarkovProcess.Kernel.Operator
public import MarkovProcess.Kernel.OperatorSemigroup
public import MarkovProcess.Kernel.PositiveC0OperatorKernel
public import MarkovProcess.Kernel.PositiveC0OperatorMass
public import MarkovProcess.Kernel.PositiveC0OperatorMeasure
public import MarkovProcess.Kernel.PositiveC0Resolvent
public import MarkovProcess.Kernel.PositiveC0SemigroupFeller
public import MarkovProcess.Kernel.PositiveC0SemigroupKernel
public import MarkovProcess.Kernel.Resolvent
public import MarkovProcess.Kernel.ResolventUniqueness
public import MarkovProcess.Kernel.WeakConvergence
public import MarkovProcess.Killed.Kernel
public import MarkovProcess.Killed.ExitTimeIdentification
public import MarkovProcess.Killed.GluingPotential
public import MarkovProcess.Killed.GluingResolventEquation
public import MarkovProcess.Killed.GluingTransfer
public import MarkovProcess.Killed.GluingLocal
public import MarkovProcess.Killed.GluingMinimal
public import MarkovProcess.Killed.GluingLinearity
public import MarkovProcess.Killed.GluingRealResolvent
public import MarkovProcess.Killed.GluingMeasure
public import MarkovProcess.Killed.GluingC0
public import MarkovProcess.Killed.KillAtExit
public import MarkovProcess.Killed.Marginals
public import MarkovProcess.Killed.Minimal
public import MarkovProcess.Killed.Nested
public import MarkovProcess.Killed.Process
public import MarkovProcess.Killed.Resolvent
public import MarkovProcess.Killed.Semigroup
public import MarkovProcess.Lifetime.Basic
public import MarkovProcess.Lifetime.CountablySeparated
public import MarkovProcess.Lifetime.ExitTime
public import MarkovProcess.Lifetime.ExitTimeStopping
public import MarkovProcess.Lifetime.Filtration
public import MarkovProcess.Lifetime.Killing
public import MarkovProcess.Lifetime.Law
public import MarkovProcess.Lifetime.Nonexplosion
public import MarkovProcess.Lifetime.NonexplosiveTransport
public import MarkovProcess.Lifetime.Shift
public import MarkovProcess.Main
public import MarkovProcess.Parameterized.Annealed
public import MarkovProcess.Parameterized.CemeteryDenseTimeMarginals
public import MarkovProcess.Parameterized.CemeteryDenseTimeSupport
public import MarkovProcess.Parameterized.CemeterySemigroup
public import MarkovProcess.Parameterized.ContinuousProcess
public import MarkovProcess.Parameterized.ContinuousProcessProperties
public import MarkovProcess.Parameterized.DenseTimeConditionalKernel
public import MarkovProcess.Parameterized.DenseTimePrefixKernel
public import MarkovProcess.Parameterized.DenseTimeTrajectory
public import MarkovProcess.Parameterized.DenseTimeTrajectoryMarginals
public import MarkovProcess.Parameterized.Equivariance
public import MarkovProcess.Parameterized.FiniteTimeKernel
public import MarkovProcess.Parameterized.FiniteTimeProjectiveFamily
public import MarkovProcess.Parameterized.Killed
public import MarkovProcess.Parameterized.OrderedGrid
public import MarkovProcess.Parameterized.Semigroup
public import MarkovProcess.Path.Basic
public import MarkovProcess.Path.ClosedSetDetection
public import MarkovProcess.Path.DenseFiltration
public import MarkovProcess.Path.DenseRestrictionIntegral
public import MarkovProcess.Path.Exhaustion
public import MarkovProcess.Path.ExitTime
public import MarkovProcess.Path.ExitTimeShift
public import MarkovProcess.Path.KernelIdentification
public import MarkovProcess.Path.MeasureIdentification
public import MarkovProcess.Path.MixedFiniteMarginals
public import MarkovProcess.Path.OptionalStopping
public import MarkovProcess.Path.Polish
public import MarkovProcess.Path.Sampling
public import MarkovProcess.Path.RandomShiftMeasurability
public import MarkovProcess.Path.RandomTimeCompactTestConvergence
public import MarkovProcess.Path.RelativeHitting
public import MarkovProcess.Path.Shift
public import MarkovProcess.Path.ShiftCompactTestConvergence
public import MarkovProcess.Path.StoppedValueMeasurability
public import MarkovProcess.Path.Stopping
public import MarkovProcess.Path.StoppingTimeDyadicCeiling
public import MarkovProcess.Restart.ConditionalExpectation
public import MarkovProcess.Restart.ConditionalMarkov
public import MarkovProcess.Restart.CountableStoppingRestart
public import MarkovProcess.Restart.CountableStoppingRestartMeasure
public import MarkovProcess.Restart.FinitePastRestart
public import MarkovProcess.Restart.MixedPastFuture
public import MarkovProcess.Restart.RationalRestart
public import MarkovProcess.Restart.RationalRestrictedRestart
public import MarkovProcess.Restart.RestrictedRestartOfJoint
public import MarkovProcess.Semigroup.Basic
public import MarkovProcess.Semigroup.CompactStrongConvergence
public import MarkovProcess.Semigroup.ContractiveResolvent
public import MarkovProcess.Semigroup.DenseCoreConvergence
public import MarkovProcess.Semigroup.Duhamel
public import MarkovProcess.Semigroup.ExponentialBounds
public import MarkovProcess.Semigroup.ExponentialComparison
public import MarkovProcess.Semigroup.Generation
public import MarkovProcess.Semigroup.Generator
public import MarkovProcess.Semigroup.GeneratorClosed
public import MarkovProcess.Semigroup.GeneratorInjectivity
public import MarkovProcess.Semigroup.GeneratorResolvent
public import MarkovProcess.Semigroup.GeneratorUniqueness
public import MarkovProcess.Semigroup.InvariantSet
public import MarkovProcess.Semigroup.OrbitContinuity
public import MarkovProcess.Semigroup.OrbitProductRule
public import MarkovProcess.Semigroup.PoissonInvariant
public import MarkovProcess.Semigroup.PositiveShift
public import MarkovProcess.Semigroup.Resolvent
public import MarkovProcess.Semigroup.ResolventComparison
public import MarkovProcess.Semigroup.ResolventGeneration
public import MarkovProcess.Semigroup.StrongOperatorLimit
public import MarkovProcess.Semigroup.TrotterKato
public import MarkovProcess.Semigroup.YosidaApproximation
public import MarkovProcess.Semigroup.YosidaStrongLimit
public import MarkovProcess.Time.CountableDenseTime
public import MarkovProcess.Time.DenseTimeApproximationFromAbove
public import MarkovProcess.Time.DenseTimeHistory
public import MarkovProcess.Time.FiniteDenseApproximationOrdered
public import MarkovProcess.Time.FiniteGridIncrement
public import MarkovProcess.Time.FiniteOrderEmbedding
public import MarkovProcess.Time.FiniteOrderedTimes
public import MarkovProcess.Time.OrderedGrid
public import MarkovProcess.Trajectory.AllTimeFiniteMarginals
public import MarkovProcess.Trajectory.AllTimeMarginals
public import MarkovProcess.Trajectory.Basic
public import MarkovProcess.Trajectory.ClampedCoordinate
public import MarkovProcess.Trajectory.Convergence
public import MarkovProcess.Trajectory.CylinderAlgebra
public import MarkovProcess.Trajectory.DenseRestrictionIntegral
public import MarkovProcess.Trajectory.DenseRestrictionMarginals
public import MarkovProcess.Trajectory.DenseStoppingRestart
public import MarkovProcess.Trajectory.DiscountedDynkin
public import MarkovProcess.Trajectory.Dynkin
public import MarkovProcess.Trajectory.DynkinMartingale
public import MarkovProcess.Trajectory.DynkinStopping
public import MarkovProcess.Trajectory.Equivariance
public import MarkovProcess.Trajectory.ExcessiveStopping
public import MarkovProcess.Trajectory.ExitLaw
public import MarkovProcess.Trajectory.ExitTimeExponentialMoment
public import MarkovProcess.Trajectory.ExitTimeLaplace
public import MarkovProcess.Trajectory.ExpectedExitTime
public import MarkovProcess.Trajectory.FellerConditional
public import MarkovProcess.Trajectory.FellerCountableStoppingRestart
public import MarkovProcess.Trajectory.FellerFiniteMarginals
public import MarkovProcess.Trajectory.FellerRestrictedRestart
public import MarkovProcess.Trajectory.FellerShift
public import MarkovProcess.Trajectory.FellerStoppingConditional
public import MarkovProcess.Trajectory.FellerStoppingRestart
public import MarkovProcess.Trajectory.FeynmanKac
public import MarkovProcess.Trajectory.FeynmanKacFunctional
public import MarkovProcess.Trajectory.FeynmanKacRealResolvent
public import MarkovProcess.Trajectory.FeynmanKacResolvent
public import MarkovProcess.Trajectory.PenalizationDomination
public import MarkovProcess.Trajectory.FiniteMarginals
public import MarkovProcess.Trajectory.HarmonicRepresentation
public import MarkovProcess.Trajectory.PathModulus
public import MarkovProcess.Trajectory.PathTightness
public import MarkovProcess.Trajectory.RationalConditional
public import MarkovProcess.Trajectory.RationalShift
public import MarkovProcess.Trajectory.ResolventExitDecomposition
public import MarkovProcess.Trajectory.StartingPointContinuity
public import MarkovProcess.Trajectory.StoppingLtTop
public import MarkovProcess.Trajectory.WeakContinuity
public import MarkovProcess.Trajectory.WeakConvergence