Identification of the unit prefix law at good horizons

The candidate is normalized before finite-dimensional uniqueness is used. The dense evaluation set contains the terminal coordinate.

References

• L. Chaumont, Excursion normalisée, méandre et pont pour les processus de Lévy stables, Bull. Sci. Math. 121 (1997), 377–403.

theorem BGW.StableTrees.integral_goodTimes_eq_prefixDensityMeasure_fintype {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : b ∈ Set.Ioo 0 1) (hbgood : NoFixedJumpUnit θ b) {I : Type u_1} [Fintype I] (t : I → NNReal) (ht : ∀ (i : I), t i ≤ b) (hgood : ∀ (i : I), NoFixedJumpUnit θ (t i)) (φ : (I → ℝ) → ℝ) (hφ : Continuous φ) (hφb : ∃ (C : ℝ), ∀ (x : I → ℝ), |φ x| ≤ C) : ∫ (e : Excursion), φ fun (i : I) => ↑e.path (t i) ∂↑(unitExcursionLaw θ) = (Scalar.stableDensity θ 0)⁻¹ * ∫ (e : Excursion), φ fun (i : I) => ↑e.path (t i) ∂prefixDensityMeasure θ b

Reindexing the good-time cylinder identity by an arbitrary finite type.

theorem BGW.StableTrees.levyExcLaw_prefix_density_of_good {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (b : NNReal) (hb : b ∈ Set.Ioo 0 1) (hbgood : NoFixedJumpUnit θ b) : unitPrefix θ b = (ENNReal.ofReal (Scalar.stableDensity θ 0))⁻¹ • MeasureTheory.Measure.map (excursionRestrict b) (prefixDensityMeasure θ b)

At a good horizon, normalized Kendall weighting gives the unit prefix law.