Second Moment of a Discrete Cross-Increment Sum

This is the exact second-moment identity for cross products of distinct Brownian coordinates on a uniform grid.

Let $W$ be a $d$-dimensional Brownian motion, let $i,j\in\mathrm{Fin}(d)$ be distinct, and let $\mathcal F$ make every coordinate a Brownian motion. For $a\ge0$, $h>0$, and $m\in\mathbb N$, define the grid points $s_k=\texttt{affineGrid}(a,h,k)$. Then the cross-increment sum is square-integrable and

This identity is the discrete variance calculation underlying the direct cross-orthogonality argument.

Original Lean declaration header

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

lemma integral_crossSum_sq (W : MultidimBrownianMotion P d) {i j : Fin d} (hij : i ≠ j)
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ)
    {a h : ℝ} (ha : 0 ≤ a) (hh : 0 < h) (m : ℕ) :
    Integrable (fun ω => (∑ k ∈ Finset.range m,
        ((W.W i).W (affineGrid a h (k + 1)) ω - (W.W i).W (affineGrid a h k) ω)
          * ((W.W j).W (affineGrid a h (k + 1)) ω - (W.W j).W (affineGrid a h k) ω)) ^ 2) P
    ∧ ∫ ω, (∑ k ∈ Finset.range m,
        ((W.W i).W (affineGrid a h (k + 1)) ω - (W.W i).W (affineGrid a h k) ω)
          * ((W.W j).W (affineGrid a h (k + 1)) ω - (W.W j).W (affineGrid a h k) ω)) ^ 2 ∂P
      = m * h ^ 2

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityDirectCross.

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

Supporting theorems: integral_mul_increment_pow, integral_pow_gaussianReal_zero.

Next: integral_mul_increment_mul_increment_eq_crossSum.

Source excerpt, lines 96–105 · Frozen source 408915f.