2444 CHAPTER 72. THE HARD ITO FORMULA

is real predictable because it is the pointwise limit of real predictable functions, those in thesequence being real predictable because of the continuity of X (t) into V ′ and Propositon72.1.2. Now since H ⊆V ′ it follows that for all v ∈V,

(t,ω)→(X (a)X[a,b) (t) ,v

)is real predictable. This holds for h ∈ H replacing v in the above because V is dense in H.By the Pettis theorem, this proves the lemma.

Lemma 72.3.3 In Situation 72.3.1 the following formula holds for a.e. ω for 0 < s < twhere M (t) ≡

∫ t0 Z (u)dW (u). Here and elsewhere, |·| denotes the norm in H and ⟨·, ·⟩

denotes the duality pairing between V,V ′. Also X = X̄ for a.e. ω at t,s so that it makes nodifference off a set of measure zero whether we write ⟨Y (u) ,X (t)⟩ or ⟨Y (u) , X̄ (t)⟩

|X (t)|2 = |X (s)|2 +2∫ t

s⟨Y (u) ,X (t)⟩du+2(X (s) ,M (t)−M (s))

+ |M (t)−M (s)|2−|X (t)−X (s)− (M (t)−M (s))|2 (72.3.4)

Also for t > 0

|X (t)|2 = |X0|2 +2∫ t

0⟨Y (u) ,X (t)⟩du+2(X0,M (t))

+ |M (t)|2−|X (t)−X0−M (t)|2 (72.3.5)

Proof: The formula is a straight forward computation which holds a.e. ω .

|M (t)−M (s)|2−|X (t)−X (s)− (M (t)−M (s))|2 +2(X (s) ,M (t)−M (s))

= |M (t)−M (s)|2−|X (t)−X (s)|2−|M (t)−M (s)|2

+2(X (t)−X (s) ,M (t)−M (s))+2(X (s) ,M (t)−M (s))

=−|X (t)−X (s)|2 +2(X (t) ,M (t)−M (s))

=−|X (t)−X (s)|2 +2(X (t) ,X (t)−X (s))−2⟨∫ t

sY (u)du,X (t)

⟩

= −|X (t)|2−|X (s)|2 +2(X (t) ,X (s))+2 |X (t)|2−2(X (t) ,X (s))

−2∫ t

s⟨Y (u) ,X (t)⟩du

= |X (t)|2−|X (s)|2−2∫ t

s⟨Y (u) ,X (t)⟩du