Documentation

BGW.StableTrees.StraddlingExcursionBasic

The excursion straddling a fixed time #

Extraction of the passage jump containing a fixed positive time, with its lifetime, normalized path and measurable data.

References #

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

Definitions #

source
noncomputable def BGW.StableTrees.straddleStart (t : NNReal) (f : Skorokhod.DLoc) :
NNReal

Start g_t = T_{L_t -} of the excursion straddling t.

Equations
Instances For
    source
    noncomputable def BGW.StableTrees.straddleEnd (t : NNReal) (f : Skorokhod.DLoc) :
    NNReal

    End d_t = T_{L_t} of the excursion straddling t.

    Equations
    Instances For
      source
      noncomputable def BGW.StableTrees.straddleLife (t : NNReal) (f : Skorokhod.DLoc) :
      ℝ

      Lifetime ζ_t = d_t - g_t as a real number.

      Equations
      Instances For
        source
        noncomputable def BGW.StableTrees.straddlingExcursion (t : NNReal) (f : Skorokhod.DLoc) :
        Excursion

        The excursion of X - I straddling t: the cut of f at the jump level L_t.

        Equations
        Instances For
          source
          noncomputable def BGW.StableTrees.straddleDensity (θ : ℝ) (t : NNReal) (p : ℝ × ℝ) :
          ENNReal

          Claimed density of (g_t, ζ_t) on ℝ × ℝ: straddleAgeDensity g * lifetimeDensity ζ on {0 < g < t < g + ζ}.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def BGW.StableTrees.straddleLaw (θ : ℝ) (t : NNReal) :
            MeasureTheory.Measure (ℝ × ℝ)

            The claimed law of (g_t, ζ_t).

            Equations
            Instances For
              source
              noncomputable def BGW.StableTrees.straddleStartDensity (θ : ℝ) (t : NNReal) (g : ℝ) :
              ENNReal

              Claimed density of g_t on ℝ: g^{α-1} (t-g)^{-α} / (Γ(α) Γ(1-α)) on (0, t).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def BGW.StableTrees.straddleData (θ : ℝ) (t : NNReal) (f : Skorokhod.DLoc) :
                (ℝ × ℝ) × Excursion

                Joint data: ((g_t, ζ_t), normalized straddling excursion).

                Equations
                Instances For
                  source
                  theorem BGW.StableTrees.ae_straddle_spec {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) :
                  ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), localTimeNN f t ∈ passageJumpSet f ∧ straddleStart t f < t ∧ t < straddleEnd t f ∧ 0 < ↑(reflectedFrom 0 f) t ∧ cutValid (straddleStart t f) (straddleEnd t f) f ∧ ↑(straddlingExcursion t f).lifetime = straddleLife t f ∧ ∀ x ∈ passageJumpSet f, t ∈ Set.Ioo (passageTimeMinus x f) (passageTime x f) → x = localTimeNN f t

                  Straddling excursion, a.s. facts (g_t < t < d_t, unique straddling jump level, valid cut, lifetime tag d_t - g_t, and R_t > 0 for R = X - I).

                  source
                  theorem BGW.StableTrees.aemeasurable_straddleData {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) :
                  AEMeasurable (straddleData θ t) ↑(stableLocalLaw θ)

                  The joint data of the straddling excursion is AEMeasurable (needed for Measure.map).

                  source
                  theorem BGW.StableTrees.aemeasurable_straddlingExcursion {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) :
                  AEMeasurable (straddlingExcursion t) ↑(stableLocalLaw θ)

                  The straddling excursion itself is AEMeasurable.

                  source
                  theorem BGW.StableTrees.ae_straddle_zero_description {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) :
                  ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), straddleStart t f = sSup {s : NNReal | s ≤ t ∧ ↑(reflectedFrom 0 f) s = 0} ∧ straddleEnd t f = sInf {s : NNReal | t < s ∧ ↑(reflectedFrom 0 f) s = 0}

                  g_t and d_t as last/first zero of the reflected process around t (R = X - I = reflectedFrom 0 f; g_t = sup{s ≤ t : R_s = 0}, d_t = inf{s > t : R_s = 0}).

                  source
                  theorem BGW.StableTrees.ae_normalize_straddling_path {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) :
                  ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (s : NNReal), ↑(normalizeExc θ (straddlingExcursion t f)).path s = straddleLife t f ^ (-(1 / θ)) * (↑f (min (straddleStart t f + (straddleEnd t f - straddleStart t f) * s) (straddleEnd t f)) - ↑f (straddleStart t f))

                  Chaumont's path formula (unnormalized X): a.s. the normalized straddling excursion is s ↦ ζ_t^{-1/θ} (X_{min(g_t + ζ_t s, d_t)} - X_{g_t}).