Clamped Increment Expansion for Simple Integrals

For a Brownian motion $W$, a simple predictable integrand $H$, times $s\le t$, and $\omega\in\Omega$, define the clamped partition point $c_i=\max\{s,\min\{H.\mathrm{partition}(i),t\}\}$. The simple Itô integral satisfies

The probability assumption on $P$ is part of the declaration, although the identity is pointwise. This provides the partition-level representation used in conditional Itô-isometry calculations.

Original Lean declaration header

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

lemma simpleIntegral_sub_eq_clamp_sum
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    {T : ℝ} (H : SimplePredictable Ω T) {s t : ℝ} (hst : s ≤ t) (ω : Ω) :
    simpleIntegral W H t ω - simpleIntegral W H s ω
      = ∑ i : Fin H.N, H.ξ i ω * (W.W (max s (min (H.partition i.succ) t)) ω
          - W.W (max s (min (H.partition i.castSucc) t)) ω)

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionCompensator.

Definition modules: LevyStochCalc/Brownian/Construction, LevyStochCalc/Brownian/ItoSimpleIntegrand.

Previous: offDiagonal_increment_integral_zero_weighted · Next: simpleIntegral_sub_sq_bochner_clamped_weighted.

Source excerpt, lines 140–146 · Frozen source 408915f.