A Frozen Picard Fixed Point Solves On A Window

Proved

LevyStochCalc.Ito.Picard.solvesOn_of_isFixedPoint_readable

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

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

This is an auxiliary conversion theorem from a frozen fixed-point equation to SolvesOn. Let $W,N,\mathcal F$ and regular Lipschitz coefficients satisfy the stated hypotheses, let $x_0\in\mathbb R^n$ , and let $T\geq0$ . Suppose $Y:\mathbb R\to\Omega\to(\operatorname{Fin}(n)\to\mathbb R)$ is jointly measurable, progressively measurable, has finite Bielecki norm, and has finite $S^2$ -type supremum integral on every positive interval. Assume that for every $t\in[0,T]$ , $Y_t$ agrees almost surely coordinatewise with its frozen Picard step:

\forall t\in[0,T],\quad Y_t=\operatorname{picardStepOnRawStop}(Y,t)\quad P\text{-a.s.}

Then SolvesOn W N ℱ ... x₀ Y T holds. The result packages the required measurability and integrability witnesses and uses the equality before the horizon to obtain the standard jump-diffusion equation.

Original Lean declaration header

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

theorem solvesOn_of_isFixedPoint
    (hReg : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsRegular coeffs ν)
    {L : ℝ} (hLip : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsLipschitz coeffs ν L)
    (x₀ : Fin n → ℝ) {T : ℝ} (hT : 0 ≤ T) {Y : ℝ → Ω → (Fin n → ℝ)}
    (hYm : Measurable (Function.uncurry Y))
    (hYa : ∀ i : Fin n, Probability.ProgressivelyMeasurable ℱ fun ω s => Y s ω i)
    (hYb : bieleckiNorm (P := P) 0 T Y < ⊤)
    (hYS : ∀ T' : ℝ, 0 < T' →
      ∫⁻ ω, (⨆ t : Set.Icc (0 : ℝ) T', ∑ i, (‖Y (t : ℝ) ω i‖₊ : ℝ≥0∞) ^ 2) ∂P < ⊤)
    (hfix : ∀ t ∈ Set.Icc (0 : ℝ) T, ∀ᵐ ω ∂P, ∀ i : Fin n,
      Y t ω i = picardStepOnRawStop W N hℱW hℱN coeffs hReg hLip hYm hYa hYb hT x₀ t ω i) :
    SolvesOn W N ℱ hℱW hℱN coeffs x₀ Y T

Module navigation

Module: LevyStochCalc/Ito/PicardWindow.

Definition modules: LevyStochCalc/Poisson/Filtered, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Ito/Setting, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Ito/PicardBieleckiNorm, LevyStochCalc/Poisson/RandomMeasure, LevyStochCalc/Probability/Progressive, LevyStochCalc/Ito/PicardIntegrandFrozen.

Supporting theorems: picardStep_rawStop_congr_ae.

Previous: picardStep_rawStop_congr_ae · Next: exists_solvesOn.

Source excerpt, lines 407–418 · Frozen source 408915f.

Preamble

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/PicardWindow.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open scoped NNReal ENNReal
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 Ω›)
variable (hℱW : ∀ j : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W j) ℱ)
variable (hℱN : LevyStochCalc.Poisson.IsPoissonFiltration N ℱ)
variable (coeffs : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs n d E)

Formal statement


theorem LevyStochCalc.Ito.Picard.solvesOn_of_isFixedPoint_readable
    (hReg : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsRegular coeffs ν)
    {L : ℝ} (hLip : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsLipschitz coeffs ν L)
    (x₀ : Fin n → ℝ) {T : ℝ} (hT : 0 ≤ T) {Y : ℝ → Ω → (Fin n → ℝ)}
    (hYm : Measurable (Function.uncurry Y))
    (hYa : ∀ i : Fin n, Probability.ProgressivelyMeasurable ℱ fun ω s => Y s ω i)
    (hYb : bieleckiNorm (P := P) 0 T Y < ⊤)
    (hYS : ∀ T' : ℝ, 0 < T' →
      ∫⁻ ω, (⨆ t : Set.Icc (0 : ℝ) T', ∑ i, (‖Y (t : ℝ) ω i‖₊ : ℝ≥0∞) ^ 2) ∂P < ⊤)
    (hfix : ∀ t ∈ Set.Icc (0 : ℝ) T, ∀ᵐ ω ∂P, ∀ i : Fin n,
      Y t ω i = picardStepOnRawStop W N hℱW hℱN coeffs hReg hLip hYm hYa hYb hT x₀ t ω i) :
    SolvesOn W N ℱ hℱW hℱN coeffs x₀ Y T := by sorry

Source

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