Raw Self-Map Modification Equals the Picard Step

This states that the path component of the raw Picard self-map is an almost-everywhere modification of the corresponding stopped Picard step.

Let $P$ be a probability measure, $W$ and $N$ be the Brownian and Poisson drivers, and let $\mathcal F$ be right-continuous, satisfy the filtration-at-zero and null-set hypotheses, and be compatible with both drivers. Let the coefficients be regular and Lipschitz. Let $Z$ be jointly measurable and progressively measurable coordinatewise, with $\operatorname{bieleckiNorm}(0,T,Z)<\top$ for $T>0$.

For every $t\in\mathbb R$,

This identifies the modification used by the self-map with the explicitly defined Picard step at each fixed time.

Original Lean declaration header

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

theorem picardSelfMapRaw_ae_eq
    (W : LevyStochCalc.Brownian.Multidim.MultidimBrownianMotion P d)
    (N : LevyStochCalc.Poisson.PoissonRandomMeasure P ν)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) [ℱ.IsRightContinuous]
    (hℱW : ∀ j : Fin d, LevyStochCalc.Brownian.IsBrownianFiltration (W.W j) ℱ)
    (hℱN : LevyStochCalc.Poisson.IsPoissonFiltration N ℱ)
    (hℱ0 : ∀ t : ℝ, t ≤ 0 → ℱ 0 ≤ ℱ t)
    (hnull : ∀ s : Set Ω, MeasurableSet s → P s = 0 → MeasurableSet[ℱ 0] s)
    (coeffs : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs n d E)
    (hReg : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsRegular coeffs ν)
    {L : ℝ} (hLip : LevyStochCalc.Ito.Setting.JumpDiffusionCoeffs.IsLipschitz coeffs ν L)
    (x₀ : Fin n → ℝ) {T : ℝ} (hT : 0 < 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 < ⊤) (t : ℝ) :
    (picardSelfMapRaw W N ℱ hℱW hℱN hℱ0 hnull coeffs hReg hLip x₀ hT hZm hZa hZb).X t
      =ᵐ[P] picardStepOnRawStop W N hℱW hℱN coeffs hReg hLip hZm hZa hZb hT.le x₀ t

Module navigation

Module: LevyStochCalc/Ito/PicardOutputModification.

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

Source excerpt, lines 482–498 · Frozen source 408915f.