Itô's formula

8 fully proved

Pathwise Taylor sums and Riemann sums

TheoremSecond-order Taylor sums along a continuous path#✓fully proved

For f of class C², a continuous path w, t ≥ 0, and a sequence of mesh counts ns j → ∞ along which the quadratic sums ∑_{k < ns j} (w (t (k + 1) / ns j) - w (t k / ns j))² stay bounded, the telescoped increment f (w t) - f (w 0) minus the second-order Taylor sums ∑_k (f'(w_k) Δw_k + (1/2) f''(w_k) Δw_k²) tends to 0.

theorem tendsto_taylor_sum_sub {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) {w : ℝ → ℝ}
    (hw : Continuous w) {t : ℝ} (ht : 0 ≤ t) {ns : ℕ → ℕ} (hns : Tendsto ns atTop atTop)
    {M : ℝ}
    (hM : ∀ j, ∑ k ∈ Finset.range (ns j),
      (w (t * (k + 1) / ns j) - w (t * k / ns j)) ^ 2 ≤ M) :
    Tendsto (fun j ↦ f (w t) - f (w 0) - ∑ k ∈ Finset.range (ns j),
      (deriv f (w (t * k / ns j)) * (w (t * (k + 1) / ns j) - w (t * k / ns j)) +
        (1 / 2) * deriv (deriv f) (w (t * k / ns j)) *
          (w (t * (k + 1) / ns j) - w (t * k / ns j)) ^ 2)) atTop (𝓝 0)

Used by 1

Used byItô's formula

TheoremLeft-point Riemann sums of a continuous function#✓fully proved

Left-point Riemann sums of a continuous function on the uniform partition of [0, t] converge to the integral: ∑_{k < n} g (t k / n) (t / n) → ∫_0^t g (t ≥ 0).

theorem tendsto_sum_riemann_uniform {g : ℝ → ℝ} (hg : Continuous g) {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun n : ℕ ↦ ∑ k ∈ Finset.range n, g (t * k / n) * (t / n)) atTop
      (𝓝 (∫ u in (0 : ℝ)..t, g u))

Used by 1

Used byItô's formula

Left-point approximation of g ∘ B

DefinitionLeft-point step process along a Brownian path#✓fully proved

The left-point step process ∑_{k < n} g(B (t k / n)) 1_{(t k / n, t (k + 1) / n]} of u ↦ g (B u) on the uniform partition of [0, t] into n cells.

noncomputable def leftPointProcess {Ω : Type*} (g : ℝ → ℝ) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0)
    (n : ℕ) (u : ℝ≥0) (ω : Ω) : ℝ :=
  ∑ i : Fin n, (Set.Ioc (t * (i : ℕ) / n) (t * ((i : ℕ) + 1) / n)).indicator
    (fun _ ↦ g (B (t * (i : ℕ) / n) ω)) u

Used by 3

Used byItô's formula · Left-point approximation of a Lipschitz function of Brownian motion · Process of the left-point integrand is the left-point step process

TheoremLeft-point approximation of a Lipschitz function of Brownian motion#✓fully proved

For a pre-Brownian motion B that is jointly measurable in (u, ω) and an L-Lipschitz g, the left-point step processes of u ↦ g (B u) converge to it in L²(P ⊗ du) on (0, t] × Ω: E ∫_0^t |leftPointProcess g B t n u - g (B u)|² du → 0.

theorem tendsto_lintegral_leftPointProcess_sub_sq
    {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBm : Measurable fun p : ℝ≥0 × Ω ↦ B p.1 p.2)
    {g : ℝ → ℝ} {L : ℝ} (hg : ∀ x y, |g x - g y| ≤ L * |x - y|) (t : ℝ≥0) :
    Tendsto (fun n ↦ ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t,
      ‖leftPointProcess g B t n u.toNNReal ω - g (B u.toNNReal ω)‖ₑ ^ 2) ∂P) atTop (𝓝 0)

Uses 1 · Used by 1

Statement usesLeft-point step process along a Brownian path

Used byItô's formula

Itô's formula

DefinitionLeft-point elementary integrand along a Brownian path#✓fully proved

The left-point elementary integrand ∑_{k < n} g(B (t k / n)) 1_{(t k / n, t (k + 1) / n]} of u ↦ g (B u) on the uniform partition of [0, t], for a measurable g bounded by C and an adapted B.

