Continuous mapping for fixed-band occupations

Outside the countable union of boundary levels, the finite-path occupation map is continuous almost surely under the stable process law.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.finiteOccupationJoint (T : NNReal) (ε : ℝ) {r : ℕ} (t : Fin r → NNReal) (f : Skorokhod.D ↑T ℝ) : Skorokhod.D ↑T ℝ × (Fin r → ℝ)

Pair a finite path with its exact Lebesgue occupations at the chosen times.

Equations

• BGW.StableTrees.DiscreteHeightApprox.finiteOccupationJoint T ε t f = (f, fun (i : Fin r) => BGW.StableTrees.DiscreteHeightApprox.finiteHeightApprox T (t i) ε f)

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_finiteOccupationJoint (T : NNReal) (ε : ℝ) {r : ℕ} (t : Fin r → NNReal) : Measurable (finiteOccupationJoint T ε t)

The finite-path joint occupation map is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.tendsto_joint_finiteOccupation {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {r : ℕ} (t : Fin r → NNReal) (ht : ∀ (i : Fin r), t i ≤ T) : ∃ (Exc : Set ℝ), Exc.Countable ∧ ∀ (ε : ℝ), 0 < ε → ε ∉ Exc → Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map fun (ω : ℕ → ℕ) => finiteOccupationJoint T ε t (DiscreteForest.forestWalkPath B n T ω)) Filter.atTop (nhds ((stableLocalLaw θ).map (continuumJoint T ε t)))

Exact finite-path occupations converge jointly with the walk outside countably many bands.