Finite-dimensional limits of real walk step paths

The increments of a floor-step path are sums over disjoint blocks of the iid walk. Their exact product law at each index and scalar convergence of each block give the finite-dimensional limits.

This is the finite-dimensional half of the functional limit theorem for walks in a stable domain of attraction (item C17 of CLASSICAL_THEORY_INPUTS.md; Skorokhod 1957, Theorem 2.7).

Increment maps and stable increment laws

def BGW.StableTrees.incrementsMap {T : ℝ} {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) : Skorokhod.D T ℝ → Fin k → ℝ

The increment vector (f t_1 - f t_0, …, f t_k - f t_{k-1}) of a path at the times t.

Equations

• BGW.StableTrees.incrementsMap t f i = f (t i.succ) - f (t i.castSucc)

theorem BGW.StableTrees.measurable_incrementsMap {T : ℝ} {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) : Measurable (incrementsMap t)

noncomputable def BGW.StableTrees.incrementVectorLaw (θ : ℝ) {k : ℕ} (t : Fin (k + 1) → ℝ) : MeasureTheory.ProbabilityMeasure (Fin k → ℝ)

The product of the stable increment laws at a finite family of times (Node 10; the underlying measure is Measure.pi (fun i => stableLawAt θ (t (i+1) - t i))).

Equations

• BGW.StableTrees.incrementVectorLaw θ t = MeasureTheory.ProbabilityMeasure.pi fun (i : Fin k) => BGW.StableTrees.stableLawAt θ (t i.succ - t i.castSucc)

theorem BGW.StableTrees.coe_incrementVectorLaw (θ : ℝ) {k : ℕ} (t : Fin (k + 1) → ℝ) : ↑(incrementVectorLaw θ t) = MeasureTheory.Measure.pi fun (i : Fin k) => ↑(stableLawAt θ (t i.succ - t i.castSucc))

theorem BGW.StableTrees.IsStableLevyLaw.map_incrementsMap {θ T : ℝ} {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D T ℝ)} (hP : IsStableLevyLaw θ T P) {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) (ht : StrictMono t) (ht0 : ↑(t 0) = 0) : P.map (incrementsMap t) = incrementVectorLaw θ fun (i : Fin (k + 1)) => ↑(t i)

Consistency with the characterization: a law with IsStableLevyLaw.increments has exactly the increment law incrementVectorLaw along every strictly increasing family starting at 0.

theorem BGW.StableTrees.realStepPath_sub {T : ℝ} (n : ℕ) (b : ℝ) (ω : ℕ → ℝ) (s u : ↑(Set.Icc 0 T)) (hsu : s ≤ u) : (Skorokhod.realStepPath T n b ω) u - (Skorokhod.realStepPath T n b ω) s = Probability.RealWalk.blockSum ω ⌊↑n * ↑s⌋₊ (⌊↑n * ↑u⌋₊ - ⌊↑n * ↑s⌋₊) / b

The step path starts at 0 with the exact increments being block sums: for 0 ≤ s ≤ u, path u - path s = blockSum ω ⌊n s⌋₊ (⌊n u⌋₊ - ⌊n s⌋₊) / b.

theorem BGW.StableTrees.map_stepPathLaw_incrementsMap (ν : MeasureTheory.ProbabilityMeasure ℝ) (T : ℝ) (B : ℕ → ℝ) (n : ℕ) {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) (ht : Monotone t) : ↑((stepPathLaw ν T B n).map (incrementsMap t)) = MeasureTheory.Measure.pi fun (i : Fin k) => MeasureTheory.Measure.map (fun (x : ℝ) => x / B n) ↑(Probability.RealWalk.sumLaw ν (⌊↑n * ↑(t i.succ)⌋₊ - ⌊↑n * ↑(t i.castSucc)⌋₊))

Exact finite-dimensional structure for every n (Node 1 block independence, valid even when blocks are empty): along a monotone family of times the increments of the step path are independent, with the laws of the normalized block sums of lengths ⌊n t_{i+1}⌋₊ - ⌊n t_i⌋₊.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_scaled_block_law {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) : Filter.Tendsto (fun (n : ℕ) => (Probability.RealWalk.sumLaw ν (⌊↑n * b⌋₊ - ⌊↑n * a⌋₊)).map fun (x : ℝ) => x / B n) Filter.atTop (nhds (stableLawAt θ (b - a)))

Scalar step (Node 4 + Slutsky): for 0 ≤ a < b the normalized block sum of length ⌊n b⌋₊ - ⌊n a⌋₊ (normalized by B n, NOT by the block's own normalizer) converges to stableLawAt θ (b - a). The length is ~ (b - a) n, so B (m n) / B n → (b - a)^{1/θ}.

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_stepPathLaw_increments {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) (ht : StrictMono t) : Filter.Tendsto (fun (n : ℕ) => (stepPathLaw ν T B n).map (incrementsMap t)) Filter.atTop (nhds (incrementVectorLaw θ fun (i : Fin (k + 1)) => ↑(t i)))

Node 10: the finite-dimensional increments of the step paths converge to the product of the stable increments at any finite strictly increasing family of times in [0,T] (not necessarily starting at 0; the terminal time T is allowed).

def BGW.StableTrees.cumulativeSum {k : ℕ} (x : Fin k → ℝ) : Fin k → ℝ

Partial sums of an increment vector (positions from increments, starting value 0).

Equations

• BGW.StableTrees.cumulativeSum x j = ∑ i : Fin k with i ≤ j, x i

theorem BGW.StableTrees.IsRealStableAttracted.tendsto_stepPathLaw_positions {ν : MeasureTheory.ProbabilityMeasure ℝ} {θ : ℝ} {B : ℕ → ℝ} (h : IsRealStableAttracted ν θ B) {T : ℝ} {k : ℕ} (t : Fin (k + 1) → ↑(Set.Icc 0 T)) (ht : StrictMono t) (ht0 : ↑(t 0) = 0) : Filter.Tendsto (fun (n : ℕ) => (stepPathLaw ν T B n).map fun (f : Skorokhod.D T ℝ) (i : Fin k) => f (t i.succ)) Filter.atTop (nhds ((incrementVectorLaw θ fun (i : Fin (k + 1)) => ↑(t i)).map cumulativeSum))

Position form, starting at 0 (the family t has t 0 = 0): the vector (f t_1, …, f t_k) converges to the cumulative sum of the independent stable increments (f t_0 = f 0 = 0 for every step path).