Weighted Clamped Bochner Isometry

Let $W$ be a Brownian motion with Brownian filtration $\mathcal F$, and let $H$ be a simple predictable integrand whose coefficient $H.\xi(i)$ is strongly measurable with respect to $\mathcal F_{H.\mathrm{partition}(i)}$. For $0\le s\le t$, let $g$ be strongly $\mathcal F_s$-measurable and suppose $|g(\omega)|\le C_g$ for every $\omega$. Put $c_i=\max\{s,\min\{H.\mathrm{partition}(i),t\}\}$. Then

where $I_r=\mathrm{simpleIntegral}(W,H,r)$. The conclusion is a weighted, simple-level conditional Itô isometry; all displayed integrals are ordinary real integrals.

Original Lean declaration header

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

lemma simpleIntegral_sub_sq_bochner_clamped_weighted
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
    {T : ℝ} (H : SimplePredictable Ω T)
    (h_adapt : ∀ i : Fin H.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ (H.partition i.castSucc)) (H.ξ i))
    {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t)
    {g : Ω → ℝ} (hg : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ s) g)
    {Cg : ℝ} (hg_bdd : ∀ ω, |g ω| ≤ Cg) :
    ∫ ω, g ω * (simpleIntegral W H t ω - simpleIntegral W H s ω) ^ 2 ∂P
      = ∑ i : Fin H.N,
        (max s (min (H.partition i.succ) t) - max s (min (H.partition i.castSucc) t))
          * ∫ ω, g ω * (H.ξ i ω) ^ 2 ∂P

Module navigation

Module: LevyStochCalc/Brownian/ItoL2CompletionCompensator.

Definition modules: LevyStochCalc/Brownian/Filtered, LevyStochCalc/Brownian/ItoSimpleIntegrand, LevyStochCalc/Brownian/Construction.

Supporting theorems: integral_factor_increment_sq, offDiagonal_increment_integral_zero_weighted, simpleIntegral_sub_eq_clamp_sum.

Previous: simpleIntegral_sub_eq_clamp_sum · Next: setIntegral_eval_sq_Icc_clamped.

Source excerpt, lines 175–189 · Frozen source 408915f.