Walk and interpolated-height path laws of the discrete forest

Heights are interpolated linearly; the walk retains the floor-step convention.

noncomputable def BGW.StableTrees.DiscreteForest.forestHeightLin (ω : ℕ → ℕ) (t : ℝ) : ℝ

Linear interpolation of the integer-time heights (not of the walk).

Equations

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

theorem BGW.StableTrees.DiscreteForest.continuous_forestHeightLin (ω : ℕ → ℕ) : Continuous (forestHeightLin ω)

The interpolated height is continuous.

noncomputable def BGW.StableTrees.DiscreteForest.forestHeightPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : C(↑(Set.Icc 0 ↑T), ℝ)

The normalised interpolated height path t ↦ (B n / n) * forestHeightLin ω (n t) on [0,T].

Equations

• BGW.StableTrees.DiscreteForest.forestHeightPath B n T ω = { toFun := fun (t : ↑(Set.Icc 0 ↑T)) => B n / ↑n * BGW.StableTrees.DiscreteForest.forestHeightLin ω (↑n * ↑t), continuous_toFun := ⋯ }

noncomputable def BGW.StableTrees.DiscreteForest.forestWalkPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : Skorokhod.D ↑T ℝ

The rescaled floor-step walk t ↦ W_{⌊n t⌋} / B n as an element of D T ℝ.

Equations

• BGW.StableTrees.DiscreteForest.forestWalkPath B n T ω = BGW.Skorokhod.realStepPath (↑T) n (B n) fun (i : ℕ) => ↑↑(ω i) - 1

noncomputable def BGW.StableTrees.DiscreteForest.forestPairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)

The pair (walk, height) path of the forest, with uniform topology on heights.

Equations

• BGW.StableTrees.DiscreteForest.forestPairPath B n T ω = (BGW.StableTrees.DiscreteForest.forestWalkPath B n T ω, BGW.StableTrees.DiscreteForest.forestHeightPath B n T ω)

theorem BGW.StableTrees.DiscreteForest.measurable_walk (k : ℕ) : Measurable fun (ω : ℕ → ℕ) => walk ω k

Each integer-time walk coordinate is measurable.

theorem BGW.StableTrees.DiscreteForest.measurable_forestHeight (k : ℕ) : Measurable fun (ω : ℕ → ℕ) => forestHeight ω k

Each integer-time record count is measurable.

theorem BGW.StableTrees.DiscreteForest.measurable_forestPairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (forestPairPath B n T)

(K01) Measurability of the pair path.

noncomputable def BGW.StableTrees.DiscreteForest.forestPairLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ))

The law of the pair path under the iid offspring sequence.

Equations

• BGW.StableTrees.DiscreteForest.forestPairLaw μ B n T = (BGW.StableTrees.DiscreteForest.offspringSeqLaw μ).map (BGW.StableTrees.DiscreteForest.forestPairPath B n T)

theorem BGW.StableTrees.DiscreteForest.forestPairLaw_fst (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : MeasureTheory.Measure.map Prod.fst ↑(forestPairLaw μ B n T) = ↑(stepPathLaw (realOffspringStepLaw μ) (↑T) B n)

The first marginal of the forest pair law is the step-path law of the offspring walk.