Uniqueness of measures from positive lifetime tail rectangles #
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.measure_eq_of_lifetime_tail_rectangles
{μ ν : MeasureTheory.Measure (↑(Set.Ioi 0) × Excursion)}
(hfin : ∀ (t : ↑(Set.Ioi 0)), μ (Set.Ioi t ×ˢ Set.univ) < ⊤)
(heq : ∀ (t : ↑(Set.Ioi 0)) (A : Set Excursion), MeasurableSet A → μ (Set.Ioi t ×ˢ A) = ν (Set.Ioi t ×ˢ A))
:
Finite positive tails suffice for uniqueness on lifetime/shape space.