Documentation

BGW.StableTrees.WalkPassageBasic

First passage of the canonical offspring walk #

The weak downward hitting time of the canonical real walk is identified with the Łukasiewicz code of a finite forest. Criticality makes the hitting time almost surely finite. The step-path formulation is deterministic and is the input to the functional stable limit theorem (J. H. B. Kemperman, The Passage Problem for a Stationary Markov Chain, University of Chicago Press, 1961; J. Pitman, Combinatorial Stochastic Processes, Springer, 2006, Section 6.1).

source
noncomputable def BGW.StableTrees.walkHitTime (ℓ : ℕ) (w : ℕ → ℝ) :
ℕ∞

The first (weak) hit of (-∞, -ℓ] by the walk k ↦ partialSum w k; ⊤ if never.

Equations
Instances For
    source
    noncomputable def BGW.StableTrees.walkPassageLaw (μ : PMF ℕ) (ℓ n : ℕ) :
    MeasureTheory.Measure ℝ

    The law of walkHitTime ℓ / n for the canonical offspring walk (finite reading).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGW.StableTrees.measurable_walkHitTime (ℓ : ℕ) :
      Measurable (walkHitTime ℓ)
      source
      theorem BGW.StableTrees.ae_step_ge_neg_one (μ : PMF ℕ) :
      ∀ᵐ (w : ℕ → ℝ) ∂↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ)), ∀ (i : ℕ), ∃ (k : ℕ), w i = ↑k - 1

      Almost surely the canonical walk is downward skip-free: every step is an integer ≥ -1.

      source
      theorem BGW.StableTrees.ae_partialSum_walkHitTime {μ : PMF ℕ} (ℓ : ℕ) :
      ∀ᵐ (w : ℕ → ℝ) ∂↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ)), ∀ (k : ℕ), walkHitTime ℓ w = ↑k → Probability.RealWalk.partialSum w k = -↑ℓ

      Weak hit is exact hit: a.s., if the walk ever reaches (-∞, -ℓ] it equals -ℓ there.

      source
      theorem BGW.StableTrees.walkPassageLaw_isProbabilityMeasure {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (ℓ n : ℕ) :
      MeasureTheory.IsProbabilityMeasure (walkPassageLaw μ ℓ n)

      walkPassageLaw is a probability measure when the hit is a.s. finite.

      source
      theorem BGW.StableTrees.walkHitTime_mass_eq_forestWeight (μ : PMF ℕ) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) (q : ℕ) :
      ↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ)) {w : ℕ → ℝ | walkHitTime ℓ w = ↑q} = forestWeight (⇑μ) ℓ q

      First-hit mass is the forest weight. For ℓ ≥ 1, the probability of a first hit of -ℓ at time q equals forestWeight μ ℓ q (via IsForestCode, firstPassageWords; the support condition K ≥ 0, i.e. steps ≥ -1, is used, since walkWeight of an arbitrary integer word does not encode μ).

      source
      theorem BGW.StableTrees.walkHitTime_mass_toReal {μ : PMF ℕ} {ℓ : ℕ} (hℓ : 1 ≤ ℓ) {q : ℕ} (hq : 1 ≤ q) :
      (↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))).real {w : ℕ → ℝ | walkHitTime ℓ w = ↑q} = ↑ℓ / ↑q * walkProb μ (↑q) (-↑ℓ)

      Kemperman for the first-hit mass. For ℓ ≥ 1, q ≥ 1: P(hit = q) = (ℓ / q) P(S_q = -ℓ), with the integer walk point probability walkProb.

      source
      theorem BGW.StableTrees.tsum_walkHitTime_mass {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {ℓ : ℕ} (hℓ : 1 ≤ ℓ) :
      ∑' (q : ℕ), forestWeight (⇑μ) ℓ q = 1

      The masses of the hitting times add up to 1 (a.s. finite hit), as tsum over q.

      source
      theorem BGW.StableTrees.ae_walkHitTime_ne_top {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (ℓ : ℕ) :
      ∀ᵐ (w : ℕ → ℝ) ∂↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ)), walkHitTime ℓ w ≠ ⊤

      The critical, nondegenerate offspring walk hits every level -ℓ a.s.

      source
      theorem BGW.StableTrees.walkHitTime_le_iff_iInf_stepPath_le {ℓ n : ℕ} {t b : ℝ} (ht : 0 ≤ t) (hb : 0 < b) (w : ℕ → ℝ) :
      walkHitTime ℓ w ≤ ↑⌊↑n * t⌋₊ ↔ ⨅ (s : ↑(Set.Icc 0 t)), (Skorokhod.realStepPath t n b w) s ≤ -↑ℓ / b

      Weak hit versus running minimum of the step path (deterministic, no limit): for b > 0, walkHitTime ℓ ≤ ⌊n t⌋ ↔ inf_{s ≤ t} realStepPath ≤ -ℓ/b. The infimum over [0, t] of the step path is a minimum over j ≤ ⌊n t⌋, so the WEAK inequality ≤ -ℓ/b is exact.