Grid Decomposition of a Weighted Cross Increment

This is a weighted telescoping identity for two distinct Brownian coordinates.

Let $W$ be a $d$-dimensional Brownian motion, let $i,j\in\mathrm{Fin}(d)$, and let $\mathcal F$ make every coordinate a Brownian motion. Assume $a\ge0$, $h>0$, $m\in\mathbb N$, and let $Z$ be strongly $\mathcal F_a$-measurable, measurable, and bounded in absolute value by $C$. With $s_k=\texttt{affineGrid}(a,h,k)$,

The declaration isolates the grid decomposition that reduces a whole-interval cross term to cell-wise cross products.

Original Lean declaration header

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

lemma integral_mul_increment_mul_increment_eq_crossSum (W : MultidimBrownianMotion P d)
    (i j : Fin d) {ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
    (hcoord : ∀ k : Fin d, IsBrownianFiltration (W.W k) ℱ)
    {a h : ℝ} (ha : 0 ≤ a) (hh : 0 < h) (m : ℕ) {Z : Ω → ℝ} (hZ : StronglyMeasurable[ℱ a] Z)
    (hZm : Measurable Z) {C : ℝ} (hZb : ∀ ω, |Z ω| ≤ C) :
    ∫ ω, Z ω * (((W.W i).W (affineGrid a h m) ω - (W.W i).W a ω)
      * ((W.W j).W (affineGrid a h m) ω - (W.W j).W a ω)) ∂P
      = ∫ ω, Z ω * ∑ 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) ω) ∂P

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.

Previous: integral_crossSum_sq · Next: integral_mul_increment_mul_increment_eq_zero.

Source excerpt, lines 226–235 · Frozen source 408915f.