Brownian motion

In this file we define two predicates over stochastic processes X : ℝ≥0 → Ω → ℝ given a probability measure P : Measure Ω. IsPreBrownianReal X P means that X is a pre-Brownian motion. It means that it has the law of the Brownian motion, namely that its finite dimensional distributions are given by projectiveFamily. Then IsBrownianReal X P means that X is a Brownian motion, which means that it is a pre-Brownian motion with almost surely continuous paths.

We prove that a centered Gaussian process X with covariances given by cov[X s, X t; P] = min s t is a pre-Brownian motion and provide basic invariance properties. We also prove the weak Markov property: if B is a pre-Brownian motion and t₀ : ℝ≥0, then the process t ↦ B (t + t₀) - B t₀ is a pre-Brownian motion independent from (B t | t ≤ t₀).

Main definitions

• IsPreBrownianReal X P: A stochastic process is called pre-Brownian if its finite-dimensional laws are those of the Brownian motion, see projectiveFamily.
• IsBrownianReal X P: A stochastic process is called Brownian if its finite-dimensional laws are those of the Brownian motion, see IsPreBrownianReal, and if it has almost-surely continuous paths.

Main statements

• IsGaussianProcess.isPreBrownianReal_of_covariance: A centered Gaussian process with the right covariance is a pre-Brownian motion.
• HasIndepIncrements.isPreBrownianReal_of_hasLaw: A stochastic process X with independent increments and such that for all t, X t has law gaussianReal 0 t is a pre-Brownian motion.
• IsPreBrownianReal.indepFun_shift: The weak Markov property: If B is a pre-Brownian motion, then B (t₀ + t) - B t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀).

Tags

pre-Brownian motion, Brownian motion, Markov property

Pre-Brownian motion

structure ProbabilityTheory.IsPreBrownianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (P : MeasureTheory.Measure Ω := by volume_tac) : Prop

A stochastic process is called pre-Brownian if its finite-dimensional laws are those of the Brownian motion, see projectiveFamily.

Note: we name the constructor mk' so as to define later IsPreBrownianReal.mk, which to pre-Brownian motion will associate a continuous modification, in a way similar to AEMeasurable.mk.

• mk' :: (
• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => X x ω) (BrownianReal.projectiveFamily I) P
• )

theorem ProbabilityTheory.IsPreBrownianReal.congr {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} {C : NNReal → Ω → ℝ} (hB : IsPreBrownianReal B P) (h : ∀ (t : NNReal), B t =ᵐ[P] C t) : IsPreBrownianReal C P

theorem ProbabilityTheory.IsPreBrownianReal.isGaussianProcess {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) : IsGaussianProcess B P

theorem ProbabilityTheory.IsPreBrownianReal.aemeasurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t : NNReal) : AEMeasurable (B t) P

theorem ProbabilityTheory.IsPreBrownianReal.hasLaw_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t : NNReal) : HasLaw (B t) (gaussianReal 0 t) P

theorem ProbabilityTheory.IsPreBrownianReal.eval_zero_ae_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) : ∀ᵐ (ω : Ω) ∂P, B 0 ω = 0

theorem ProbabilityTheory.IsPreBrownianReal.hasLaw_sub {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (s t : NNReal) : HasLaw (B s - B t) (gaussianReal 0 (nndist ↑s ↑t)) P

theorem ProbabilityTheory.IsPreBrownianReal.integral_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t : NNReal) : ∫ (x : Ω), B t x ∂P = 0

theorem ProbabilityTheory.IsPreBrownianReal.integrable_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t : NNReal) : MeasureTheory.Integrable (B t) P

theorem ProbabilityTheory.IsPreBrownianReal.covariance_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (s t : NNReal) : covariance (B s) (B t) P = ↑(min s t)

