Prove2Me

Sudijono Thm. 1.1 (2): concentration of ξt(0)\xi_t(0) on scale t\sqrt t

Open
KPZBallistic.sudijono_thm_1_1_concentration

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 are constants c,C∈(0,∞)c,C\in(0,\infty) such that for every t≥1t\ge1 and r≥0r\ge0,

P(∣ξt(0)−Eξt(0)∣≥r)≤Cexp⁡{−c r2t+r}.P\big(|\xi_t(0)-E\xi_t(0)|\ge r\big)\le C\exp\Big\{-c\,\frac{r^2}{t+r}\Big\}.

This exponential concentration inequality implies the diffusive variance bound Var⁡ξt(0)≤Ct\operatorname{Var}\xi_t(0)\le Ct.

Preamble
import Mathlib
import Definitions.Def_KPZBallistic_Defs

open MeasureTheory ProbabilityTheory Filter Topology
Formal statement
namespace KPZBallistic

theorem sudijono_thm_1_1_concentration {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (τ : ℤ → ℕ → Ω → ℝ) (hτ : IsPoissonClocks P τ) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ t : ℝ, 1 ≤ t → ∀ r : ℝ, 0 ≤ r →
      P.real {ω | r ≤ |bdHeightReal τ t 0 ω - ∫ ω', bdHeightReal τ t 0 ω' ∂P|} ≤
        C * Real.exp (-c * r ^ 2 / (t + r)) := 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 (2), 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