Fourth-Moment Bound for an Itô Integral Supported on an Interval

This theorem gives a fourth-moment bound for an $L^2$ Itô integral whose integrand is supported in $(a,b]$.

Let $W$ be a Brownian motion with Brownian filtration $\mathcal F$, and let $F:\Omega\times\mathbb R\to\mathbb R$ be jointly measurable and progressively measurable. Assume:

1. the squared norm of $F$ has finite $[0,\infty]$-valued integral on every $[0,T]$ with $T>0$;
2. $C\ge0$ and $|F(\omega,s)|\le C$ for all $\omega,s$;
3. $0\le a<b$;
4. $F(\omega,s)=0$ whenever $s\notin(a,b]$.

Then

The statement uses stochasticIntegralBrownian, ENNReal.ofReal, and an ENNReal-valued lintegral. It is the localized fourth-moment estimate for simple-integrand approximation and Fatou arguments.

Original Lean declaration header

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

theorem lintegral_stochasticIntegralBrownian_pow_four_le_Ioc
    (F : Ω → ℝ → ℝ) (hm : Measurable (Function.uncurry F))
    (hp : Probability.ProgressivelyMeasurable ℱ F)
    (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖F ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {C : ℝ} (hC0 : 0 ≤ C) (hCF : ∀ ω s, |F ω s| ≤ C)
    {a b : ℝ} (ha : 0 ≤ a) (hab : a < b)
    (hsupp : ∀ ω s, s ∉ Set.Ioc a b → F ω s = 0) :
    ∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ F hm hp hq b ω‖₊ : ℝ≥0∞) ^ 4 ∂P
      ≤ ENNReal.ofReal ((6 + gaussianFourthMoment) * C ^ 4 * (b - a) ^ 2)

Module navigation

Module: LevyStochCalc/Brownian/ItoIncrementMomentBounds.

Definition modules: LevyStochCalc/Brownian/ItoL2CompletionMaster, LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/Construction, LevyStochCalc/Brownian/ItoFourthMomentIncrements, LevyStochCalc/Probability/Progressive.

Selected supporting theorems: SimplePredictable.exists_restrict_Ioc, integral_partialSum_pow_four_le_varClock, SimplePredictable.lintegral_eval_sq_lt_top, SimplePredictable.lintegral_pow_four_eq, SimplePredictable.varClock_le_Ioc.

Next: lintegral_stochasticIntegralBrownian_sub_pow_four_le.

Source excerpt, lines 55–64 · Frozen source 408915f.