Finite-Sum Linearity of the Brownian Itô Integral

This statement gives finite-sum linearity of the Brownian Itô integral together with admissibility data for the summed integrand. Let $(Ω,P)$ be a probability space, let $W$ be a Brownian motion, and let $ℱ$ be a Brownian filtration. For an index type $ι$, let $H_i:Ω×ℝ→ℝ$ be jointly measurable and progressively measurable for every $i∈ι$, and assume that each $H_i$ has finite squared ENNReal energy on every interval $[0,T]$ with $T>0$. Let $J$ be a finite subset of $ι$ and let $T>0$.

There exist joint measurability and progressive-measurability proofs for the finite sum $\sum_{i∈J}H_i$, together with the corresponding finite-energy property, such that

The theorem is existential in the auxiliary admissibility proofs; it does not assert uniqueness of those proofs. It packages finite-sum linearity for later constructions.

Original Lean declaration header

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

theorem exists_stochasticIntegralBrownian_finsetSum {ι : Type*}
    (H : ι → Ω → ℝ → ℝ) (hm : ∀ i, Measurable (Function.uncurry (H i)))
    (hp : ∀ i, Probability.ProgressivelyMeasurable ℱ (H i))
    (hq : ∀ (i : ι) (T : ℝ), 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H i ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (J : Finset ι) {T : ℝ} (hT : 0 < T) :
    ∃ (hms : Measurable (Function.uncurry fun ω u => ∑ i ∈ J, H i ω u))
      (hps : Probability.ProgressivelyMeasurable ℱ fun ω u => ∑ i ∈ J, H i ω u)
      (hqs : ∀ T', 0 < T' → ∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) T',
        (‖∑ i ∈ J, H i ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤),
      stochasticIntegralBrownian W ℱ hℱ (fun ω u => ∑ i ∈ J, H i ω u) hms hps hqs T
        =ᵐ[P] fun ω => ∑ i ∈ J,
          stochasticIntegralBrownian W ℱ hℱ (H i) (hm i) (hp i) (hq i) T ω

Module navigation

Module: LevyStochCalc/Brownian/ItoFinsetSum.

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

Supporting theorems: lintegral_energy_lt_top_of_bound, stochasticIntegralBrownian_add, stochasticIntegralBrownian_ae_zero.

Previous: stochasticIntegralBrownian_sub.

Source excerpt, lines 124–136 · Frozen source 408915f.