Elementary Integral Against an Elementary Integral

Let $W$ be a Brownian motion, and let $G,K$ be simple predictable integrands with the same final partition point. For every time $t$ and sample point $ω$,

where $I_K=\texttt{simpleIntegral}(W,K)$ and the product is formed on the common refinement. The equality is pointwise; the probability assumption on $P$ is present in the declaration but no almost-everywhere qualification occurs in the conclusion. This is the finite-partition associativity identity used to pass from elementary products to Itô-integral products.

Original Lean declaration header

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

theorem SimplePredictable.sum_xi_mul_simpleIntegral_sub
    {P : Measure Ω} [IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
    {T : ℝ} (G K : SimplePredictable Ω T)
    (h_eq : G.partition (Fin.last G.N) = K.partition (Fin.last K.N))
    (t : ℝ) (ω : Ω) :
    (∑ i : Fin G.N, G.ξ i ω *
        (simpleIntegral W K (min (G.partition i.succ) t) ω
          - simpleIntegral W K (min (G.partition i.castSucc) t) ω))
      = simpleIntegral W (G.mul_on_common K h_eq) t ω

Module navigation

Module: LevyStochCalc/Brownian/ItoAlgebraProduct.

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

Previous: SimplePredictable.eval_mul_on_common · Next: SimplePredictable.appendInterval_integralAgainst.

Source excerpt, lines 115–123 · Frozen source 408915f.