Joint walk and height observables

Discrete and continuum joint observables are measurable. Exceptional boundary levels are countable by disjointness of their level sets in path-time product measure.

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

The discrete joint object: the rescaled walk path and the ε-occupations at times t.

Equations

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

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

The continuum joint object: the restricted path and heightApprox ε at times t.

Equations

• BGW.StableTrees.DiscreteHeightApprox.continuumJoint T ε t f = (BGW.Skorokhod.DLoc.restrict T f, fun (i : Fin r) => BGW.StableTrees.heightApprox ε f (t i))

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_discreteJoint (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ε : ℝ) {r : ℕ} (t : Fin r → NNReal) : Measurable (discreteJoint B n T ε t)

The discrete joint walk and occupation observable is measurable.

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

The continuum joint walk and occupation observable is measurable.

noncomputable def BGW.StableTrees.DiscreteHeightApprox.heightJoint (B : ℕ → ℝ) (n : ℕ) (T : NNReal) {r : ℕ} (t : Fin r → NNReal) (ω : ℕ → ℕ) : Skorokhod.D ↑T ℝ × (Fin r → ℝ)

The joint object (scaled walk, normalized discrete heights).

Equations

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

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

The limit object (restricted path, continuum height height θ) at times t.

Equations

• BGW.StableTrees.DiscreteHeightApprox.heightLimitJoint θ T t f = (BGW.Skorokhod.DLoc.restrict T f, fun (i : Fin r) => BGW.StableTrees.height θ f (t i))

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_heightJoint (B : ℕ → ℝ) (n : ℕ) (T : NNReal) {r : ℕ} (t : Fin r → NNReal) : Measurable (heightJoint B n T t)

The discrete joint walk and height observable is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.measurable_heightLimitJoint (θ : ℝ) (T : NNReal) {r : ℕ} (t : Fin r → NNReal) : Measurable (heightLimitJoint θ T t)

The continuum joint walk and height observable is measurable.

theorem BGW.StableTrees.DiscreteHeightApprox.countable_boundaryLevels {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (t : NNReal) : {ε : ℝ | 0 < ε ∧ 0 < ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | 0 < MeasureTheory.volume {s : ℝ | 0 ≤ s ∧ s ≤ ↑t ∧ ↑f s.toNNReal = futureInf f t s.toNNReal + ε}}}.Countable

Boundary levels are countable (Fubini): at most countably many ε > 0 have P(Leb{s ≤ t | X_s = I^s_t + ε} > 0) > 0 (the level sets are disjoint in Ω × [0,t]).