Additivity of the Brownian Itô Integral

This statement establishes additivity of the L² Brownian Itô integral in its integrand. Let $(Ω,P)$ be a probability space, let $W$ be a Brownian motion under $P$, and let $ℱ$ be a filtration for which $W$ is Brownian. Let $H₁,H₂:Ω×ℝ→ℝ$ be jointly measurable and progressively measurable. Assume that, for every $T>0$, the squared-energy integrals of $H₁$, $H₂$, and $H₁+H₂$ are finite in $[0,∞]$.

For every $T>0$, the integral of the pointwise sum agrees $P$-almost everywhere with the sum of the two integrals:

Here each displayed energy is an iterated ENNReal integral of the squared nnnorm, and all measurability, progressive-measurability, and finiteness hypotheses are explicit. The result is the basic linearity lemma used to obtain finite-sum and scalar-multiplication identities.

Original Lean declaration header

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

theorem stochasticIntegralBrownian_add {H₁ H₂ : Ω → ℝ → ℝ}
    (hm₁ : Measurable (Function.uncurry H₁)) (hm₂ : Measurable (Function.uncurry H₂))
    (hp₁ : Probability.ProgressivelyMeasurable ℱ H₁)
    (hp₂ : Probability.ProgressivelyMeasurable ℱ H₂)
    (hq₁ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H₁ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hq₂ : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hma : Measurable (Function.uncurry fun ω s => H₁ ω s + H₂ ω s))
    (hpa : Probability.ProgressivelyMeasurable ℱ fun ω s => H₁ ω s + H₂ ω s)
    (hqa : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H₁ ω s + H₂ ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {T : ℝ} (hT : 0 < T) :
    stochasticIntegralBrownian W ℱ hℱ (fun ω s => H₁ ω s + H₂ ω s) hma hpa hqa T
      =ᵐ[P] fun ω => stochasticIntegralBrownian W ℱ hℱ H₁ hm₁ hp₁ hq₁ T ω
        + stochasticIntegralBrownian W ℱ hℱ H₂ hm₂ hp₂ hq₂ T ω

Module navigation

Module: LevyStochCalc/Brownian/ItoLinear.

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

Supporting theorems: ae_eq_add_of_sq_distances, lintegral_energy_lt_top_of_bound, lintegral_energy_parallelogram.

Previous: ae_eq_add_of_sq_distances · Next: ae_eq_const_mul_of_sq_distances.

Source excerpt, lines 257–272 · Frozen source 408915f.