Discrete walk bridges

Offspring vectors, their conditioned path laws and the finite cyclic identities. The path retains its terminal value -1 / B n.

1. The offspring vector, its path, and the two conditioned laws

noncomputable def BGW.StableTrees.DiscreteBridge.offspringVec (μ : PMF ℕ) (n : ℕ) : MeasureTheory.Measure (Fin n → ℕ)

The product law of an offspring vector (ω_0, ..., ω_{n-1}).

Equations

• BGW.StableTrees.DiscreteBridge.offspringVec μ n = MeasureTheory.Measure.pi fun (x : Fin n) => μ.toMeasure

instance BGW.StableTrees.DiscreteBridge.instIsProbabilityMeasureForallFinNatOffspringVec (μ : PMF ℕ) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (offspringVec μ n)

noncomputable def BGW.StableTrees.DiscreteBridge.vecPath (B : ℕ → ℝ) (n : ℕ) (ω : Fin n → ℕ) : Skorokhod.D 1 ℝ

The rescaled Łukasiewicz path t ↦ W_{⌊n t⌋} / B n of an offspring vector.

Equations

• BGW.StableTrees.DiscreteBridge.vecPath B n ω = BGW.Skorokhod.stepPath (BGW.stepWord ω) (B n)

theorem BGW.StableTrees.DiscreteBridge.measurable_vecPath (B : ℕ → ℝ) (n : ℕ) : Measurable (vecPath B n)

The path map is measurable (countable discrete source).

theorem BGW.StableTrees.DiscreteBridge.vecPath_one_of_mem_countBridges {B : ℕ → ℝ} {n : ℕ} (hn : 1 ≤ n) {ω : Fin n → ℕ} (hω : ω ∈ countBridges n) : (vecPath B n ω) ⟨1, ⋯⟩ = -1 / B n

Value at the terminal time of the path of a bridge vector: -1 / B n.

noncomputable def BGW.StableTrees.DiscreteBridge.conditionedVecOrJunk (μ : PMF ℕ) (n : ℕ) (A : Set (Fin n → ℕ)) : MeasureTheory.ProbabilityMeasure (Fin n → ℕ)

The offspring vector conditioned on A; the Dirac law at 0 when the conditioning event has mass zero (so that no proof field uses an unproved positivity fact).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.DiscreteBridge.walkBridgeLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (_hn : Admissible μ n) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

The walk bridge law: the offspring vector conditioned on ∑ ω_i = n - 1, pushed through vecPath (totalized; hn excludes the junk branch, see the positivity theorems below).

Equations

• BGW.StableTrees.DiscreteBridge.walkBridgeLaw μ B n _hn = (BGW.StableTrees.DiscreteBridge.conditionedVecOrJunk μ n (BGW.countBridges n)).map (BGW.StableTrees.DiscreteBridge.vecPath B n)

noncomputable def BGW.StableTrees.DiscreteBridge.exactWalkLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (_hn : Admissible μ n) : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)

The exact-size walk law: the offspring vector conditioned on being a tree excursion (Łukasiewicz path of a BGW tree of size n), pushed through vecPath (totalized).

Equations

• BGW.StableTrees.DiscreteBridge.exactWalkLaw μ B n _hn = (BGW.StableTrees.DiscreteBridge.conditionedVecOrJunk μ n (BGW.countExcursions n)).map (BGW.StableTrees.DiscreteBridge.vecPath B n)

theorem BGW.StableTrees.DiscreteBridge.offspringVec_countBridges_ne_zero {μ : PMF ℕ} {n : ℕ} (hn : Admissible μ n) : (offspringVec μ n) (countBridges n) ≠ 0

Admissibility (K03: exact-size mass nonzero) is positivity of the bridge mass (Kemperman: P(bridge) = n P(ζ = n)). Not used by any definition.

theorem BGW.StableTrees.DiscreteBridge.offspringVec_countExcursions_ne_zero {μ : PMF ℕ} {n : ℕ} (hn : Admissible μ n) : (offspringVec μ n) (countExcursions n) ≠ 0

Admissibility is positivity of the excursion mass P(excursion word) = P(ζ = n). Not used by any definition.

theorem BGW.StableTrees.DiscreteBridge.coe_conditionedVecOrJunk (μ : PMF ℕ) (n : ℕ) (A : Set (Fin n → ℕ)) (hA : (offspringVec μ n) A ≠ 0) : ↑(conditionedVecOrJunk μ n A) = (offspringVec μ n)[|A]

Off the junk branch the totalized law is the conditioned product law.

