Bounded Evaluation of a Simple Predictable Integrand

This technical lemma bounds every evaluation of a simple predictable integrand by a uniform coefficient bound.

Let $H$ be a SimplePredictable integrand on $\Omega$ with time horizon $T$, and let $C\ge0$. Assume that every coefficient $\xi_i(\omega)$ satisfies $|\xi_i(\omega)|\le C$ for every tile index $i$ and every $\omega\in\Omega$. Then, for every time $s\in\mathbb R$ and every $\omega\in\Omega$,

The statement uses the Lean definition SimplePredictable.eval. It also covers times outside all partition tiles, where the evaluation is zero. This bound is used to transfer coefficient bounds to the associated elementary integral.

Original Lean declaration header

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

theorem SimplePredictable.abs_eval_le {T : ℝ} (H : SimplePredictable Ω T) {C : ℝ} (hC0 : 0 ≤ C)
    (hC : ∀ (i : Fin H.N) (ω : Ω), |H.ξ i ω| ≤ C) (s : ℝ) (ω : Ω) : |H.eval s ω| ≤ C

Module navigation

Module: LevyStochCalc/Brownian/ItoIncrementMomentRestrict.

Definition modules: LevyStochCalc/Brownian/ItoSimpleIntegrand.

Next: SimplePredictable.varClock_le_Ioc.

Source excerpt, lines 60–61 · Frozen source 408915f.