Documentation

BGW.StableTrees.MarkedExcursionsBasic

Marked excursions at passage jumps #

The marked measure associates each positive passage jump with its excursion cut. This module establishes its deterministic counting representation and excursion support.

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

source
noncomputable def BGW.StableTrees.jumpExcursion (x : NNReal) (f : Skorokhod.DLoc) :
Excursion

The excursion attached to the jump level x: the excursion cut excursionCut of f on (T_{x-}, T_x).

Equations
Instances For
    source
    noncomputable def BGW.StableTrees.excursionPointMeasure (f : Skorokhod.DLoc) :
    MeasureTheory.Measure (NNReal × Excursion)

    The marked excursion point measure on ℝ≥0 × Excursion: ∑_{x ∈ J f} δ_{(x, jumpExcursion x f)} (zero measure when J f is not countable).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGW.StableTrees.excursionPointMeasure_apply {f : Skorokhod.DLoc} (hf : (passageJumpSet f).Countable) {s : Set (NNReal × Excursion)} (hs : MeasurableSet s) :
      (excursionPointMeasure f) s = ↑{x : NNReal | x ∈ passageJumpSet f ∧ (x, jumpExcursion x f) ∈ s}.encard

      Counting-measure form (deterministic): when J f is countable, the mass of a measurable set is the number of jump levels whose marked point lies in it.

      source
      theorem BGW.StableTrees.ae_excursionPointMeasure_counting {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) :
      ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∃ (S : Set (NNReal × Excursion)), S.Countable ∧ excursionPointMeasure f = MeasureTheory.Measure.sum fun (p : ↑S) => MeasureTheory.Measure.dirac ↑p

      Counting measure (the counting field of IsTimeSimpleLevy): a.s. the point measure is the sum of unit Dirac masses at the points of a countable set, namely the marked points.

      source
      theorem BGW.StableTrees.excursionPointMeasure_atZero (f : Skorokhod.DLoc) :
      (excursionPointMeasure f) ({0} ×ˢ Set.univ) = 0

      No mass at label 0 (jump levels are positive).

      source
      theorem BGW.StableTrees.ae_excursionPointMeasure_singleton_prod {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) :
      ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x : NNReal) (A : Set Excursion), MeasurableSet A → (excursionPointMeasure f) ({x} ×ˢ A) = if x ∈ passageJumpSet f ∧ jumpExcursion x f ∈ A then 1 else 0

      Atoms: a.s., the label-x slice of a measurable mark set A has mass one iff x is a jump level whose excursion lies in A, and zero otherwise.

      source
      theorem BGW.StableTrees.ae_excursionPointMeasure_timeSimple {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) :
      ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s : NNReal), (excursionPointMeasure f) ({s} ×ˢ Set.univ) ≤ 1

      Time-simplicity (the timeSimple field of IsTimeSimpleLevy): a.s. at most one excursion per label (the labels are distinct points x, each carrying a single cut).