Orthogonality of Itô Integrals on Distinct Brownian Coordinates

This is the orthogonality identity for Itô integrals driven by distinct coordinates of a multidimensional Brownian motion.

Let $W$ be a $d$-dimensional Brownian motion, let $i\ne j$, and let $\mathcal F$ be a common Brownian filtration. Let $H$ and $K$ be measurable and progressively measurable integrands whose integrated squared norms are finite in $\mathrm{ENNReal}$ on every positive interval. For $t\ge0$, the corresponding scalar Itô integrals satisfy

where $I^i_t=\texttt{stochasticIntegral}(W^i,\mathcal F,H,t)$ and $I^j_t=\texttt{stochasticIntegral}(W^j,\mathcal F,K,t)$.

The statement is the general orthogonality result obtained from elementary-integrand orthogonality and $L^2$ convergence.

Formalization Note The square-integrability hypotheses are expressed through MemLp in the supporting declarations, while the integrand assumptions use $\mathrm{ENNReal}$ lower integrals.

Original Lean declaration header

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

theorem integral_stochasticIntegral_mul_eq_zero (W : MultidimBrownianMotion P d)
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} {i j : Fin d} (hij : i ≠ j)
    (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ)
    {H K : Ω → ℝ → ℝ} (hHm : Measurable (Function.uncurry H))
    (hHp : Probability.ProgressivelyMeasurable ℱ H)
    (hHs : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hKm : Measurable (Function.uncurry K))
    (hKp : Probability.ProgressivelyMeasurable ℱ K)
    (hKs : ∀ T : ℝ, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 ≤ t) :
    ∫ ω, stochasticIntegral (W.W i) ℱ (hcoord i) H hHm hHp hHs t ω
      * stochasticIntegral (W.W j) ℱ (hcoord j) K hKm hKp hKs t ω ∂P = 0

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityLimit.

Definition modules: LevyStochCalc/Brownian/ItoL2CompletionApi, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Multidim, LevyStochCalc/Probability/Progressive.

Supporting theorems: integral_mul_eq_zero_of_tendsto_eLpNorm, integral_simpleIntegral_mul_eq_zero, memLp_simpleIntegral.

Previous: integral_mul_eq_zero_of_tendsto_eLpNorm.

Source excerpt, lines 371–384 · Frozen source 408915f.