Endpoint weights for exact-size prefixes

The endpoint recovers the pending stack by rounding the integer walk value.

noncomputable def BGW.StableTrees.ExactPrefix.prefixStack (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (x : Skorokhod.D ↑a ℝ) : ℕ

The number of pending subtrees j = W_m + 1 read off the path value at a.

Equations

• BGW.StableTrees.ExactPrefix.prefixStack B n a x = (round (BGW.StableTrees.DiscreteBridge.endValue a x * B n) + 1).toNat

noncomputable def BGW.StableTrees.ExactPrefix.prefixWeightFn (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (x : Skorokhod.D ↑a ℝ) : ℝ

The RN weight R_n(m,j) (K03 exactPrefixWeight) as a function of the prefix path, m = ⌊a n⌋, j = prefixStack.

Equations

• BGW.StableTrees.ExactPrefix.prefixWeightFn μ B n a x = BGW.StableTrees.exactPrefixWeight μ n ⌊↑a * ↑n⌋₊ (BGW.StableTrees.ExactPrefix.prefixStack B n a x)

theorem BGW.StableTrees.ExactPrefix.measurable_prefixStack (B : ℕ → ℝ) (n : ℕ) (a : NNReal) : Measurable (prefixStack B n a)

The pending-stack count is measurable.

theorem BGW.StableTrees.ExactPrefix.measurable_prefixWeightFn (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) : Measurable (prefixWeightFn μ B n a)

Measurability of the weight (a function of the value at a only).

def BGW.StableTrees.ExactPrefix.LatticeGood (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) (x : Skorokhod.D ↑a ℝ) : Prop

Tail-prefix atoms are lattice-good: j ≥ 1 and d ∣ (n - m) - j (every tree has size ≡ 1 mod d, increments are ≡ -1 mod d).

Equations

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

theorem BGW.StableTrees.ExactPrefix.tendsto_prefixWeightFn_continuousConv {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) {x : Skorokhod.D ↑a ℝ} (hx : ContinuousAt ⇑x ⟨↑a, ⋯⟩) (hxpos : 0 < DiscreteBridge.endValue a x) {y : ℕ → Skorokhod.D ↑a ℝ} (hy : ∀ (k : ℕ), LatticeGood μ B (q k) a (y k)) (hyx : Filter.Tendsto y Filter.atTop (nhds x)) : Filter.Tendsto (fun (k : ℕ) => prefixWeightFn μ B (q k) a (y k)) Filter.atTop (nhds (gammaA θ (↑a) (DiscreteBridge.endValue a x)))

Weight convergence along sequences: if y_k → x in D a ℝ, x is continuous at a with x(a) > 0, and each y_k is lattice-good at the size q k, then R_{q k}(m, j(y_k)) → gammaA θ a (x a) (K03 exactPrefixWeight_uniform).