Zero Extension Preserves Elementary Integrals

Let $G$ be a simple predictable integrand with horizon $T$, let $T'$ be later than its final partition point, and let $M:ℝ→Ω→ℝ$ be any process. The zero-extended integrand G.appendInterval hlt has the same elementary integral against $M$ at every time $t$ and sample point $ω$:

The equality is pointwise and requires no measurability or probabilistic assumptions on $M$. This bookkeeping lemma permits simple integrands with different horizons to be placed on a common terminal partition.

Original Lean declaration header

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

theorem SimplePredictable.appendInterval_integralAgainst
    {T : ℝ} (G : SimplePredictable Ω T) {T' : ℝ}
    (hlt : G.partition (Fin.last G.N) < T') (M : ℝ → Ω → ℝ) (t : ℝ) (ω : Ω) :
    (G.appendInterval hlt).integralAgainst M t ω = G.integralAgainst M t ω

Module navigation

Module: LevyStochCalc/Brownian/ItoAlgebraProduct.

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

Previous: SimplePredictable.sum_xi_mul_simpleIntegral_sub · Next: SimplePredictable.exists_mul_simple.

Source excerpt, lines 231–234 · Frozen source 408915f.