noncomputable def leftPoint {Ω : Type*} {mΩ : MeasurableSpace Ω} (F : Filtration ℝ≥0 mΩ)
    {B : ℝ≥0 → Ω → ℝ} (hBF : Adapted F B) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ}
    (hgC : ∀ x, |g x| ≤ C) (t : ℝ≥0) (n : ℕ) : ElementaryIntegrand F where
  n := n
  time := fun k ↦ t * k / n
  monotone_time := fun i j hij ↦ by
    have : ((i : ℕ) : ℝ≥0) ≤ (j : ℕ) := by exact_mod_cast hij
    dsimp only
    gcongr
  coeff := fun k ω ↦ g (B (t * (k.castSucc : ℕ) / n) ω)
  measurable_coeff := fun _ ↦ hg.comp (hBF _)
  bound := C
  abs_coeff_le := fun _ _ ↦ hgC _

Uses 1 · Used by 3

Statement usesElementary integrand

Used byItô's formula · Itô integral of the left-point integrand is the left-point sum · Process of the left-point integrand is the left-point step process

TheoremItô integral of the left-point integrand is the left-point sum#✓fully proved

The elementary Itô integral of leftPoint at time t is the left-point Itô sum ∑_{k < n} g(B (t k / n)) (B (t (k + 1) / n) - B (t k / n)).

theorem itoIntegral_leftPoint {Ω : Type*} {mΩ : MeasurableSpace Ω} (F : Filtration ℝ≥0 mΩ)
    {B : ℝ≥0 → Ω → ℝ} (hBF : Adapted F B) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ}
    (hgC : ∀ x, |g x| ≤ C) (t : ℝ≥0) (n : ℕ) (ω : Ω) :
    (leftPoint F hBF hg hgC t n).itoIntegral B t ω = ∑ k ∈ Finset.range n,
      g (B (t * k / n) ω) * (B (t * (k + 1) / n) ω - B (t * k / n) ω)

Uses 2 · Used by 1

Statement usesItô integral of an elementary integrand · Left-point elementary integrand along a Brownian path

Used byItô's formula

TheoremProcess of the left-point integrand is the left-point step process#✓fully proved

The process of leftPoint is leftPointProcess.

theorem toProcess_leftPoint {Ω : Type*} {mΩ : MeasurableSpace Ω} (F : Filtration ℝ≥0 mΩ)
    {B : ℝ≥0 → Ω → ℝ} (hBF : Adapted F B) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ}
    (hgC : ∀ x, |g x| ≤ C) (t : ℝ≥0) (n : ℕ) :
    (leftPoint F hBF hg hgC t n).toProcess = leftPointProcess g B t n

Uses 4 · Used by 1

Statement usesLeft-point elementary integrand along a Brownian path · Elementary integrand as a process · Left-point step process along a Brownian path

Proof usesElementary integrand

Used byItô's formula

TheoremItô's formula#✓fully proved

Itô's formula for Brownian motion: for a Brownian motion B adapted to F with increments independent of the past and jointly measurable in (t, ω), and f of class C² with |f'| ≤ C and |f''| ≤ C, f(B t) = f(B 0) + ∫_0^t f'(B u) dB u + (1/2) ∫_0^t f''(B u) du almost surely, for every t ≥ 0 (Karatzas–Shreve 1991, Theorem 3.3.3). The last integral is a pathwise Riemann integral; it is the integral of a continuous function on almost every path.

theorem ito_formula {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {F : Filtration ℝ≥0 mΩ} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P)
    (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P)
    (hBm : Measurable fun p : ℝ≥0 × Ω ↦ B p.1 p.2)
    {f : ℝ → ℝ} (hf : ContDiff ℝ 2 f) (C : ℝ) (hf1 : ∀ x, |deriv f x| ≤ C)
    (hf2 : ∀ x, |deriv (deriv f) x| ≤ C) (t : ℝ≥0) :
    (fun ω ↦ f (B t ω)) =ᵐ[P]
      fun ω ↦ f (B 0 ω) + itoIntegral P F B (fun u ω' ↦ deriv f (B u ω')) t ω +
        (1 / 2) * ∫ u in (0 : ℝ)..t, deriv (deriv f) (B (Real.toNNReal u) ω)

Uses 20

Statement usesItô integral process

Proof usesElementary integrand · Itô integral of an elementary integrand · Itô integral of the left-point integrand is the left-point sum · Left-point elementary integrand along a Brownian path · Square integrability of the elementary Itô integral · Elementary integrand as a process · Process of the left-point integrand is the left-point step process · Squared \(L^2\) distance between integrands · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Left-point step process along a Brownian path · Restriction to (0, t) preserves joint measurability · Weighted quadratic variation of Brownian motion · Left-point approximation of a Lipschitz function of Brownian motion · Left-point Riemann sums of a continuous function · Second-order Taylor sums along a continuous path · The Itô integral is well defined · Function as an element of \(L^2\) · Weighted quadratic-variation error of Brownian motion

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.