Grid stopping times for Itô-integral locality

Definition

KLSModular_LevyStochCalc_Brownian_ItoLocality

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-contextvendored-levystochcalc

Vendored from the LevyStochCalc library at https://github.com/cgarryZA/LevyStochCalc, commit 984dbf0b790031eac05d56fe5a84b65e15e1e932. For a stopping time $\tau:\Omega\to\mathbb R\cup\{\infty\}$ , stepStop τ c is the two-valued stopping time that is $\infty$ when $c\le\tau$ and $c$ otherwise. gridPt t n k is $kt/n$ , gridStopAux τ t n recursively takes the minimum of the relevant stepStop values, and gridStop τ t n is the resulting stopping time at the first grid point strictly beyond $\tau$ among the grid points indexed through $n$ .

Original module imports

import LevyStochCalc.Brownian.ItoOptionalStopping
import LevyStochCalc.Brownian.ItoIncrement

Original declaration excerpt

Shown in the original module context.

noncomputable def stepStop (c : ℝ) : Ω → WithTop ℝ :=
  fun ω => if (c : WithTop ℝ) ≤ τ ω then ⊤ else (c : WithTop ℝ)

Module navigation

Direct project imports: LevyStochCalc/Brownian/ItoOptionalStopping, LevyStochCalc/Brownian/ItoIncrement.

Theorems in source order:

Project result: The KLS conjecture.

Original module · LevyStochCalc.Brownian.ItoLocality · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoOptionalStopping
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoIncrement

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoLocality.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal Topology
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
  (τ : Ω → WithTop ℝ)
section GridStop
/-- The two-valued stopping time that stops at `c`, unless `τ` has already reached `c`. -/
noncomputable def stepStop (c : ℝ) : Ω → WithTop ℝ :=
  fun ω => if (c : WithTop ℝ) ≤ τ ω then ⊤ else (c : WithTop ℝ)
/-- A point of the uniform grid on `[0, t]` with `n` steps. -/
noncomputable def gridPt (t : ℝ) (n k : ℕ) : ℝ := (k : ℝ) * t / (n : ℝ)
/-- The stopping time that stops at the first grid point strictly beyond `τ`, among the first
`k + 1` points. -/
noncomputable def gridStopAux (t : ℝ) (n : ℕ) : ℕ → Ω → WithTop ℝ
  | 0 => stepStop τ (gridPt t n 0)
  | (k + 1) => fun ω => min (stepStop τ (gridPt t n (k + 1)) ω) (gridStopAux t n k ω)
/-- The stopping time that stops at the first point of the uniform grid on `[0, t]` with `n`
steps that lies strictly beyond `τ`. -/
noncomputable def gridStop (t : ℝ) (n : ℕ) : Ω → WithTop ℝ := gridStopAux τ t n n
end GridStop
end Ito
end Brownian
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Brownian/ItoLocality.lean#L40-L171 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Brownian.ItoLocality`, definition bundle `KLSModular_LevyStochCalc_Brownian_ItoLocality`; the repository is private at upload time). Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (Apache-2.0; upstream copyright notice retained in the Lean text).

View graph