Existence of an Adapted Simple Product

Let $W$ be a Brownian motion, let $ℱ$ be a filtration, and let $G,K$ be simple predictable integrands with arbitrary horizons. Assume every coefficient of $G$ and $K$ is strongly measurable with respect to the filtration at its preceding partition time.

Then there exist a horizon $T₃$ and a simple predictable integrand $Q$ on that horizon such that: (1) every coefficient of $Q$ is adapted and strongly measurable; (2) for all $s,ω$, $Q(s,ω)=G(s,ω)K(s,ω)$; and (3) for all $t,ω$,

The statement is existential because the common horizon and refinement are constructed from the two original horizons. It provides closure of simple predictable integrands under products.

Original Lean declaration header

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

theorem SimplePredictable.exists_mul_simple
    {P : Measure Ω} [IsProbabilityMeasure P] (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›)
    {T₁ T₂ : ℝ} (G : SimplePredictable Ω T₁) (K : SimplePredictable Ω T₂)
    (h_adaptG : ∀ i : Fin G.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ (G.partition i.castSucc)) (G.ξ i))
    (h_adaptK : ∀ i : Fin K.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
      (ℱ (K.partition i.castSucc)) (K.ξ i)) :
    ∃ (T₃ : ℝ) (Q : SimplePredictable Ω T₃),
      (∀ i : Fin Q.N, @MeasureTheory.StronglyMeasurable Ω ℝ _
        (ℱ (Q.partition i.castSucc)) (Q.ξ i))
      ∧ (∀ s ω, Q.eval s ω = G.eval s ω * K.eval s ω)
      ∧ (∀ t ω, G.integralAgainst (fun u ω' => simpleIntegral W K u ω') t ω
          = simpleIntegral W Q t ω)

Module navigation

Module: LevyStochCalc/Brownian/ItoAlgebraProduct.

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

Supporting theorems: SimplePredictable.appendInterval_integralAgainst, SimplePredictable.eval_mul_on_common, SimplePredictable.sum_xi_mul_simpleIntegral_sub.

Previous: SimplePredictable.appendInterval_integralAgainst.

Source excerpt, lines 284–297 · Frozen source 408915f.