forked from RemyDegenne/brownian-motion
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathBrownianMotion.lean
More file actions
64 lines (64 loc) · 2.91 KB
/
BrownianMotion.lean
File metadata and controls
64 lines (64 loc) · 2.91 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
import BrownianMotion.Auxiliary.Adapted
import BrownianMotion.Auxiliary.Algebra
import BrownianMotion.Auxiliary.Analysis
import BrownianMotion.Auxiliary.ContinuousBilinForm
import BrownianMotion.Auxiliary.ENNReal
import BrownianMotion.Auxiliary.Filtration
import BrownianMotion.Auxiliary.FiniteInf
import BrownianMotion.Auxiliary.HasGaussianLaw
import BrownianMotion.Auxiliary.HasLaw
import BrownianMotion.Auxiliary.IsStoppingTime
import BrownianMotion.Auxiliary.Jensen
import BrownianMotion.Auxiliary.LinearAlgebra
import BrownianMotion.Auxiliary.Martingale
import BrownianMotion.Auxiliary.MeanInequalities
import BrownianMotion.Auxiliary.MeasureTheory
import BrownianMotion.Auxiliary.Metric
import BrownianMotion.Auxiliary.NNReal
import BrownianMotion.Auxiliary.Nat
import BrownianMotion.Auxiliary.Real
import BrownianMotion.Auxiliary.SetAlgebra
import BrownianMotion.Auxiliary.StoppedProcess
import BrownianMotion.Auxiliary.Topology
import BrownianMotion.Auxiliary.WithLp
import BrownianMotion.Auxiliary.WithTop
import BrownianMotion.Choquet.AnalyticSet
import BrownianMotion.Choquet.Capacity
import BrownianMotion.Choquet.CompactSystem
import BrownianMotion.Continuity.Chaining
import BrownianMotion.Continuity.CoveringNumber
import BrownianMotion.Continuity.HasBoundedInternalCoveringNumber
import BrownianMotion.Continuity.IsKolmogorovProcess
import BrownianMotion.Continuity.KolmogorovChentsov
import BrownianMotion.Continuity.KolmogorovChentsovInequality
import BrownianMotion.Debut.Approximation
import BrownianMotion.Debut.Basic
import BrownianMotion.Gaussian.BrownianMotion
import BrownianMotion.Gaussian.CovMatrix
import BrownianMotion.Gaussian.Gaussian
import BrownianMotion.Gaussian.GaussianProcess
import BrownianMotion.Gaussian.Moment
import BrownianMotion.Gaussian.MultivariateGaussian
import BrownianMotion.Gaussian.ProjectiveLimit
import BrownianMotion.Gaussian.StochasticProcesses
import BrownianMotion.StochasticIntegral.ApproxSeq
import BrownianMotion.StochasticIntegral.Cadlag
import BrownianMotion.StochasticIntegral.Centering
import BrownianMotion.StochasticIntegral.ClassD
import BrownianMotion.StochasticIntegral.DoobLp
import BrownianMotion.StochasticIntegral.DoobMeyer
import BrownianMotion.StochasticIntegral.Komlos
import BrownianMotion.StochasticIntegral.L2M
import BrownianMotion.StochasticIntegral.LocalMartingale
import BrownianMotion.StochasticIntegral.LocalMonad
import BrownianMotion.StochasticIntegral.LocalizingSequence
import BrownianMotion.StochasticIntegral.Locally
import BrownianMotion.StochasticIntegral.MathlibImports
import BrownianMotion.StochasticIntegral.OptionalSampling
import BrownianMotion.StochasticIntegral.Predictable
import BrownianMotion.StochasticIntegral.QuadraticVariation
import BrownianMotion.StochasticIntegral.SimpleProcess
import BrownianMotion.StochasticIntegral.SquareIntegrable
import BrownianMotion.StochasticIntegral.UniformIntegrable
import BrownianMotion.Verso.Brownian
import BrownianMotion.Verso.Processes