Brownian motion and bridge laws on Skorokhod space

The constructed Brownian motion and Brownian bridge are viewed as probability laws on the Skorokhod space through the continuous-path embedding. The bridge prefix law is compared with Brownian motion by its Gaussian density.

References

• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Sections 8 and 12.
• D. Revuz and M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Springer, 1999, Chapter I.

noncomputable def BGW.ContinuumTrees.BrownianD.brownianPath (T : ℝ) (ω : NNReal → ℝ) : C(↑(Set.Icc 0 T), ℝ)

Anchored Brownian path on [0,T] as a continuous function, from the constructed ProbabilityTheory.brownian.

Equations

• BGW.ContinuumTrees.BrownianD.brownianPath T ω = { toFun := fun (t : ↑(Set.Icc 0 T)) => ProbabilityTheory.brownian ⟨↑t, ⋯⟩ ω - ProbabilityTheory.brownian 0 ω, continuous_toFun := ⋯ }

theorem BGW.ContinuumTrees.BrownianD.measurable_ofContinuous {T : ℝ} : Measurable Skorokhod.ofContinuous

Continuous paths are Borel-measurably embedded in Skorokhod space.

theorem BGW.ContinuumTrees.BrownianD.measurable_restrict {T a : ℝ} (haT : a ≤ T) : Measurable (Skorokhod.restrict haT)

Restriction D T ℝ → D a ℝ is Borel measurable (both σ-algebras are generated by evaluations).

theorem BGW.ContinuumTrees.BrownianD.measurable_brownianPath (T : ℝ) : Measurable (brownianPath T)

The anchored Brownian path map is measurable.

noncomputable def BGW.ContinuumTrees.BrownianD.wienerPathLaw (c : NNReal) (T : ℝ) : MeasureTheory.ProbabilityMeasure C(↑(Set.Icc 0 T), ℝ)

The law of c · B on [0,T] in C([0,T], ℝ).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.ContinuumTrees.BrownianD.wienerD (c : NNReal) (T : ℝ) : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)

The law of c · B on [0,T] as a probability measure on D([0,T], ℝ): Brownian motion with variance c² t, pushed forward by ofContinuous.

Equations

• BGW.ContinuumTrees.BrownianD.wienerD c T = ⟨MeasureTheory.Measure.map BGW.Skorokhod.ofContinuous ↑(BGW.ContinuumTrees.BrownianD.wienerPathLaw c T), ⋯⟩

