Prove2Me

Sudijono Thm. 1.1 (3): Var ξt(0)≤Ct\mathrm{Var}\,\xi_t(0)\le Ct

Open
KPZBallistic.sudijono_thm_1_1_variance

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

ballistic-depositionkpzprobability

In one-dimensional nearest-neighbour ballistic deposition on Z\mathbb Z from a flat surface, there is a constant C∈(0,∞)C\in(0,\infty) such that

Var⁡ξt(0)≤C tfor all t≥1.\operatorname{Var}\xi_t(0)\le C\,t\qquad\text{for all } t\ge1.

This is the best known upper bound on the height fluctuations; the KPZ prediction is Var⁡ξt(0)≍t2/3\operatorname{Var}\xi_t(0)\asymp t^{2/3}.

Preamble
import Mathlib
import Definitions.Def_KPZBallistic_Defs

open MeasureTheory ProbabilityTheory Filter Topology
Formal statement
namespace KPZBallistic

theorem sudijono_thm_1_1_variance {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (τ : ℤ → ℕ → Ω → ℝ) (hτ : IsPoissonClocks P τ) :
    ∃ C : ℝ, 0 < C ∧ ∀ t : ℝ, 1 ≤ t → variance (bdHeightReal τ t 0) P ≤ C * t := by sorry

end KPZBallistic
Source
T. Sudijono, A Linear Variance Bound for Ballistic Deposition (2026), https://arxiv.org/abs/2609.24056, Theorem 1.1, inequality (3), p. 2 (case d = 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