Law of the excursion straddling a fixed time

Predictable compensation and the passage potential identify the joint law of the start, lifetime and normalized shape. The normalized shape is independent of the first two coordinates, and the start has the generalized arcsine density.

References

J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapter IV.

theorem BGW.StableTrees.map_straddleData_eq_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (straddleData θ t) ↑(stableLocalLaw θ) = (straddleLaw θ t).prod ↑(unitExcursionLaw θ)

Joint law (path part): ((g_t, d_t - g_t), normalized straddling excursion) has the product law straddleLaw ⊗ unitExcursionLaw: the normalized excursion is independent of (g_t, d_t) with the unit excursion law, and (g_t, ζ_t) has the explicit density from compensation and the lifetime density.

theorem BGW.StableTrees.map_straddleAgeLife_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => (↑(straddleStart t f), straddleLife t f)) ↑(stableLocalLaw θ) = straddleLaw θ t

Law of (g_t, ζ_t) is straddleLaw.

theorem BGW.StableTrees.isProbabilityMeasure_straddleLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.IsProbabilityMeasure (straddleLaw θ t)

The claimed law of (g_t, ζ_t) is a probability measure (Beta integral).

theorem BGW.StableTrees.map_normalize_straddling_eq_unitExcursionLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => normalizeExc θ (straddlingExcursion t f)) ↑(stableLocalLaw θ) = ↑(unitExcursionLaw θ)

Blueprint statement: normalizeExc of the straddling excursion has the unit law.

theorem BGW.StableTrees.indepFun_straddle_age_shape {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : ProbabilityTheory.IndepFun (fun (f : Skorokhod.DLoc) => (↑(straddleStart t f), straddleLife t f)) (fun (f : Skorokhod.DLoc) => normalizeExc θ (straddlingExcursion t f)) ↑(stableLocalLaw θ)

Independence of (g_t, ζ_t) and the normalized straddling excursion.

theorem BGW.StableTrees.map_straddling_restrict_eq_levyExcLaw {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => excursionRestrict 1 (normalizeExc θ (straddlingExcursion t f))) ↑(stableLocalLaw θ) = ↑(levyExcLaw θ)

Path version: the normalized straddling excursion restricted to [0,1] has law levyExcLaw θ.

theorem BGW.StableTrees.map_straddleStart_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) : MeasureTheory.Measure.map (fun (f : Skorokhod.DLoc) => ↑(straddleStart t f)) ↑(stableLocalLaw θ) = MeasureTheory.volume.withDensity (straddleStartDensity θ t)

Generalized arcsine law of g_t: g_t/t ~ Beta(1/θ, 1-1/θ).