Scalar Homogeneity of the Brownian Itô Integral

This statement establishes homogeneity of the Brownian Itô integral. Let $(Ω,P)$ be a probability space, let $W$ be a Brownian motion, and let $ℱ$ be a Brownian filtration. Let $H:Ω×ℝ→ℝ$ be jointly measurable and progressively measurable, with finite squared ENNReal energy on every $[0,T]$ for $T>0$. Fix $c∈ℝ$, and assume the scaled process $cH$ is jointly measurable, progressively measurable, and has finite squared energy on every positive time interval.

For every $T>0$,

The statement is pointwise in the scalar $c$ and time $T$, with all admissibility hypotheses for both integrands explicit. It complements additivity to provide linearity of the integral.

Original Lean declaration header

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

theorem stochasticIntegralBrownian_const_mul {H : Ω → ℝ → ℝ}
    (hm : Measurable (Function.uncurry H)) (hp : Probability.ProgressivelyMeasurable ℱ H)
    (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (c : ℝ)
    (hmc : Measurable (Function.uncurry fun ω s => c * H ω s))
    (hpc : Probability.ProgressivelyMeasurable ℱ fun ω s => c * H ω s)
    (hqc : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖c * H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {T : ℝ} (hT : 0 < T) :
    stochasticIntegralBrownian W ℱ hℱ (fun ω s => c * H ω s) hmc hpc hqc T
      =ᵐ[P] fun ω => c * 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_const_mul_of_sq_distances, lintegral_energy_const_mul.

Previous: ae_eq_const_mul_of_sq_distances.

Source excerpt, lines 346–357 · Frozen source 408915f.