Nondegenerate increments of the constructed Brownian bridge

An evaluation difference has variance d * (1 - d), where d is the distance between its two unit-interval times. For 0 < d < 1 its Gaussian law has no atoms. The exclusions are essential: equal times and the pair of endpoints both give a deterministic zero difference.

theorem BGW.ContinuumTrees.BrownianBridge.hasGaussianLaw_eval_sub (s t : ↑unitInterval) : ProbabilityTheory.HasGaussianLaw (fun (f : C(↑unitInterval, ℝ)) => f s - f t) ↑law

Differences of evaluations are Gaussian under the actual continuous bridge law.

theorem BGW.ContinuumTrees.BrownianBridge.integral_eval_sub (s t : ↑unitInterval) : ∫ (f : C(↑unitInterval, ℝ)), f s - f t ∂↑law = 0

theorem BGW.ContinuumTrees.BrownianBridge.variance_eval (s : ↑unitInterval) : ProbabilityTheory.variance (fun (f : C(↑unitInterval, ℝ)) => f s) ↑law = ↑s - ↑s * ↑s

The variance of an individual bridge evaluation.

theorem BGW.ContinuumTrees.BrownianBridge.variance_eval_sub (s t : ↑unitInterval) : ProbabilityTheory.variance (fun (f : C(↑unitInterval, ℝ)) => f s - f t) ↑law = |↑s - ↑t| * (1 - |↑s - ↑t|)

The increment variance includes the endpoint degeneracy at distance one.

theorem BGW.ContinuumTrees.BrownianBridge.variance_eval_sub_pos (s t : ↑unitInterval) (hzero : 0 < |↑s - ↑t|) (hone : |↑s - ↑t| < 1) : 0 < ProbabilityTheory.variance (fun (f : C(↑unitInterval, ℝ)) => f s - f t) ↑law

Every increment at a nonzero distance strictly below one has positive variance.

theorem BGW.ContinuumTrees.BrownianBridge.measure_eval_sub_eq_zero (s t : ↑unitInterval) (hzero : 0 < |↑s - ↑t|) (hone : |↑s - ↑t| < 1) (a : ℝ) : ↑law {f : C(↑unitInterval, ℝ) | f s - f t = a} = 0

Nondegenerate bridge increments have zero mass at each real value.

theorem BGW.ContinuumTrees.BrownianBridge.ae_eval_ne (s t : ↑unitInterval) (hzero : 0 < |↑s - ↑t|) (hone : |↑s - ↑t| < 1) : ∀ᵐ (f : C(↑unitInterval, ℝ)) ∂↑law, f s ≠ f t

Two bridge values at nondegenerate time separation are almost surely distinct.