Vanishing Cross Term with Ordered Starting Times

This is a cross-orthogonality identity when the second interval starts no earlier than the first coefficient's reference time.

Let $W$ be a $d$-dimensional Brownian motion with distinct coordinates $i\ne j$, and let $\mathcal F$ make every coordinate a Brownian motion. Assume $p,r\ge0$, $p\le r< v$. Let $\xi$ be bounded, measurable, and strongly $\mathcal F_p$-measurable; let $\eta$ be bounded, measurable, and strongly $\mathcal F_r$-measurable. Then

The endpoint $q$ is unrestricted; the result covers both relative positions of $q$ and $r$ by splitting the first increment when necessary.

Original Lean declaration header

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

theorem integral_cross_increment_eq_zero_of_le (W : MultidimBrownianMotion P d)
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} {i j : Fin d} (hij : i ≠ j)
    (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ) {p q r v : ℝ} (hp : 0 ≤ p)
    (hr : 0 ≤ r) (hrv : r < v) (hpr : p ≤ r) {ξ η : Ω → ℝ} (hξ : StronglyMeasurable[ℱ p] ξ)
    (hξm : Measurable ξ) {Mξ : ℝ} (hξb : ∀ ω, |ξ ω| ≤ Mξ) (hη : StronglyMeasurable[ℱ r] η)
    (hηm : Measurable η) {Mη : ℝ} (hηb : ∀ ω, |η ω| ≤ Mη) :
    ∫ ω, (ξ ω * ((W.W i).W q ω - (W.W i).W p ω))
      * (η ω * ((W.W j).W v ω - (W.W j).W r ω)) ∂P = 0

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityLimit.

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

Supporting theorems: integral_mul_increment_pow, integral_pow_gaussianReal_zero, integrable_cross_term, integral_mul_increment_mul_increment_eq_zero.

Previous: integrable_cross_term · Next: integrable_and_integral_cross_clamped.

Source excerpt, lines 85–92 · Frozen source 408915f.