Documentation

BGW.StableTrees.PathTailReconstruction

Reconstruction of mesh increments from a compact step path #

Mesh evaluations recover every increment seen before the deterministic horizon. Unseen increments are set to minus one, so the reconstructed walk continues downwards.

source
noncomputable def BGW.StableTrees.PathTail.meshPoint (M : NNReal) (n k : ℕ) :
↑(Set.Icc 0 ↑M)

Mesh evaluation time, clipped to the source horizon for a total definition.

Equations
Instances For
    source
    noncomputable def BGW.StableTrees.PathTail.reconstructIncrements (M : NNReal) (n : ℕ) (b : ℝ) (y : Skorokhod.D ↑M ℝ) (i : ℕ) :
    ℝ

    Reconstruct the observed mesh increments and continue with minus-one increments.

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

      The reconstruction uses finitely many measurable evaluations.

      source
      theorem BGW.StableTrees.PathTail.reconstructIncrements_stepPath {M : NNReal} {n i : ℕ} {b : ℝ} (hn : 0 < n) (hb : b ≠ 0) (ω : ℕ → ℝ) (hi : i < ⌊↑n * ↑M⌋₊) :
      reconstructIncrements M n b (Skorokhod.realStepPath (↑M) n b ω) i = ω i

      Every increment observed before the horizon is recovered exactly when the scales are nonzero.

      source
      theorem BGW.StableTrees.PathTail.reconstructIncrements_skipFree {M : NNReal} {n : ℕ} {b : ℝ} (hb : n ≠ 0 → b ≠ 0) (ω : ℕ → ℝ) (hω : ∀ (i : ℕ), IsSkipFreeIncrement (ω i)) (i : ℕ) :
      IsSkipFreeIncrement (reconstructIncrements M n b (Skorokhod.realStepPath (↑M) n b ω) i)

      Reconstruction preserves skip-free increments on the image of a skip-free step path.

      source
      theorem BGW.StableTrees.PathTail.realStepPath_reconstructIncrements {M : NNReal} {n : ℕ} {b : ℝ} (hb : n ≠ 0 → b ≠ 0) (ω : ℕ → ℝ) :
      Skorokhod.realStepPath (↑M) n b (reconstructIncrements M n b (Skorokhod.realStepPath (↑M) n b ω)) = Skorokhod.realStepPath (↑M) n b ω

      Reconstructing the increments does not change the compact step path.

      source
      theorem BGW.StableTrees.PathTail.ae_reconstructIncrements (μ : PMF ℕ) (M : NNReal) (n : ℕ) (b : ℝ) (hb : n ≠ 0 → b ≠ 0) :
      ∀ᵐ (y : Skorokhod.D ↑M ℝ) ∂↑(stepPathLaw (realOffspringStepLaw μ) (↑M) (fun (x : ℕ) => b) n), Skorokhod.realStepPath (↑M) n b (reconstructIncrements M n b y) = y ∧ ∀ (i : ℕ), IsSkipFreeIncrement (reconstructIncrements M n b y i)

      The reconstructed sequence is skip-free and reproduces the source path almost surely under its actual iid step-path law.