Documentation

BGW.StableTrees.TailPairSelection

Reconstruction of the selected pair from a compact forest pair #

The walk determines the selected endpoints and cut. The height uses those same endpoints in the continuous host coordinate. No independent height or lifetime is introduced.

source
noncomputable def BGW.StableTrees.TailPair.extractedForestPair (M T : NNReal) (b : ℝ) (n : ℕ) (z : Skorokhod.D ↑M ℝ × C(↑(Set.Icc 0 ↑M), ℝ)) :
Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)

The selected closed-walk and centered-height pair reconstructed from a compact forest pair.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGW.StableTrees.TailPair.measurable_extractedForestPair (M T : NNReal) (b : ℝ) (n : ℕ) :
    Measurable (extractedForestPair M T b n)

    Reconstructing the selected pair is measurable.

    source
    def BGW.StableTrees.TailPair.selectionLocalEvent (M : NNReal) (b : ℝ) (n : ℕ) :
    Set (Skorokhod.D ↑M ℝ × C(↑(Set.Icc 0 ↑M), ℝ))

    The observable event that the reconstructed selected block ends within the observed mesh.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGW.StableTrees.TailPair.measurableSet_selectionLocalEvent (M : NNReal) (b : ℝ) (n : ℕ) :
      MeasurableSet (selectionLocalEvent M b n)

      The finite-mesh selection event is measurable.

      source
      theorem BGW.StableTrees.TailPair.cutHeightPath_forest_block (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (M T : NNReal) {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) (hdM : ↑(DiscreteForest.ladderTime ω (r + 1)) / ↑n ≤ ↑M) :
      cutHeightPath M T (DiscreteForest.forestHeightPath B n M ω) (↑(DiscreteForest.ladderTime ω r) / ↑n) (↑(DiscreteForest.ladderTime ω (r + 1)) / ↑n) = treeHeightPath B n T (DiscreteForest.blockLF ω r)

      The centered continuous cut of a forest block is exactly that block's tree height.

      source
      theorem BGW.StableTrees.TailPair.extractedForestPair_forestPairPath (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (hb : B n ≠ 0) (M T : NNReal) {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (hE : DiscreteForest.forestPairPath B n M ω ∈ selectionLocalEvent M (B n) n) :
      extractedForestPair M T (B n) n (DiscreteForest.forestPairPath B n M ω) = (Skorokhod.realStepPath (↑T) n (B n) (PathTail.closedTreeIncrementSeq (DiscreteForest.firstLongTree n ω)), treeHeightPath B n T (DiscreteForest.firstLongTree n ω))

      On a finite ladder forest whose reconstructed selection ends in the window, reconstruction recovers the pair of its first long tree, with the walk closed at its terminal step.