Frozen And Unfrozen Picard Steps Agree Before The Horizon

Proved

LevyStochCalc.Ito.Picard.picardStep_rawStop_congr_ae_readable

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

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

This is a window-locality statement. Let $W,N,\mathcal F$ and the regular Lipschitz coefficients satisfy the stated Brownian, Poisson, measurability, and integrability hypotheses. Let $Z$ be a jointly measurable, progressively measurable state process with finite Bielecki norm and finite $S^2$ -type supremum integral on every positive interval. If $0\leq T$ , $0\leq t$ , and $t\leq T$ , then

\operatorname{picardStepOnRawStop}(Z,t,\omega)=\operatorname{picardStep}(Z,t,\omega)

for $P$ -almost every $\omega$ . Thus freezing the input path at $T$ does not alter the Picard step at earlier times. The lemma is used to pass from raw fixed-point equations on a window to the usual picardStep equation.

Original Lean declaration header

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

theorem picardStep_rawStop_congr_ae
    (hReg : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsRegular coeffs ν)
    {L : ℝ} (hLip : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsLipschitz coeffs ν L)
    (x₀ : Fin n → ℝ) {T : ℝ} {Z : ℝ → Ω → (Fin n → ℝ)}
    (hZm : Measurable (Function.uncurry Z))
    (hZa : ∀ i : Fin n, Probability.ProgressivelyMeasurable ℱ fun ω s => Z s ω i)
    (hZb : bieleckiNorm (P := P) 0 T Z < ⊤)
    (hZS : ∀ T' : ℝ, 0 < T' →
      ∫⁻ ω, (⨆ t : Set.Icc (0 : ℝ) T', ∑ i, (‖Z (t : ℝ) ω i‖₊ : ℝ≥0∞) ^ 2) ∂P < ⊤)
    (hT : 0 ≤ T) {t : ℝ} (ht0 : 0 ≤ t) (htT : t ≤ T) :
    ∀ᵐ ω ∂P,
      picardStepOnRawStop W N hℱW hℱN coeffs hReg hLip hZm hZa hZb hT x₀ t ω
        = picardStep W N ℱ hℱW hℱN coeffs Z x₀
            (measurable_sigma_comp_state coeffs hReg hZm)
            (progressivelyMeasurable_sigma_comp_state coeffs hReg hZa)
            (lintegral_sq_sigma_lt_top_of_supL2 coeffs hReg hLip hZm hZS)
            (measurable_gamma_comp_state coeffs hReg hZm)
            (markedProgressivelyMeasurable_gamma_comp_state coeffs hReg hZa)
            (lintegral_sq_gamma_lt_top_of_supL2 coeffs hReg hLip hZm hZS)
            t ω

Module navigation

Module: LevyStochCalc/Ito/PicardWindow.

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

Supporting theorems: picardStep_diffusion_congr_ae, picardStep_jump_congr_ae.

Previous: ae_eq_of_solvesOn · Next: solvesOn_of_isFixedPoint.

Source excerpt, lines 338–357 · 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.picardStep_rawStop_congr_ae_readable
    (hReg : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsRegular coeffs ν)
    {L : ℝ} (hLip : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsLipschitz coeffs ν L)
    (x₀ : Fin n → ℝ) {T : ℝ} {Z : ℝ → Ω → (Fin n → ℝ)}
    (hZm : Measurable (Function.uncurry Z))
    (hZa : ∀ i : Fin n, Probability.ProgressivelyMeasurable ℱ fun ω s => Z s ω i)
    (hZb : bieleckiNorm (P := P) 0 T Z < ⊤)
    (hZS : ∀ T' : ℝ, 0 < T' →
      ∫⁻ ω, (⨆ t : Set.Icc (0 : ℝ) T', ∑ i, (‖Z (t : ℝ) ω i‖₊ : ℝ≥0∞) ^ 2) ∂P < ⊤)
    (hT : 0 ≤ T) {t : ℝ} (ht0 : 0 ≤ t) (htT : t ≤ T) :
    ∀ᵐ ω ∂P,
      picardStepOnRawStop W N hℱW hℱN coeffs hReg hLip hZm hZa hZb hT x₀ t ω
        = picardStep W N ℱ hℱW hℱN coeffs Z x₀
            (measurable_sigma_comp_state coeffs hReg hZm)
            (progressivelyMeasurable_sigma_comp_state coeffs hReg hZa)
            (lintegral_sq_sigma_lt_top_of_supL2 coeffs hReg hLip hZm hZS)
            (measurable_gamma_comp_state coeffs hReg hZm)
            (markedProgressivelyMeasurable_gamma_comp_state coeffs hReg hZa)
            (lintegral_sq_gamma_lt_top_of_supL2 coeffs hReg hLip hZm hZS)
            t ω := by sorry

Source

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