Global patching of finite-window paths

Definition

KLSModular_LevyStochCalc_Ito_PicardGlobal

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

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

Vendored from the LevyStochCalc library (https://github.com/cgarryZA/LevyStochCalc). globalPatch Y selects from a family of path maps $Y:\mathbb{N}\to\mathbb{R}\to\Omega\to(\mathrm{Fin}\,n\to\mathbb{R})$ the member indexed by the nonnegative ceiling $\lceil t\rceil_+$ at time $t$ . It is the stated gluing operation for finite-window solutions, but this bundle contains only the definition and no theorem asserting consistency or that the patched map solves the global equation.

Original module imports

import LevyStochCalc.Ito.PicardWindow

Original declaration excerpt

Shown in the original module context.

noncomputable def globalPatch (Y : ℕ → ℝ → Ω → (Fin n → ℝ)) : ℝ → Ω → (Fin n → ℝ) :=
  fun t ω => Y ⌈t⌉₊ t ω

Module navigation

Direct project imports: LevyStochCalc/Ito/PicardWindow.

Theorems in source order:

Project result: The KLS conjecture.

Original module · LevyStochCalc.Ito.PicardGlobal · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_LevyStochCalc_Ito_PicardWindow

/-
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
open scoped NNReal ENNReal
namespace LevyStochCalc
namespace Ito
namespace Picard
universe u v
variable {Ω : Type u} [MeasurableSpace Ω] {E : Type v} [MeasurableSpace E]
variable {P : Measure Ω} [IsProbabilityMeasure P] {n d : ℕ}
/-- Glue a family of window solutions, using on `[0, t]` the member whose horizon covers `t`. -/
noncomputable def globalPatch (Y : ℕ → ℝ → Ω → (Fin n → ℝ)) : ℝ → Ω → (Fin n → ℝ) :=
  fun t ω => Y ⌈t⌉₊ t ω
end Picard
end Ito
end LevyStochCalc

Source

Lean source: https://github.com/cgarryZA/LevyStochCalc/blob/984dbf0b790031eac05d56fe5a84b65e15e1e932/LevyStochCalc/Ito/PicardGlobal.lean#L86-L88 (repository human-ai-mathematics/kls-lean, commit 408915f, module `LevyStochCalc.Ito.PicardGlobal`, definition bundle `KLSModular_LevyStochCalc_Ito_PicardGlobal`; 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