Seppäläinen: $\xi_t(0)/t\to\rho_1$ almost surely

Open

KPZBallistic.seppalainen_strong_law

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

ballistic-depositionkpzprobability

In one-dimensional nearest-neighbour ballistic deposition on $\mathbb Z$ from a flat surface, there is a constant $\rho_1\in(0,\infty)$ with $E[\xi_t(0)]/t\to\rho_1$ and

\frac{\xi_t(0)}{t}\to\rho_1\qquad\text{almost surely as } t\to\infty.

This is the strong law of large numbers for the height of a column; the limit is the same constant as in the $L^p$ law of large numbers.

Preamble

import Mathlib
import Definitions.Def_KPZBallistic_Defs

open MeasureTheory ProbabilityTheory Filter Topology

Formal statement

namespace KPZBallistic

theorem seppalainen_strong_law {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (τ : ℤ → ℕ → Ω → ℝ) (hτ : IsPoissonClocks P τ) :
    ∃ ρ : ℝ, 0 < ρ ∧
      Tendsto (fun t : ℝ => (∫ ω, bdHeightReal τ t 0 ω ∂P) / t) atTop (𝓝 ρ) ∧
      ∀ᵐ ω ∂P, Tendsto (fun t : ℝ => bdHeightReal τ t 0 ω / t) atTop (𝓝 ρ) := by sorry

end KPZBallistic

Source

M. D. Penrose, Growth and roughness of the interface for ballistic deposition, J. Stat. Phys. 131 (2008), https://arxiv.org/abs/math/0608540, remark after Theorem 2.1, p. 5 ('In the special case of the NN model, it can be deduced from Theorem 1 of Seppalainen [19] that (2.11) holds with almost sure convergence'); T. Seppalainen, Strong law of large numbers for the interface in ballistic deposition, Ann. Inst. H. Poincare Probab. Statist. 36 (2000), https://arxiv.org/abs/math/9906193, Theorem 1

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Seppäläinen: ξt(0)/t→ρ1\xi_t(0)/t\to\rho_1ξt​(0)/t→ρ1​ almost surely

Seppäläinen: $\xi_t(0)/t\to\rho_1$ almost surely