Prove2Me

Penrose Thm. 2.1: Eξt(0)/t→ρ1E\xi_t(0)/t\to\rho_1 and LpL^p law of large numbers

Open
KPZBallistic.penrose_thm_2_1

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, let h(t)=E[ξt(0)]h(t)=E[\xi_t(0)]. There is a constant ρ1∈(0,∞)\rho_1\in(0,\infty) such that

h(t)t→ρ1(t→∞),\frac{h(t)}{t}\to\rho_1\qquad(t\to\infty),

and moreover, for every p∈[1,∞)p\in[1,\infty), ξt(0)/t→ρ1\xi_t(0)/t\to\rho_1 in Lp(P)L^p(P) as t→∞t\to\infty.

The constant ρ1\rho_1 is the asymptotic growth speed of the interface; it is the centring for any fluctuation result.

Preamble
import Mathlib
import Definitions.Def_KPZBallistic_Defs

open MeasureTheory ProbabilityTheory Filter Topology
Formal statement
namespace KPZBallistic

theorem penrose_thm_2_1 {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (τ : ℤ → ℕ → Ω → ℝ) (hτ : IsPoissonClocks P τ) :
    ∃ ρ : ℝ, 0 < ρ ∧
      Tendsto (fun t : ℝ => (∫ ω, bdHeightReal τ t 0 ω ∂P) / t) atTop (𝓝 ρ) ∧
      ∀ p : ℝ, 1 ≤ p →
        Tendsto (fun t : ℝ => eLpNorm (fun ω => bdHeightReal τ t 0 ω / t - ρ)
          (ENNReal.ofReal p) P) atTop (𝓝 0) := 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, Section 2, Theorem 2.1 and eq. (2.11), p. 5 (case d = 1, nearest-neighbour model)
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