Documentation

BGW.ContinuumTrees.BrownianBridge

A continuous Brownian bridge law #

The source probability space and Brownian motion are the actual constructions ProbabilityTheory.gaussianLimit and ProbabilityTheory.brownian supplied by the pinned BrownianMotion dependency. No existence assumption on a process is required here.

The path is anchored as B t - B 0 - t * (B 1 - B 0). Its two endpoint values are zero for every outcome, including exceptional outcomes for which B 0 need not vanish. Its measurable pushforward to C(unitInterval, ℝ) is a probability law with centered Gaussian finite-dimensional distributions and covariance min s t - s * t.

source
def BGW.ContinuumTrees.BrownianBridge.time (t : ↑unitInterval) :
NNReal

A unit-interval time viewed as a nonnegative real Brownian time.

Equations
Instances For
    source
    @[simp]
    theorem BGW.ContinuumTrees.BrownianBridge.coe_time (t : ↑unitInterval) :
    ↑(time t) = ↑t
    source
    @[simp]
    theorem BGW.ContinuumTrees.BrownianBridge.time_zero :
    time 0 = 0
    source
    @[simp]
    theorem BGW.ContinuumTrees.BrownianBridge.time_one :
    time 1 = 1
    source
    theorem BGW.ContinuumTrees.BrownianBridge.continuous_time :
    Continuous time
    source
    noncomputable def BGW.ContinuumTrees.BrownianBridge.path (ω : NNReal → ℝ) :
    C(↑unitInterval, ℝ)

    The anchored continuous path obtained from the constructed Brownian motion.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem BGW.ContinuumTrees.BrownianBridge.path_apply (ω : NNReal → ℝ) (t : ↑unitInterval) :
      (path ω) t = ProbabilityTheory.brownian (time t) ω - ProbabilityTheory.brownian 0 ω - ↑t * (ProbabilityTheory.brownian 1 ω - ProbabilityTheory.brownian 0 ω)
      source
      theorem BGW.ContinuumTrees.BrownianBridge.path_zero (ω : NNReal → ℝ) :
      (path ω) 0 = 0
      source
      theorem BGW.ContinuumTrees.BrownianBridge.path_one (ω : NNReal → ℝ) :
      (path ω) 1 = 0
      source
      theorem BGW.ContinuumTrees.BrownianBridge.measurable_path :
      Measurable path

      Measurability is for the Borel structure of the continuous-path space.

      source
      noncomputable def BGW.ContinuumTrees.BrownianBridge.law :
      MeasureTheory.ProbabilityMeasure C(↑unitInterval, ℝ)

      The genuine pushforward of the constructed Brownian probability measure.

      Equations
      Instances For
        source
        @[simp]
        theorem BGW.ContinuumTrees.BrownianBridge.coe_law :
        ↑law = MeasureTheory.Measure.map path ProbabilityTheory.gaussianLimit
        source
        theorem BGW.ContinuumTrees.BrownianBridge.law_apply {A : Set C(↑unitInterval, ℝ)} (hA : MeasurableSet A) :
        ↑law A = ProbabilityTheory.gaussianLimit (path ⁻¹' A)
        source
        theorem BGW.ContinuumTrees.BrownianBridge.hasLaw_path :
        ProbabilityTheory.HasLaw path (↑law) ProbabilityTheory.gaussianLimit
        source
        theorem BGW.ContinuumTrees.BrownianBridge.ae_endpoints :
        ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, f 0 = 0 ∧ f 1 = 0

        The continuous bridge law is concentrated on paths with both endpoints zero.

        source
        theorem BGW.ContinuumTrees.BrownianBridge.isGaussianProcess_path :
        ProbabilityTheory.IsGaussianProcess (fun (t : ↑unitInterval) (ω : NNReal → ℝ) => (path ω) t) ProbabilityTheory.gaussianLimit

        Each path evaluation is a finite linear combination of Brownian evaluations.

        source
        theorem BGW.ContinuumTrees.BrownianBridge.isGaussianProcess_eval :
        ProbabilityTheory.IsGaussianProcess (fun (t : ↑unitInterval) (f : C(↑unitInterval, ℝ)) => f t) ↑law

        All finite-dimensional distributions under the constructed path law are Gaussian.

        source
        theorem BGW.ContinuumTrees.BrownianBridge.integrable_eval (t : ↑unitInterval) :
        MeasureTheory.Integrable (fun (f : C(↑unitInterval, ℝ)) => f t) ↑law

        Evaluation integrability follows from the proved Gaussian finite-dimensional laws.

        source
        theorem BGW.ContinuumTrees.BrownianBridge.integral_path (t : ↑unitInterval) :
        ∫ (ω : NNReal → ℝ), (path ω) t ∂ProbabilityTheory.gaussianLimit = 0
        source
        theorem BGW.ContinuumTrees.BrownianBridge.integral_eval (t : ↑unitInterval) :
        ∫ (f : C(↑unitInterval, ℝ)), f t ∂↑law = 0

        Every evaluation has mean zero under the actual bridge law.

        source
        theorem BGW.ContinuumTrees.BrownianBridge.covariance_path (s t : ↑unitInterval) :
        ProbabilityTheory.covariance (fun (ω : NNReal → ℝ) => (path ω) s) (fun (ω : NNReal → ℝ) => (path ω) t) ProbabilityTheory.gaussianLimit = min ↑s ↑t - ↑s * ↑t
        source
        theorem BGW.ContinuumTrees.BrownianBridge.covariance_eval (s t : ↑unitInterval) :
        ProbabilityTheory.covariance (fun (f : C(↑unitInterval, ℝ)) => f s) (fun (f : C(↑unitInterval, ℝ)) => f t) ↑law = min ↑s ↑t - ↑s * ↑t

        The standard unit-bridge covariance, transported through the genuine measurable path map.