Reversal of tilted bridge prefixes

Reversing the increments of a strict prefix preserves its tilted law, since the tilt depends only on its endpoint. This reversal is centered at the prefix endpoint.

theorem BGW.StableTrees.bridgePrefixLaw_absolutelyContinuous (θ a : ℝ) (ha : 0 ≤ a) (P : MeasureTheory.Measure (Skorokhod.D a ℝ)) : (bridgePrefixLaw θ a ha P).AbsolutelyContinuous P

The bridge prefix is absolutely continuous with respect to its underlying path law.

theorem BGW.StableTrees.bridgePrefixLaw_ae_zero {θ a : ℝ} (ha : 0 ≤ a) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) : ∀ᵐ (f : Skorokhod.D a ℝ) ∂bridgePrefixLaw θ a ha ↑P, f ⟨0, ⋯⟩ = 0

A bridge prefix starts at zero almost surely.

theorem BGW.StableTrees.bridgeOpenLaw_ae_zero {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : BridgeOpen) ∂↑(bridgeOpenLaw θ), f.eval 0 = 0

The open stable bridge starts at zero almost surely.

theorem BGW.StableTrees.map_reverseIncrements_bridgePrefixLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) : MeasureTheory.Measure.map (Skorokhod.reverseIncrements ⋯) (bridgePrefixLaw θ a ⋯ ↑P) = bridgePrefixLaw θ a ⋯ ↑P

Reversal centered at the prefix endpoint preserves the tilted prefix law.