Integrable Clamped Cross Term with Zero Mean

This is an integrability and zero-mean statement for time-clamped Brownian cross terms.

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 $0\le p<q$ and $0\le r<v$. Let $\xi$ and $\eta$ be bounded, measurable, and strongly measurable with respect to $\mathcal F_p$ and $\mathcal F_r$, respectively. For arbitrary $t,t'\in\mathbb R$, define the clamped increments using $\min(q,t)-\min(p,t)$ and $\min(v,t')-\min(r,t')$. The resulting product is integrable and

This lemma handles the individual terms appearing when simple stochastic integrals are expanded into partition sums.

Original Lean declaration header

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

lemma integrable_and_integral_cross_clamped (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)
    (hpq : p < q)
    (hr : 0 ≤ r) (hrv : r < v) {ξ η : Ω → ℝ} (hξ : StronglyMeasurable[ℱ p] ξ)
    (hξm : Measurable ξ) {Mξ : ℝ} (hξb : ∀ ω, |ξ ω| ≤ Mξ)
    (hη : StronglyMeasurable[ℱ r] η) (hηm : Measurable η)
    {Mη : ℝ} (hηb : ∀ ω, |η ω| ≤ Mη) (t t' : ℝ) :
    Integrable (fun ω => (ξ ω * ((W.W i).W (min q t) ω - (W.W i).W (min p t) ω))
      * (η ω * ((W.W j).W (min v t') ω - (W.W j).W (min r t') ω))) P
    ∧ ∫ ω, (ξ ω * ((W.W i).W (min q t) ω - (W.W i).W (min p t) ω))
      * (η ω * ((W.W j).W (min v t') ω - (W.W j).W (min r t') ω)) ∂P = 0

Module navigation

Module: LevyStochCalc/Brownian/CrossOrthogonalityLimit.

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

Supporting theorems: integrable_cross_term, integral_cross_increment_eq_zero_of_le.

Previous: integral_cross_increment_eq_zero_of_le · Next: integral_simpleIntegral_mul_eq_zero.

Source excerpt, lines 210–221 · Frozen source 408915f.