Documentation

BGW.StableTrees.HeightBridgesCompact

Compact prefix representatives for height approximations #

Constant extension supplies literal representatives on the compact prefix space. The definitions agree with the original observables on every local path.

source
def BGW.StableTrees.horizonExtension (T : NNReal) (f : Skorokhod.D ↑T ℝ) :
Skorokhod.DLoc

Constant extension of a compact prefix to a local càdlàg path.

Equations
Instances For
    source
    theorem BGW.StableTrees.measurable_horizonExtension (T : NNReal) :
    Measurable (horizonExtension T)

    Constant extension of a compact prefix is measurable.

    source
    theorem BGW.StableTrees.restrict_horizonExtension (T : NNReal) (f : Skorokhod.D ↑T ℝ) :
    Skorokhod.DLoc.restrict T (horizonExtension T f) = f

    Restricting the constant extension recovers the compact prefix.

    source
    noncomputable def BGW.StableTrees.horizonHeightApprox (ε : ℝ) (T : NNReal) (f : Skorokhod.D ↑T ℝ) :
    ℝ

    Compact-prefix representative of the height approximation.

    Equations
    Instances For
      source
      noncomputable def BGW.StableTrees.horizonHeight (θ : ℝ) (T : NNReal) (f : Skorokhod.D ↑T ℝ) :
      ℝ

      Compact-prefix representative of H02's chosen height.

      Equations
      Instances For
        source
        theorem BGW.StableTrees.measurable_horizonHeightApprox (ε : ℝ) (T : NNReal) :
        Measurable (horizonHeightApprox ε T)

        The compact approximation is measurable.

        source
        theorem BGW.StableTrees.measurable_horizonHeight (θ : ℝ) (T : NNReal) :
        Measurable (horizonHeight θ T)

        The compact height representative is measurable.

        source
        theorem BGW.StableTrees.horizonHeightApprox_restrict (ε : ℝ) (T : NNReal) (f : Skorokhod.DLoc) :
        horizonHeightApprox ε T (Skorokhod.DLoc.restrict T f) = heightApprox ε f T

        Restricting a local path preserves its compact approximation.

        source
        theorem BGW.StableTrees.horizonHeight_restrict (θ : ℝ) (T : NNReal) (f : Skorokhod.DLoc) :
        horizonHeight θ T (Skorokhod.DLoc.restrict T f) = height θ f T

        Restricting a local path preserves its compact H02 height.

        source
        theorem BGW.StableTrees.horizonHeightApprox_tendstoInMeasure {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) :
        MeasureTheory.TendstoInMeasure (MeasureTheory.Measure.map (Skorokhod.DLoc.restrict T) ↑(stableLocalLaw θ)) (fun (ε : ℝ) => horizonHeightApprox ε T) (nhdsWithin 0 (Set.Ioi 0)) (horizonHeight θ T)

        H02 convergence on the compact stable prefix law.