Càdlàg Regularity of the Global Window Patch

Proved

LevyStochCalc.Ito.Picard.cadlag_globalPatch_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concavevendored-levystochcalc

This states that a global patch of compatible window paths is almost surely càdlàg on the nonnegative time domain.

Let $Y_k:\mathbb R\to\Omega\to\mathbb R^n$ . Assume: (1) almost surely, globalPatch Y agrees with $Y_k$ on $[0,k+1]$ for every $k$ ; and (2) almost surely, each $Y_k$ is right-continuous and every coordinate has a left limit at every time.

Then, almost surely, for every $t\ge0$ , the global patch is right-continuous at $t$ and each coordinate has a left limit:

\lim_{s\downarrow t}\operatorname{globalPatch}(Y,s,\omega)=\operatorname{globalPatch}(Y,t,\omega),

and for every $i<n$ there exists $\ell\in\mathbb R$ with

\lim_{s\uparrow t}\operatorname{globalPatch}(Y,s,\omega,i)=\ell.

The conclusion is restricted to $t\ge0$ and is an almost-everywhere path property.

Original Lean declaration header

Within namespace LevyStochCalc.Ito.Picard. Shown in its original module context. Proof omitted.

theorem cadlag_globalPatch {Y : ℕ → ℝ → Ω → (Fin n → ℝ)}
    (hagree : ∀ᵐ ω ∂P, ∀ k : ℕ, ∀ t ∈ Set.Icc (0 : ℝ) ((k : ℝ) + 1),
      globalPatch Y t ω = Y k t ω)
    (hYcad : ∀ k, ∀ᵐ ω ∂P, ∀ t : ℝ,
      Filter.Tendsto (fun s => Y k s ω) (nhdsWithin t (Set.Ioi t)) (nhds (Y k t ω))
        ∧ ∀ i : Fin n, ∃ ℓ : ℝ,
            Filter.Tendsto (fun s => Y k s ω i) (nhdsWithin t (Set.Iio t)) (nhds ℓ)) :
    ∀ᵐ ω ∂P, ∀ t : ℝ, 0 ≤ t →
      Filter.Tendsto (fun s => globalPatch Y s ω) (nhdsWithin t (Set.Ioi t))
          (nhds (globalPatch Y t ω))
        ∧ ∀ i : Fin n, ∃ ℓ : ℝ,
            Filter.Tendsto (fun s => globalPatch Y s ω i) (nhdsWithin t (Set.Iio t)) (nhds ℓ)

Module navigation

Module: LevyStochCalc/Ito/PicardGlobal.

Previous: ae_all_windows_agree · Next: solvesOn_globalPatch.

Source excerpt, lines 202–213 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Ito_PicardGlobal

/-
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/Ito/PicardGlobal.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory LevyStochCalc.Probability
universe u v
variable {Ω : Type u} [MeasurableSpace Ω] {E : Type v} [MeasurableSpace E]
variable {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {n d : ℕ}
variable {ν : MeasureTheory.Measure E} [MeasureTheory.SigmaFinite ν]
variable (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
variable (N : LevyStochCalc.Poisson.PoissonRandomMeasure P ν)
variable (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
omit [MeasurableSpace E] [SigmaFinite ν] [IsProbabilityMeasure P]

Formal statement


theorem LevyStochCalc.Ito.Picard.cadlag_globalPatch_readable {Y : ℕ → ℝ → Ω → (Fin n → ℝ)}
    (hagree : ∀ᵐ ω ∂P, ∀ k : ℕ, ∀ t ∈ Set.Icc (0 : ℝ) ((k : ℝ) + 1),
      globalPatch Y t ω = Y k t ω)
    (hYcad : ∀ k, ∀ᵐ ω ∂P, ∀ t : ℝ,
      Filter.Tendsto (fun s => Y k s ω) (nhdsWithin t (Set.Ioi t)) (nhds (Y k t ω))
        ∧ ∀ i : Fin n, ∃ ℓ : ℝ,
            Filter.Tendsto (fun s => Y k s ω i) (nhdsWithin t (Set.Iio t)) (nhds ℓ)) :
    ∀ᵐ ω ∂P, ∀ t : ℝ, 0 ≤ t →
      Filter.Tendsto (fun s => globalPatch Y s ω) (nhdsWithin t (Set.Ioi t))
          (nhds (globalPatch Y t ω))
        ∧ ∀ i : Fin n, ∃ ℓ : ℝ,
            Filter.Tendsto (fun s => globalPatch Y s ω i) (nhdsWithin t (Set.Iio t)) (nhds ℓ) := by sorry

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Ito/PicardGlobal.lean#L200-L246 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Ito.PicardGlobal`, declaration `LevyStochCalc.Ito.Picard.cadlag_globalPatch`; 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