Residual and Gaussian-tilt lemmas for Brownian bridge prefixes

Measure-theoretic and Gaussian-process lemmas used to compare the bridge prefix law with Brownian motion: independence of an endpoint-adjusted residual from the endpoint, densities of a pair with an endpoint weight, and the Gaussian tilt identity for the prefix density (Gaussian conditioning as in D. Revuz and M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Springer, 1999, Chapter I).

theorem BGW.ContinuumTrees.BrownianD.map_withDensity_comp_snd {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) (F : Ω → α × β) (hF : Measurable F) (g : β → ENNReal) (hg : Measurable g) : MeasureTheory.Measure.map F (μ.withDensity fun (ω : Ω) => g (F ω).2) = (MeasureTheory.Measure.map F μ).withDensity fun (z : α × β) => g z.2

Reweighting by a function of the second coordinate commutes with pushforward along F.

theorem BGW.ContinuumTrees.BrownianD.map_withDensity_pair_indep {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y) (hXY : ProbabilityTheory.IndepFun X Y μ) (w : β → ENNReal) (hw : Measurable w) : MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) (μ.withDensity fun (ω : Ω) => w (Y ω)) = (MeasureTheory.Measure.map X μ).prod ((MeasureTheory.Measure.map Y μ).withDensity w)

Reweighting by a function of an independent coordinate keeps the pair law a product.

theorem BGW.ContinuumTrees.BrownianD.indepFun_residual_endpoint {Ω : Type u_1} {ι : Type u_2} {J : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω → ℝ} (hX : ProbabilityTheory.IsGaussianProcess X μ) (hmeas : ∀ (i : ι), Measurable (X i)) (u : J → ι) (e : ι) (l : J → ℝ) (hcov : ∀ (j : J), ProbabilityTheory.covariance (X (u j)) (X e) μ = l j * ProbabilityTheory.covariance (X e) (X e) μ) : ProbabilityTheory.IndepFun (fun (ω : Ω) (j : J) => X (u j) ω - l j * X e ω) (X e) μ

In a Gaussian process, the residual X (u j) - l j * X e is independent of X e whenever X e has covariance l j * Var (X e) with each X (u j).

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

The Gaussian tilt identity: the centered Gaussian density of variance c² a, multiplied by the explicit prefix density, is the centered Gaussian density of variance c² a (1 - a).