theorem ProbabilityTheory.IsPreBrownianReal.covariance_fun_eval {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (s t : NNReal) : covariance (fun (ω : Ω) => B s ω) (fun (ω : Ω) => B t ω) P = ↑(min s t)

theorem ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covariance {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (h1 : IsGaussianProcess X P) (h2 : ∀ (t : NNReal), ∫ (x : Ω), X t x ∂P = 0) (h3 : ∀ (s t : NNReal), s ≤ t → covariance (X s) (X t) P = ↑s) : IsPreBrownianReal X P

A centered Gaussian process with the right covariance is a pre-Brownian motion.

theorem ProbabilityTheory.IsPreBrownianReal.hasIndepIncrements {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) : HasIndepIncrements B P

A pre-Brownian motion has independent increments.

theorem ProbabilityTheory.HasIndepIncrements.isPreBrownianReal_of_hasLaw {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (law : ∀ (t : NNReal), HasLaw (X t) (gaussianReal 0 t) P) (incr : HasIndepIncrements X P) : IsPreBrownianReal X P

A stochastic process X with independent increments and such that for all t, X t has law gaussianReal 0 t is a pre-Brownian motion.

theorem ProbabilityTheory.IsPreBrownianReal.neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) : IsPreBrownianReal (-B) P

theorem ProbabilityTheory.IsPreBrownianReal.smul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) {c : NNReal} (hc : c ≠ 0) : IsPreBrownianReal (fun (t : NNReal) (ω : Ω) => (√↑c)⁻¹ * B (c * t) ω) P

If B is a pre-Brownian motion and c > 0, then t ↦ (√c)⁻¹ B (c t) is a pre-Brownian motion.

theorem ProbabilityTheory.IsPreBrownianReal.shift {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t₀ : NNReal) : IsPreBrownianReal (fun (t : NNReal) (ω : Ω) => B (t₀ + t) ω - B t₀ ω) P

Weak Markov property: If B is a pre-Brownian motion, then t ↦ B (t₀ + t) - B t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀). This is the proof that it is pre-Brownian, see IsPreBrownianReal.indepFun_shift for independence.

theorem ProbabilityTheory.IsPreBrownianReal.indepFun_shift {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) (t₀ : NNReal) : IndepFun (fun (ω : Ω) (t : NNReal) => B (t₀ + t) ω - B t₀ ω) (fun (ω : Ω) (t : ↑(Set.Iic t₀)) => B (↑t) ω) P

Weak Markov property: If B is a pre-Brownian motion, then B (t₀ + t) - B t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀). This is the proof of independence, see IsPreBrownianReal.shift for the proof that it is pre-Brownian.

theorem ProbabilityTheory.IsPreBrownianReal.inv {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω} (hB : IsPreBrownianReal B P) : IsPreBrownianReal (fun (t : NNReal) (ω : Ω) => ↑t * B (1 / t) ω) P

If B is a pre-Brownian motion then t ↦ t * B (1 / t) is a pre-Brownian motion.

Brownian motion

structure ProbabilityTheory.IsBrownianReal {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : NNReal → Ω → ℝ) (P : MeasureTheory.Measure Ω := by volume_tac) extends ProbabilityTheory.IsPreBrownianReal X P : Prop

A stochastic process is called Brownian if its finite-dimensional laws are those of the Brownian motion, see IsPreBrownianReal, and if it has almost-surely continuous paths.

• hasLaw (I : Finset NNReal) : HasLaw (fun (ω : Ω) => I.restrict fun (x : NNReal) => X x ω) (BrownianReal.projectiveFamily I) P
• cont : ∀ᵐ (ω : Ω) ∂P, Continuous fun (x : NNReal) => X x ω

theorem ProbabilityTheory.IsBrownianReal.neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsBrownianReal B P) : IsBrownianReal (-B) P

theorem ProbabilityTheory.IsBrownianReal.smul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsBrownianReal B P) {c : NNReal} (hc : c ≠ 0) : IsBrownianReal (fun (t : NNReal) (ω : Ω) => (√↑c)⁻¹ * B (c * t) ω) P

If B is a Brownian motion and c > 0, then t ↦ (√c)⁻¹ B (c t) is a Brownian motion.

theorem ProbabilityTheory.IsBrownianReal.shift {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsBrownianReal B P) (t₀ : NNReal) : IsBrownianReal (fun (t : NNReal) (ω : Ω) => B (t₀ + t) ω - B t₀ ω) P

theorem ProbabilityTheory.IsBrownianReal.tendsto_nhds_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ} (hB : IsBrownianReal B P) : ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun (x : NNReal) => B x ω) (nhds 0) (nhds 0)