Fourth-Moment Expansion for a Brownian Increment

This technical lemma gives the fourth-moment recursion for adding a bounded, time-$a$-measurable multiple of a Brownian increment.

Let $W$ be a Brownian motion with Brownian filtration $\mathcal F$, let $0\le a<b$, and let $S,\xi:\Omega\to\mathbb R$ satisfy:

1. $S\in L^4(P)$ and $S$ is measurable and strongly measurable with respect to $\mathcal F_a$;
2. $\xi$ is measurable and strongly measurable with respect to $\mathcal F_a$;
3. $C\ge0$ and $|\xi(\omega)|\le C$ for every $\omega$.

Then

where $\mathsf g_4$ is gaussianFourthMoment. This result is an auxiliary one-step identity for fourth-moment recursions.

Original Lean declaration header

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

private theorem integral_add_mul_increment_pow_four
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
    {a b : ℝ} (ha : 0 ≤ a) (hab : a < b) {S ξ : Ω → ℝ}
    (hS4 : MemLp S 4 P) (hSm : Measurable S)
    (hSad : @MeasureTheory.StronglyMeasurable Ω ℝ _ (ℱ a) S)
    (hξm : Measurable ξ) (hξad : @MeasureTheory.StronglyMeasurable Ω ℝ _ (ℱ a) ξ)
    {C : ℝ} (hC0 : 0 ≤ C) (hCξ : ∀ ω, |ξ ω| ≤ C) :
    ∫ ω, (S ω + ξ ω * (W.W b ω - W.W a ω)) ^ 4 ∂P
      = (∫ ω, S ω ^ 4 ∂P)
        + 6 * ((∫ ω, S ω ^ 2 * ξ ω ^ 2 ∂P) * (b - a))
        + (∫ ω, ξ ω ^ 4 ∂P) * ((b - a) ^ 2 * gaussianFourthMoment)

Module navigation

Module: LevyStochCalc/Brownian/ItoFourthMomentPartialSums.

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

Supporting theorems: integral_mul_increment_pow, integral_pow_gaussianReal_zero.

Previous: integral_add_mul_increment_sq · Next: integral_partialSum_sq_succ.

Source excerpt, lines 107–117 · Frozen source 408915f.