Picard Self-Map Agrees With Its Limit

This is an auxiliary fixed-point statement for a jump-diffusion Picard construction. Let $(\Omega,P)$ be a probability space, let $E$ carry a sigma-finite measure $\nu$, let $W$ be a $d$-dimensional Brownian motion and $N$ a Poisson random measure, and let $\mathcal F'$ be a right-continuous filtration for which $W$ is Brownian and $N$ is Poisson. Assume the filtration is suitably ordered at nonpositive times and that every $P$-null measurable set is measurable at time $0$. Let coeffs be regular Lipschitz jump-diffusion coefficients with Lipschitz constant $L$, let $x_0\in\mathbb R^n$, let $T>0$, let $\beta>0$, and let $X_0$ be an $\mathcal F'$-adapted bounded initial process on $[0,T]$. Assume

For every $t\in[0,T]$, the raw self-map applied to the Picard limit agrees almost surely, coordinatewise, with that Picard limit:

Here the displayed expressions use the measurable, progressively measurable, and finite-Bielecki-norm witnesses required by the Lean definitions picardLimit and picardSelfMapRaw. The result is a technical realization of the Picard fixed point as a process in the admissible process space.

Formalization Note bieleckiNorm and the contraction factor take values in $[0,\infty]$ (ENNReal); the almost-everywhere assertion is with respect to the probability measure $P$ and is pointwise in time and coordinate.

Original Lean declaration header

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

theorem picardSelfMapRaw_picardLimit_ae_eq {β : ℝ} (hβ : 0 < β) (hT : 0 < T)
    (X₀ : SBoundedProcess (n := n) P ℱ' T)
    (hq : (ENNReal.ofReal
            ((3 * ((n : ℝ) * L ^ 2 * T + (n : ℝ) * ((d : ℝ) * L ^ 2) + (n : ℝ) * L ^ 2))
              / (2 * β))) ^ ((1 : ℝ) / 2) < 1)
    {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) T) :
    ∀ᵐ ω ∂P, ∀ i,
      (picardSelfMapRaw W N ℱ' hℱW hℱN hℱ0 hnull coeffs hReg hLip x₀ hT
          (measurable_picardLimit W N ℱ' hℱW hℱN hℱ0 hnull coeffs hReg hLip x₀ hT X₀)
          (progressivelyMeasurable_picardLimit W N ℱ' hℱW hℱN hℱ0 hnull coeffs hReg hLip
            x₀ hT X₀)
          (bieleckiNorm_picardLimit_lt_top W N ℱ' hℱW hℱN hℱ0 hnull coeffs hReg hLip x₀
            hβ hT X₀ hq)).X t ω i
        = picardLimit W N ℱ' hℱW hℱN hℱ0 hnull coeffs hReg hLip x₀ hT X₀ t ω i

Module navigation

Module: LevyStochCalc/Ito/PicardContractionFixedPoint.

Definition modules: LevyStochCalc/Ito/PicardBieleckiNorm, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Ito/PicardOutputModification, LevyStochCalc/Poisson/RandomMeasure, LevyStochCalc/Ito/Setting, LevyStochCalc/Poisson/Filtered, LevyStochCalc/Brownian/Filtered.

Supporting theorems: ae_eq_zero_of_bieleckiNorm_eq_zero, bieleckiNorm_picardStepOnRawStop_picardLimit_eq_zero, measurable_picardStepOnRawStop_slice, picardSelfMapRaw_ae_eq.

Previous: ae_eq_zero_of_bieleckiNorm_eq_zero · Next: bieleckiNorm_picardStepOnRawStop_diff_le.

Source excerpt, lines 268–281 · Frozen source 408915f.