noncomputable def BGW.StableTrees.DiscreteBridge.restrictLaw (a : NNReal) (ha : a ≤ 1) (P : MeasureTheory.ProbabilityMeasure (Skorokhod.D 1 ℝ)) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑a ℝ)

Law of the restriction of a path to [0, a], a ≤ 1.

Equations

• BGW.StableTrees.DiscreteBridge.restrictLaw a ha P = P.map (BGW.Skorokhod.restrict ⋯)

noncomputable def BGW.StableTrees.DiscreteBridge.endValue (a : NNReal) (x : Skorokhod.D ↑a ℝ) : ℝ

The value of a path on [0, a] at its last time a.

Equations

• BGW.StableTrees.DiscreteBridge.endValue a x = x ⟨↑a, ⋯⟩

noncomputable def BGW.StableTrees.DiscreteBridge.rotateVec {n : ℕ} (ω : Fin n → ℕ) : Fin n → ℕ

The rotation of an offspring vector at the Vervaat index of its step word.

Equations

• BGW.StableTrees.DiscreteBridge.rotateVec ω = BGW.countsOfWord n ((BGW.stepWord ω).rotate (BGW.Skorokhod.vervaatIndex (BGW.stepWord ω)))

theorem BGW.StableTrees.DiscreteBridge.measurable_rotateVec (n : ℕ) : Measurable rotateVec

Rotation is a measurable map of the (countable, discrete) vector space.

theorem BGW.StableTrees.DiscreteBridge.vervaatD_vecPath {B : ℕ → ℝ} {n : ℕ} (hn : 1 ≤ n) (hB : 0 < B n) {ω : Fin n → ℕ} (hω : ω ∈ countBridges n) : Skorokhod.vervaatD (vecPath B n ω) = vecPath B n (rotateVec ω)

Deterministic identity: on bridge vectors the càdlàg Vervaat map of the path is the path of the rotated vector (vervaatD_stepPath, stepWord_countsOfWord), for positive norming.

theorem BGW.StableTrees.DiscreteBridge.rotateVec_mem_countExcursions {n : ℕ} (hn : 1 ≤ n) {ω : Fin n → ℕ} (hω : ω ∈ countBridges n) : rotateVec ω ∈ countExcursions n

A bridge vector rotated at the Vervaat index is a tree excursion (cycle lemma, exists_unique_rotate_isTreeExcursion).

theorem BGW.StableTrees.DiscreteBridge.map_rotateVec_cond_countBridges {μ : PMF ℕ} {n : ℕ} (hn : Admissible μ n) : MeasureTheory.Measure.map rotateVec (offspringVec μ n)[|countBridges n] = (offspringVec μ n)[|countExcursions n]

Cyclic law at the level of vectors: the bridge-conditioned product law, rotated at the Vervaat index, is the excursion-conditioned product law.

theorem BGW.StableTrees.DiscreteBridge.map_vervaatD_walkBridgeLaw {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (hB : 0 < B n) : MeasureTheory.Measure.map Skorokhod.vervaatD ↑(walkBridgeLaw μ B n hn) = ↑(exactWalkLaw μ B n hn)

Cyclic law at the level of paths (K06 second export): the Vervaat image of the discrete walk bridge is the exact-size Łukasiewicz path law. Positive norming is explicit.

noncomputable def BGW.StableTrees.DiscreteBridge.treePath (B : ℕ → ℝ) (n : ℕ) (τ : LocallyFinite.Tree) : Skorokhod.D 1 ℝ

The Łukasiewicz step path t ↦ W_{⌊n t⌋}/B n of a finite tree (junk path 0 for infinite trees), from its DFS increments.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.DiscreteBridge.measurable_treePath (B : ℕ → ℝ) (n : ℕ) : Measurable (treePath B n)

The totalized tree path is measurable because finite trees form a countable set.

theorem BGW.StableTrees.DiscreteBridge.treePath_toLocallyFinite (B : ℕ → ℝ) (n : ℕ) (t : PlaneTree) : treePath B n t.toLocallyFinite = Skorokhod.stepPath t.increments (B n)

The tree path evaluated on the finite-tree embedding is its increment step path.

theorem BGW.StableTrees.DiscreteBridge.map_treePath_exactTreeLaw {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) : MeasureTheory.Measure.map (treePath B n) ↑(DiscreteForest.exactTreeLaw μ n) = ↑(exactWalkLaw μ B n hn)

The exact-size walk law is the Łukasiewicz path of the exact-size BGW tree: one object.