noncomputable def BGW.ContinuumTrees.BrownianD.bridgeD (c : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

The law of c · (standard Brownian bridge) on D([0,1], ℝ), pushed forward from BrownianBridge.law by scaling and ofContinuous.

Equations

• BGW.ContinuumTrees.BrownianD.bridgeD c = ⟨MeasureTheory.Measure.map (fun (g : C(↑unitInterval, ℝ)) => BGW.Skorokhod.ofContinuous (↑c • g)) ↑BGW.ContinuumTrees.BrownianBridge.law, ⋯⟩

theorem BGW.ContinuumTrees.BrownianD.coe_wienerD (c : NNReal) (T : ℝ) : ↑(wienerD c T) = MeasureTheory.Measure.map Skorokhod.ofContinuous ↑(wienerPathLaw c T)

The measure underlying wienerD is the stated continuous-path pushforward.

theorem BGW.ContinuumTrees.BrownianD.ae_mem_range_ofContinuous_wienerD (c : NNReal) (T : ℝ) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(wienerD c T), f ∈ Set.range Skorokhod.ofContinuous

The law is carried by continuous paths.

theorem BGW.ContinuumTrees.BrownianD.ae_eval_zero_wienerD (c : NNReal) {T : ℝ} (hT : 0 ≤ T) : ∀ᵐ (f : Skorokhod.D T ℝ) ∂↑(wienerD c T), f ⟨0, ⋯⟩ = 0

Brownian motion starts at zero.

theorem BGW.ContinuumTrees.BrownianD.isGaussianProcess_eval_wienerD (c : NNReal) (T : ℝ) : ProbabilityTheory.IsGaussianProcess (fun (t : ↑(Set.Icc 0 T)) (f : Skorokhod.D T ℝ) => f t) ↑(wienerD c T)

All finite-dimensional laws are centered Gaussian.

theorem BGW.ContinuumTrees.BrownianD.integral_eval_wienerD (c : NNReal) {T : ℝ} (t : ↑(Set.Icc 0 T)) : ∫ (f : Skorokhod.D T ℝ), f t ∂↑(wienerD c T) = 0

The law of the coordinate process on D is a centered Gaussian process.

theorem BGW.ContinuumTrees.BrownianD.covariance_eval_wienerD (c : NNReal) {T : ℝ} (s t : ↑(Set.Icc 0 T)) : ProbabilityTheory.covariance (fun (f : Skorokhod.D T ℝ) => f s) (fun (f : Skorokhod.D T ℝ) => f t) ↑(wienerD c T) = ↑c ^ 2 * min ↑s ↑t

Covariance c² min(s,t).

noncomputable def BGW.ContinuumTrees.BrownianD.variance (c : NNReal) (t : ℝ) : NNReal

Variance of the scaled Brownian motion at time t, with negative times truncated to zero.

Equations

• BGW.ContinuumTrees.BrownianD.variance c t = c ^ 2 * t.toNNReal

theorem BGW.ContinuumTrees.BrownianD.integral_exp_neg_eval_wienerD_sqrt_two {T : ℝ} (t : ↑(Set.Icc 0 T)) (l : ℝ) : ∫ (f : Skorokhod.D T ℝ), Real.exp (-l * f t) ∂↑(wienerD (NNReal.sqrt 2) T) = Real.exp (↑t * l ^ 2)

The √2 normalization has Laplace transform exp(t l²).

theorem BGW.ContinuumTrees.BrownianD.coe_bridgeD (c : NNReal) : ↑(bridgeD c) = MeasureTheory.Measure.map (fun (g : C(↑unitInterval, ℝ)) => Skorokhod.ofContinuous (↑c • g)) ↑BrownianBridge.law

The measure underlying bridgeD is the stated continuous-path pushforward.

theorem BGW.ContinuumTrees.BrownianD.ae_mem_range_ofContinuous_bridgeD (c : NNReal) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(bridgeD c), f ∈ Set.range Skorokhod.ofContinuous

The law is carried by continuous paths.

theorem BGW.ContinuumTrees.BrownianD.ae_endpoints_bridgeD (c : NNReal) : ∀ᵐ (f : Skorokhod.D 1 ℝ) ∂↑(bridgeD c), f ⟨0, ⋯⟩ = 0 ∧ f ⟨1, ⋯⟩ = 0

Both endpoints of the bridge vanish almost surely.

theorem BGW.ContinuumTrees.BrownianD.isGaussianProcess_eval_bridgeD (c : NNReal) : ProbabilityTheory.IsGaussianProcess (fun (t : ↑(Set.Icc 0 1)) (f : Skorokhod.D 1 ℝ) => f t) ↑(bridgeD c)

All finite dimensional bridge evaluations are centered Gaussian.

theorem BGW.ContinuumTrees.BrownianD.integral_eval_bridgeD (c : NNReal) (t : ↑(Set.Icc 0 1)) : ∫ (f : Skorokhod.D 1 ℝ), f t ∂↑(bridgeD c) = 0

Every bridge evaluation has mean zero.

theorem BGW.ContinuumTrees.BrownianD.covariance_eval_bridgeD (c : NNReal) (s t : ↑(Set.Icc 0 1)) : ProbabilityTheory.covariance (fun (f : Skorokhod.D 1 ℝ) => f s) (fun (f : Skorokhod.D 1 ℝ) => f t) ↑(bridgeD c) = ↑c ^ 2 * (min ↑s ↑t - ↑s * ↑t)

Covariance c² (min(s,t) - s t).

theorem BGW.ContinuumTrees.BrownianD.map_eval_bridgeD (c : NNReal) (t : ↑(Set.Icc 0 1)) : MeasureTheory.Measure.map (fun (f : Skorokhod.D 1 ℝ) => f t) ↑(bridgeD c) = ProbabilityTheory.gaussianReal 0 (c ^ 2 * ⟨↑t * (1 - ↑t), ⋯⟩)

Gaussian law of one bridge evaluation on Skorokhod space.

Prefix density of the bridge with respect to Brownian motion

noncomputable def BGW.ContinuumTrees.BrownianD.prefixDensity (c : NNReal) (a x : ℝ) : ℝ

The density p_{c²(1-a)}(-x) / p_{c²}(0) of the bridge prefix on [0,a] with respect to Brownian motion on [0,a], evaluated at the terminal value x = f(a).

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.ContinuumTrees.BrownianD.prefixDensity_eq {c : NNReal} (hc : c ≠ 0) {a : ℝ} (ha : a < 1) (x : ℝ) : prefixDensity c a x = (1 - a) ^ (-(1 / 2)) * Real.exp (-x ^ 2 / (2 * ↑c ^ 2 * (1 - a)))

Explicit form of the prefix density: (1-a)^{-1/2} exp (-x² / (2 c² (1-a))).

theorem BGW.ContinuumTrees.BrownianD.lintegral_prefixDensity_wienerD {c : NNReal} (hc : c ≠ 0) {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) : ∫⁻ (f : Skorokhod.D a ℝ), ENNReal.ofReal (prefixDensity c a (f ⟨a, ⋯⟩)) ∂↑(wienerD c a) = 1

The prefix density is a probability density for Brownian motion on [0,a].

theorem BGW.ContinuumTrees.BrownianD.map_restrict_bridgeD_eq_withDensity {c : NNReal} (hc : c ≠ 0) {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) : MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑(bridgeD c) = (↑(wienerD c a)).withDensity fun (f : Skorokhod.D a ℝ) => ENNReal.ofReal (prefixDensity c a (f ⟨a, ⋯⟩))

Bridge prefix density. For 0 ≤ a < 1, the law of the bridge restricted to [0,a] is absolutely continuous with respect to Brownian motion on [0,a], with density p_{c²(1-a)}(-X_a) / p_{c²}(0).

theorem BGW.ContinuumTrees.BrownianD.map_restrict_bridgeD_absolutelyContinuous {c : NNReal} (hc : c ≠ 0) {a : ℝ} (ha0 : 0 ≤ a) (ha1 : a < 1) : (MeasureTheory.Measure.map (Skorokhod.restrict ⋯) ↑(bridgeD c)).AbsolutelyContinuous ↑(wienerD c a)

Absolute continuity of the bridge prefix.