Documentation

BGW.StableTrees.DiscreteHeightApproxFiniteOccupation

Finite-path occupation observables #

Constant extension past the terminal endpoint lets the finite-horizon occupation functional use the sealed local-path height approximation.

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

Extend a compact path constantly beyond its terminal endpoint.

Equations
Instances For
    source
    theorem BGW.StableTrees.DiscreteHeightApprox.extendFinitePath_apply (T : NNReal) (f : Skorokhod.D ↑T ℝ) (u : NNReal) (hu : u ≤ T) :
    ↑(extendFinitePath T f) u = f ⟨↑u, ⋯⟩

    Constant extension agrees with the finite path before its terminal endpoint.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.measurable_extendFinitePath (T : NNReal) :
    Measurable (extendFinitePath T)

    Constant extension is measurable for the evaluation sigma-algebra.

    source
    theorem BGW.StableTrees.DiscreteHeightApprox.futureInf_extendFinitePath (T : NNReal) (f : Skorokhod.D ↑T ℝ) {s t : NNReal} (hst : s ≤ t) (ht : t ≤ T) :
    futureInf (extendFinitePath T f) t s = Skorokhod.windowInf f ⋯ hst ht

    The future infimum of a constant extension is the finite window infimum.

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

    The sealed occupation approximation applied to the constant extension of a finite path.

    Equations
    Instances For
      source
      theorem BGW.StableTrees.DiscreteHeightApprox.measurable_finiteHeightApprox (T t : NNReal) (ε : ℝ) :
      Measurable (finiteHeightApprox T t ε)

      Finite-path occupation observables are measurable.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.continuousAt_extended_gap (T : NNReal) {s t : NNReal} (hst : s ≤ t) (ht : t ≤ T) {f : Skorokhod.D ↑T ℝ} (hsf : ContinuousAt ⇑f ⟨↑s, ⋯⟩) (htf : t = T ∨ ContinuousAt ⇑f ⟨↑t, ⋯⟩) :
      ContinuousAt (fun (g : Skorokhod.D ↑T ℝ) => ↑(extendFinitePath T g) s - futureInf (extendFinitePath T g) t s) f

      The finite-path gap is continuous at a path continuous at the two window endpoints.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.futureInf_eq_of_prefix {f g : Skorokhod.DLoc} {t s : NNReal} (he : ∀ u ≤ t, ↑f u = ↑g u) :
      futureInf f t s = futureInf g t s

      Prefix agreement determines the future infimum at all earlier times.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.heightApprox_eq_of_prefix {f g : Skorokhod.DLoc} {t : NNReal} (he : ∀ u ≤ t, ↑f u = ↑g u) (ε : ℝ) :
      heightApprox ε f t = heightApprox ε g t

      Prefix agreement determines the fixed-time occupation approximation.

      source
      theorem BGW.StableTrees.DiscreteHeightApprox.finiteHeightApprox_restrict (T t : NNReal) (ht : t ≤ T) (ε : ℝ) (f : Skorokhod.DLoc) :
      finiteHeightApprox T t ε (Skorokhod.DLoc.restrict T f) = heightApprox ε f t

      Extending a restriction preserves all occupations before that restriction endpoint.