Pulling a Past Weight Into a Windowed Itô Integral

This formalizes the pull-out identity for a bounded weight known at the beginning of a time window.

Let $(\Omega,\mathcal A,P)$ be a probability space, let $W$ be a Brownian motion under $P$, and let $\mathcal F$ be a filtration for which hℱ states that $W$ is Brownian. Let $0\le a<b$. Assume:

1. $V:\Omega\to\mathbb R$ is bounded, measurable, and strongly measurable with respect to $\mathcal F_a$.
2. $K:\Omega\times\mathbb R\to\mathbb R$ is jointly measurable and progressively measurable.
3. For every $T>0$, its $L^2$ energy is finite in the ENNReal sense:

$$\int_\Omega\int_{[0,T]}\|K(\omega,s)\|_+^2\,ds\,dP<\top.$$

4. The windowed integrand $\mathbf 1_{(a,b]}(s)K(\omega,s)$ is measurable, progressively measurable, and has finite energy on every positive horizon.
5. The weighted windowed integrand $V(\omega)\mathbf 1_{(a,b]}(s)K(\omega,s)$ is likewise measurable, progressively measurable, and has finite energy on every positive horizon.

Then for every $t>0$, the following equality holds $P$-almost everywhere:

$$V(\omega)\,I_t\!\left[\mathbf 1_{(a,b]}K\right](\omega) = I_t\!\left[V\mathbf 1_{(a,b]}K\right](\omega),$$

where $I_t$ denotes stochasticIntegralBrownian.

This is the main reusable pull-out identity for bounded information available before a window.

Original Lean declaration header

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

theorem mul_stochasticIntegralBrownian_indIoc {a b : ℝ} (ha : 0 ≤ a) (hab : a < b)
    {V : Ω → ℝ} (hVb : ∃ M : ℝ, ∀ ω, |V ω| ≤ M) (hVm : Measurable V)
    (hVa : @MeasureTheory.StronglyMeasurable Ω ℝ _ (ℱ a) V)
    (K : Ω → ℝ → ℝ) (hm : Measurable (Function.uncurry K))
    (hp : Probability.ProgressivelyMeasurable ℱ K)
    (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (him : Measurable (Function.uncurry fun ω s => indIoc Ω a b ω s * K ω s))
    (hip : Probability.ProgressivelyMeasurable ℱ fun ω s => indIoc Ω a b ω s * K ω s)
    (hiq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖indIoc Ω a b ω s * K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hvm : Measurable (Function.uncurry fun ω s => V ω * indIoc Ω a b ω s * K ω s))
    (hvp : Probability.ProgressivelyMeasurable ℱ fun ω s => V ω * indIoc Ω a b ω s * K ω s)
    (hvq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖V ω * indIoc Ω a b ω s * K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 < t) :
    (fun ω => V ω * stochasticIntegralBrownian W ℱ hℱ
        (fun ω s => indIoc Ω a b ω s * K ω s) him hip hiq t ω)
      =ᵐ[P] stochasticIntegralBrownian W ℱ hℱ
        (fun ω s => V ω * indIoc Ω a b ω s * K ω s) hvm hvp hvq t

Module navigation

Module: LevyStochCalc/Brownian/ItoPullOut.

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

Supporting theorems: stepIocMul_eval, stepIocMul₀_eval, stochasticIntegralBrownian_indicator_Ioc, stochasticIntegralBrownian_integralAgainst.

Previous: progressivelyMeasurable_mul_indIoc.

Source excerpt, lines 176–195 · Frozen source 408915f.

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoPullOut

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/ItoPullOut.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
variable {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
  (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : LevyStochCalc.Brownian.IsBrownianFiltration W ℱ)
include hℱ

theorem LevyStochCalc.Brownian.Ito.mul_stochasticIntegralBrownian_indIoc_readable {a b : ℝ} (ha : 0 ≤ a) (hab : a < b)
    {V : Ω → ℝ} (hVb : ∃ M : ℝ, ∀ ω, |V ω| ≤ M) (hVm : Measurable V)
    (hVa : @MeasureTheory.StronglyMeasurable Ω ℝ _ (ℱ a) V)
    (K : Ω → ℝ → ℝ) (hm : Measurable (Function.uncurry K))
    (hp : Probability.ProgressivelyMeasurable ℱ K)
    (hq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (him : Measurable (Function.uncurry fun ω s => indIoc Ω a b ω s * K ω s))
    (hip : Probability.ProgressivelyMeasurable ℱ fun ω s => indIoc Ω a b ω s * K ω s)
    (hiq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖indIoc Ω a b ω s * K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    (hvm : Measurable (Function.uncurry fun ω s => V ω * indIoc Ω a b ω s * K ω s))
    (hvp : Probability.ProgressivelyMeasurable ℱ fun ω s => V ω * indIoc Ω a b ω s * K ω s)
    (hvq : ∀ T, 0 < T → ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
      (‖V ω * indIoc Ω a b ω s * K ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
    {t : ℝ} (ht : 0 < t) :
    (fun ω => V ω * stochasticIntegralBrownian W ℱ hℱ
        (fun ω s => indIoc Ω a b ω s * K ω s) him hip hiq t ω)
      =ᵐ[P] stochasticIntegralBrownian W ℱ hℱ
        (fun ω s => V ω * indIoc Ω a b ω s * K ω s) hvm hvp hvq t := by sorry