Orthogonality of Simple Integrals on Distinct Coordinates

This is the orthogonality statement for elementary stochastic integrals against distinct Brownian coordinates.

Let $W$ be a $d$-dimensional Brownian motion with distinct coordinates $i\ne j$, and let $\mathcal F$ be a common Brownian filtration. Let $H$ and $K$ be simple predictable integrands with strongly measurable coefficients at their respective partition start times. For arbitrary $t,t'\in\mathbb R$,

This is the finite-partition orthogonality result used before passing to general stochastic integrals by $L^2$ approximation.

Original Lean declaration header

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

theorem integral_simpleIntegral_mul_eq_zero (W : MultidimBrownianMotion P d)
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} {i j : Fin d} (hij : i ≠ j)
    (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ) {TH TK : ℝ}
    (H : SimplePredictable Ω TH)
    (K : SimplePredictable Ω TK)
    (hH : ∀ a : Fin H.N, StronglyMeasurable[ℱ (H.partition a.castSucc)] (H.ξ a))
    (hK : ∀ b : Fin K.N, StronglyMeasurable[ℱ (K.partition b.castSucc)] (K.ξ b))
    (t t' : ℝ) :
    ∫ ω, simpleIntegral (W.W i) H t ω * simpleIntegral (W.W j) K t' ω ∂P = 0

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityLimit.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Brownian/ItoSimpleIntegrand.

Supporting theorems: integrable_and_integral_cross_clamped.

Previous: integrable_and_integral_cross_clamped · Next: memLp_simpleIntegral.

Source excerpt, lines 240–248 · Frozen source 408915f.