Regression on a Brownian bridge increment

Subtracting the covariance profile times one increment leaves zero covariance with that increment at every time. The profile is explicit on the intervals before and after the increment, which will separate their minimum values. The normalized identities retain nondegeneracy of the increment. Joint Gaussianity then proves independence of the continuous residual path and the increment, using exactly the sigma-algebra generated by path evaluations. Uniqueness of minima is a later probability result.

theorem BGW.ContinuumTrees.BrownianBridge.covariance_eval_increment (s b c : ↑unitInterval) : ProbabilityTheory.covariance (fun (f : C(↑unitInterval, ℝ)) => f s) (fun (f : C(↑unitInterval, ℝ)) => f c - f b) ↑law = min ↑s ↑c - min ↑s ↑b - ↑s * (↑c - ↑b)

Covariance with an increment, computed under the actual bridge law.

noncomputable def BGW.ContinuumTrees.BrownianBridge.regressionProfile (b c : ↑unitInterval) : C(↑unitInterval, ℝ)

The continuous covariance profile. Normalized regression is used only when 0 < c - b < 1; the formula itself is total at other parameters.

Equations

• BGW.ContinuumTrees.BrownianBridge.regressionProfile b c = { toFun := fun (s : ↑unitInterval) => (min ↑s ↑c - min ↑s ↑b - ↑s * (↑c - ↑b)) / ((↑c - ↑b) * (1 - (↑c - ↑b))), continuous_toFun := ⋯ }

@[simp]

theorem BGW.ContinuumTrees.BrownianBridge.regressionProfile_apply (b c s : ↑unitInterval) : (regressionProfile b c) s = (min ↑s ↑c - min ↑s ↑b - ↑s * (↑c - ↑b)) / ((↑c - ↑b) * (1 - (↑c - ↑b)))

theorem BGW.ContinuumTrees.BrownianBridge.regressionProfile_of_le (b c s : ↑unitInterval) (hbc : b < c) (hshort : ↑c - ↑b < 1) (hs : s ≤ b) : (regressionProfile b c) s = -↑s / (1 - (↑c - ↑b))

Before the increment, the regression profile is nonpositive and linear in time.

theorem BGW.ContinuumTrees.BrownianBridge.regressionProfile_of_ge (b c s : ↑unitInterval) (hbc : b < c) (hshort : ↑c - ↑b < 1) (hs : c ≤ s) : (regressionProfile b c) s = (1 - ↑s) / (1 - (↑c - ↑b))

After the increment, the profile is nonnegative and linear in the time remaining.

noncomputable def BGW.ContinuumTrees.BrownianBridge.regressionResidual (b c : ↑unitInterval) (f : C(↑unitInterval, ℝ)) : C(↑unitInterval, ℝ)

Remove the chosen increment times its covariance profile from a continuous path.

Equations

• BGW.ContinuumTrees.BrownianBridge.regressionResidual b c f = f - (f c - f b) • BGW.ContinuumTrees.BrownianBridge.regressionProfile b c

theorem BGW.ContinuumTrees.BrownianBridge.continuous_regressionResidual (b c : ↑unitInterval) : Continuous (regressionResidual b c)

theorem BGW.ContinuumTrees.BrownianBridge.covariance_regressionResidual_increment (b c s : ↑unitInterval) (hbc : b < c) (hshort : ↑c - ↑b < 1) : ProbabilityTheory.covariance (fun (f : C(↑unitInterval, ℝ)) => (regressionResidual b c f) s) (fun (f : C(↑unitInterval, ℝ)) => f c - f b) ↑law = 0

The residual has zero covariance with the increment at each fixed time.

theorem BGW.ContinuumTrees.BrownianBridge.indepFun_regressionResidual_increment (b c : ↑unitInterval) (hbc : b < c) (hshort : ↑c - ↑b < 1) : ProbabilityTheory.IndepFun (regressionResidual b c) (fun (f : C(↑unitInterval, ℝ)) => f c - f b) ↑law

The whole continuous residual path is independent of the chosen increment.