Weighted Off-Diagonal Brownian Cancellation

This establishes cancellation of a weighted product of separated Brownian increments. Let $W$ be a Brownian motion with Brownian filtration $\mathcal F$, let $0\le a_1<b_1\le a_2<b_2$, and let $\xi_1,\xi_2,g:\Omega\to\mathbb R$ be strongly measurable with respect to $\mathcal F_{a_1}$, $\mathcal F_{a_2}$, and $\mathcal F_{a_1}$, respectively. Then

This is a technical off-diagonal identity used when expanding squared sums of Brownian increments; the later increment is conditionally centered relative to the information available at $a_2$.

Original Lean declaration header

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

lemma offDiagonal_increment_integral_zero_weighted
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
    {a₁ b₁ a₂ b₂ : ℝ} (ha₁ : 0 ≤ a₁) (h₁ : a₁ < b₁) (h₁₂ : b₁ ≤ a₂) (h₂ : a₂ < b₂)
    (ξ₁ ξ₂ g : Ω → ℝ)
    (hadapt₁ : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ a₁) ξ₁)
    (hadapt₂ : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ a₂) ξ₂)
    (hg : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ a₁) g) :
    ∫ ω, g ω * ((ξ₁ ω * (W.W b₁ ω - W.W a₁ ω)) * (ξ₂ ω * (W.W b₂ ω - W.W a₂ ω))) ∂P
      = 0

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionCompensator.

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

Next: simpleIntegral_sub_eq_clamp_sum.

Source excerpt, lines 74–87 · Frozen source 408915f.