One-dimensional marginals of the projective bridge

Restriction consistency identifies every strict prefix. The endpoint marginal has density p_a(x) p_{1-a}(-x) / p_1(0); reflection interchanges the two times.

noncomputable def BGW.StableTrees.BridgeOpen.prefix (a : ℝ) (ha1 : a < 1) (f : BridgeOpen) : Skorokhod.D a ℝ

A strict prefix of an open path, read from a sufficiently large coordinate.

Equations

• BGW.StableTrees.BridgeOpen.prefix a ha1 f = BGW.Skorokhod.restrict ⋯ (↑f (Nat.find ⋯))

theorem BGW.StableTrees.BridgeOpen.measurable_prefix (a : ℝ) (ha1 : a < 1) : Measurable («prefix» a ha1)

Strict-prefix restriction is measurable.

theorem BGW.StableTrees.BridgeOpen.prefix_eval (a : ℝ) (ha1 : a < 1) (f : BridgeOpen) (t : ↑(Set.Icc 0 a)) : («prefix» a ha1 f) t = f.eval ↑t

Prefix evaluation agrees with open evaluation.

theorem BGW.StableTrees.map_prefix_bridgeOpen {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (P : (a : ℝ) → MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)) (hP : ∀ (a : ℝ), 0 < a → a < 1 → IsStableLevyLaw θ a (P a)) (Q : MeasureTheory.ProbabilityMeasure BridgeOpen) (hQ : ∀ (n : ℕ), MeasureTheory.Measure.map (Skorokhod.CompatiblePaths.coord n) ↑Q = bridgePrefixLaw θ (bridgeHorizon n) ⋯ ↑(P (bridgeHorizon n))) {a : ℝ} (ha : 0 < a) (ha1 : a < 1) : MeasureTheory.Measure.map (BridgeOpen.prefix a ha1) ↑Q = bridgePrefixLaw θ a ⋯ ↑(P a)

Every strict prefix of an abstract projective bridge has the tilted law.

theorem BGW.StableTrees.map_endpoint_bridgePrefixLaw {θ a : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) : MeasureTheory.Measure.map (fun (f : Skorokhod.D a ℝ) => f ⟨a, ⋯⟩) (bridgePrefixLaw θ a ⋯ ↑P) = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (stableDensityAt θ a x) * ENNReal.ofReal (stableDensityAt θ (1 - a) (-x) / Scalar.stableDensity θ 0)

The endpoint marginal of a tilted prefix has the product of the two increment densities.

theorem BGW.StableTrees.bridgePrefix_endpoint_abs_tail_symm {θ a ε : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (ha : 0 < a) (ha1 : a < 1) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D a ℝ)} (hP : IsStableLevyLaw θ a P) {P' : MeasureTheory.ProbabilityMeasure (Skorokhod.D (1 - a) ℝ)} (hP' : IsStableLevyLaw θ (1 - a) P') : (bridgePrefixLaw θ a ⋯ ↑P) {f : Skorokhod.D a ℝ | ε < |f ⟨a, ⋯⟩|} = (bridgePrefixLaw θ (1 - a) ⋯ ↑P') {f : Skorokhod.D (1 - a) ℝ | ε < |f ⟨1 - a, ⋯⟩|}

One-dimensional endpoint reflection for complementary bridge times.