Clamped Simple-Integrand Square Integral

This technical identity concerns a simple predictable integrand $G$ on a measurable space $(\Omega,\mathcal F)$, a point $\omega\in\Omega$, a horizon parameter $T\in\mathbb R$, and a time $t\in\mathbb R$. Writing $p_i=G.\mathrm{partition}(i)$, $\xi_i=G.\xi(i,\omega)$, and $G.\mathrm{eval}(u,\omega)$ for the integrand value, the real integral over the interval $[0,t]$ equals the partition sum

The clamping by minima makes each partition length nonnegative, including when $t<0$. This is the real-valued companion of the corresponding nonnegative integral formula and provides a closed sum representation for the simple-level compensator.

Original Lean declaration header

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

lemma setIntegral_eval_sq_Icc_clamped {T : ℝ} (G : SimplePredictable Ω T) (ω : Ω)
    {t : ℝ} :
    ∫ u in Set.Icc (0 : ℝ) t, (G.eval u ω) ^ 2 ∂volume
      = ∑ i : Fin G.N,
        (min (G.partition i.succ) t - min (G.partition i.castSucc) t) * (G.ξ i ω) ^ 2

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionCompensator.

Definition modules: LevyStochCalc/Brownian/ItoSimpleIntegrand.

Previous: simpleIntegral_sub_sq_bochner_clamped_weighted · Next: martingale_simpleIntegral_sq_sub_compensator.

Source excerpt, lines 288–292 · Frozen source 408915f.