Itô integral

StructureElementary integrand#✓fully proved

An elementary integrand for a filtration F indexed by ℝ≥0: partition times time 0 ≤ ⋯ ≤ time n and coefficients coeff i, bounded by bound and measurable with respect to F (time i), representing the process ∑ i, coeff i 1_{(time i, time (i + 1)]}. Equal consecutive times are allowed (the corresponding interval is empty).

ProbabilityTheory.ElementaryIntegrand · 15 lines

structure ElementaryIntegrand (F : Filtration ℝ≥0 mΩ) where
  /-- The number of partition intervals. -/
  n : ℕ
  /-- The partition times `time 0 ≤ time 1 ≤ ⋯ ≤ time n`. -/
  time : Fin (n + 1) → ℝ≥0
  /-- The partition times are nondecreasing. -/
  monotone_time : Monotone time
  /-- The coefficient on the interval `(time i, time (i + 1)]`. -/
  coeff : Fin n → Ω → ℝ
  /-- Each coefficient is known at the left end of its interval. -/
  measurable_coeff : ∀ i, Measurable[F (time i.castSucc)] (coeff i)
  /-- A uniform bound on the coefficients. -/
  bound : ℝ
  /-- The coefficients are bounded by `bound`. -/
  abs_coeff_le : ∀ i ω, |coeff i ω| ≤ bound

Used by 40

Used byUniform bound on an elementary integrand · Measurability of the \(L^2\) Itô integral · Locality of approximability · Delayed-average approximation of a progressive process · Partition intervals of an elementary integrand are disjoint · Polarized Itô isometry · Itô isometry · Itô isometry, discrete form · Time integral of a squared elementary integrand · Itô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Finite distance between elementary integrands · Itô-approximable process · Density of elementary integrands · Elementary integrands are Itô-approximable · Itô integral of an elementary integrand · Continuous modification · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Elementary integrands · Itô integral agrees with the elementary integral on elementary integrands · Elementary Itô integral vanishes at time zero · Itô isometry · Martingale property · Martingale property of the Itô integral · Elementary integrands are jointly measurable · Square integrability of the elementary Itô integral · Left-point step approximation of a deterministic integrand · Single-step elementary integrand · Convergence of the delayed averages · \(L^2\) convergence of left-point approximations of a continuous function · The Itô integral is well defined · Elementary integrand as a process · Elementary integrand on a partition interval · Process of a single-step elementary integrand · Itô's formula · Left-point elementary integrand along a Brownian path · Process of the left-point integrand is the left-point step process · Covariance of the Wiener integrals · Elementary Itô integrals agree for modifications

TheoremSecond moment of a Brownian increment#✓fully proved

The second moment of a Brownian increment: E[(B v - B r)²] = v - r for r ≤ v.

theorem IsPreBrownianReal.integral_sub_sq {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) {r v : ℝ≥0} (hrv : r ≤ v) :
    P[fun ω ↦ (B v ω - B r ω) ^ 2] = (v : ℝ) - r

Used by 2

Used byPolarized Itô isometry · Itô isometry, discrete form

DefinitionElementary integrand as a process#✓fully proved

The elementary integrand as a process: u ↦ ∑ i, coeff i 1_{(time i, time (i + 1)]}(u).

noncomputable def toProcess (H : ElementaryIntegrand F) (u : ℝ≥0) (ω : Ω) : ℝ :=
  ∑ i, (Set.Ioc (H.time i.castSucc) (H.time i.succ)).indicator (fun _ ↦ H.coeff i ω) u

Uses 1 · Used by 28

Statement usesElementary integrand

Used byUniform bound on an elementary integrand · Measurability of the \(L^2\) Itô integral · Locality of approximability · Polarized Itô isometry · Itô isometry · Time integral of a squared elementary integrand · Itô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Finite distance between elementary integrands · Itô-approximable process · Density of elementary integrands · Elementary integrands are Itô-approximable · Continuous modification · Elementary integrands · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · Elementary integrands are jointly measurable · Convergence of the delayed averages · \(L^2\) convergence of left-point approximations of a continuous function · The Itô integral is well defined · Elementary integrand on a partition interval · Process of a single-step elementary integrand · Itô's formula · Process of the left-point integrand is the left-point step process · Covariance of the Wiener integrals

DefinitionItô integral of an elementary integrand#✓fully proved

The Itô integral of an elementary integrand against a process B: t ↦ ∑ i, coeff i (B (time (i + 1) ∧ t) - B (time i ∧ t)).

def itoIntegral (H : ElementaryIntegrand F) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (ω : Ω) : ℝ :=
  ∑ i, H.coeff i ω * (B (min (H.time i.succ) t) ω - B (min (H.time i.castSucc) t) ω)

Uses 1 · Used by 26

Statement usesElementary integrand

Used byThe Itô form of the Ornstein–Uhlenbeck solution · Measurability of the \(L^2\) Itô integral · Polarized Itô isometry · Itô isometry · Itô isometry, discrete form · Itô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Continuous modification · Wiener's integration by parts · Elementary integrands · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Itô integral of a Riemann step approximation · Elementary integrands · Itô integral agrees with the elementary integral on elementary integrands · Elementary Itô integral vanishes at time zero · Itô isometry · Martingale property · Martingale property of the Itô integral · Square integrability of the elementary Itô integral · Itô–Riemann sums of a deterministic C¹ integrand · The Itô integral is well defined · Itô's formula · Itô integral of the left-point integrand is the left-point sum · The pathwise Langevin solution driven by Brownian motion is Gaussian · Elementary Itô integrals agree for modifications

DefinitionSingle-step elementary integrand#✓fully proved

The elementary integrand ξ 1_{(a, b]} for a ≤ b and an F a-measurable ξ bounded by C.

def single (a b : ℝ≥0) (hab : a ≤ b) (ξ : Ω → ℝ) (hξ : Measurable[F a] ξ) (C : ℝ)
    (hξC : ∀ ω, |ξ ω| ≤ C) : ElementaryIntegrand F where
  n := 1
  time := ![a, b]
  monotone_time := by
    refine Fin.monotone_iff_le_succ.mpr fun i ↦ ?_
    fin_cases i
    simpa using hab
  coeff := fun _ ↦ ξ
  measurable_coeff := fun i ↦ by obtain rfl : i = 0 := Subsingleton.elim _ _; exact hξ
  bound := C
  abs_coeff_le := fun _ ↦ hξC

Uses 1 · Used by 3

Statement usesElementary integrand

Used byElementary integrands · Elementary integrands · Process of a single-step elementary integrand

TheoremProcess of a single-step elementary integrand#✓fully proved

The process of single a b hab ξ hξ C hξC is u ↦ ξ 1_{(a, b]}(u).

theorem toProcess_single (a b : ℝ≥0) (hab : a ≤ b) (ξ : Ω → ℝ) (hξ : Measurable[F a] ξ)
    (C : ℝ) (hξC : ∀ ω, |ξ ω| ≤ C) :
    (single a b hab ξ hξ C hξC).toProcess =
      fun u ω ↦ (Set.Ioc a b).indicator (fun _ ↦ ξ ω) u

Uses 3 · Used by 1

Statement usesSingle-step elementary integrand · Elementary integrand as a process

Proof usesElementary integrand

Used byElementary integrands

TheoremElementary integrands#✓fully proved

The Itô integral of ξ 1_{(a, b]} is ξ (B (b ∧ t) - B (a ∧ t)) (Karatzas–Shreve 1991, Section 3.2.A); this holds for every process B and every ω, by definition.

theorem itoIntegral_single (a b : ℝ≥0) (hab : a ≤ b) (ξ : Ω → ℝ) (hξ : Measurable[F a] ξ)
    (C : ℝ) (hξC : ∀ ω, |ξ ω| ≤ C) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (ω : Ω) :
    (single a b hab ξ hξ C hξC).itoIntegral B t ω =
      ξ ω * (B (min b t) ω - B (min a t) ω)

Uses 3 · Used by 1

Statement usesItô integral of an elementary integrand · Single-step elementary integrand

Proof usesElementary integrand

Used byElementary integrands

TheoremElementary Itô integral vanishes at time zero#✓fully proved

The elementary Itô integral vanishes at time 0.

@[simp]
theorem itoIntegral_zero (H : ElementaryIntegrand F) (B : ℝ≥0 → Ω → ℝ) :
    H.itoIntegral B 0 = 0

Uses 2

Statement usesElementary integrand · Itô integral of an elementary integrand

TheoremItô isometry, discrete form#✓fully proved

For a pre-Brownian motion B adapted to F whose increments B t - B s are independent of F s, E[(∫_0^t H dB)²] = ∑ i, E[ξ_i²] (t_{i+1} ∧ t - t_i ∧ t).

theorem integral_itoIntegral_sq_eq_sum (H : ElementaryIntegrand F) {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) (t : ℝ≥0) :
    P[fun ω ↦ H.itoIntegral B t ω ^ 2] =
      ∑ i, P[fun ω ↦ H.coeff i ω ^ 2] *
        ((min (H.time i.succ) t : ℝ) - (min (H.time i.castSucc) t : ℝ))

Uses 3 · Used by 1

Statement usesElementary integrand · Itô integral of an elementary integrand

Proof usesSecond moment of a Brownian increment

Used byItô isometry

TheoremPartition intervals of an elementary integrand are disjoint#✓fully proved

The partition intervals of an elementary integrand are pairwise disjoint.

theorem disjoint_Ioc_time
    (H : ElementaryIntegrand F) {i j : Fin H.n} (hij : i ≠ j) :
    Disjoint (Set.Ioc (H.time i.castSucc) (H.time i.succ))
      (Set.Ioc (H.time j.castSucc) (H.time j.succ))

Uses 1 · Used by 2

Statement usesElementary integrand

Used byTime integral of a squared elementary integrand · Elementary integrand on a partition interval

TheoremElementary integrand on a partition interval#✓fully proved

On its i-th interval, an elementary integrand equals its i-th coefficient.

theorem toProcess_eq_of_mem (H : ElementaryIntegrand F) {i : Fin H.n} {u : ℝ≥0}
    (hu : u ∈ Set.Ioc (H.time i.castSucc) (H.time i.succ)) (ω : Ω) :
    H.toProcess u ω = H.coeff i ω

Uses 3 · Used by 2

Statement usesElementary integrand · Elementary integrand as a process

Proof usesPartition intervals of an elementary integrand are disjoint

Used byConvergence of the delayed averages · \(L^2\) convergence of left-point approximations of a continuous function

TheoremTime integral of a squared elementary integrand#✓fully proved

The time integral of the squared elementary integrand, path by path: ∫_0^t H_u² du = ∑ i, ξ_i² (t_{i+1} ∧ t - t_i ∧ t).

theorem integral_toProcess_sq (H : ElementaryIntegrand F) (t : ℝ≥0) (ω : Ω) :
    ∫ u in (0 : ℝ)..t, H.toProcess (Real.toNNReal u) ω ^ 2 =
      ∑ i, H.coeff i ω ^ 2 *
        ((min (H.time i.succ) t : ℝ) - (min (H.time i.castSucc) t : ℝ))

Uses 3 · Used by 1

Statement usesElementary integrand · Elementary integrand as a process

Proof usesPartition intervals of an elementary integrand are disjoint

Used byItô isometry

TheoremItô isometry#✓fully proved

Itô isometry for elementary integrands: for a pre-Brownian motion B adapted to F whose increments B t - B s are independent of F s, E[(∫_0^t H dB)²] = E ∫_0^t H_u² du (Karatzas–Shreve 1991, Section 3.2.A).

theorem integral_itoIntegral_sq (H : ElementaryIntegrand F) {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) (t : ℝ≥0) :
    P[fun ω ↦ H.itoIntegral B t ω ^ 2] =
      P[fun ω ↦ ∫ u in (0 : ℝ)..t, H.toProcess (Real.toNNReal u) ω ^ 2]

Uses 5

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process

Proof usesItô isometry, discrete form · Time integral of a squared elementary integrand

TheoremMartingale property#✓fully proved

For a pre-Brownian motion B adapted to F whose increments B t - B s are independent of F s, the elementary Itô integral t ↦ ∫_0^t H dB is an F-martingale.

theorem martingale_itoIntegral (H : ElementaryIntegrand F) {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) :
    Martingale (H.itoIntegral B) F P

Uses 2 · Used by 3

Statement usesElementary integrand · Itô integral of an elementary integrand

Used byMeasurability of the \(L^2\) Itô integral · Continuous modification · Martingale property of the Itô integral

TheoremPolarized Itô isometry#✓fully proved

Polarized Itô isometry for elementary integrands: for a pre-Brownian motion B adapted to F whose increments B t - B s are independent of F s, and two elementary integrands H, K (with possibly different partitions), E[(∫_0^t H dB) (∫_0^t K dB)] = E ∫_0^t H_u K_u du.

theorem integral_itoIntegral_mul (H K : ElementaryIntegrand F) {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) (t : ℝ≥0) :
    P[fun ω ↦ H.itoIntegral B t ω * K.itoIntegral B t ω] =
      P[fun ω ↦ ∫ u in (0 : ℝ)..t, H.toProcess (Real.toNNReal u) ω *
        K.toProcess (Real.toNNReal u) ω]

Uses 4 · Used by 1

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process

Proof usesSecond moment of a Brownian increment

Used byItô isometry for elementary integrands

TheoremRiemann–Stieltjes integration by parts, uniform partitions#✓fully proved

For a C¹ function g, a continuous path w and t ≥ 0, the left-point sums ∑_{k < n} g (t k / n) (w (t (k + 1) / n) - w (t k / n)) converge, as n → ∞, to g t w t - g 0 w 0 - ∫_0^t g' w.

theorem tendsto_sum_mul_sub_uniform {g : ℝ → ℝ} (hg : ContDiff ℝ 1 g) {w : ℝ → ℝ}
    (hw : Continuous w) {t : ℝ} (ht : 0 ≤ t) :
    Tendsto (fun n : ℕ ↦ ∑ k ∈ Finset.range n,
        g (t * k / n) * (w (t * (k + 1) / n) - w (t * k / n))) atTop
      (𝓝 (g t * w t - g 0 * w 0 - ∫ u in (0 : ℝ)..t, deriv g u * w u))

Used by 1

Used byItô–Riemann sums of a deterministic C¹ integrand

DefinitionLeft-point step approximation of a deterministic integrand#✓fully proved

The left-point step approximation ∑_{k < n} g (t k / n) 1_{(t k / n, t (k + 1) / n]} of a deterministic g on the uniform partition of [0, t] into n cells, as an elementary integrand for any filtration F (deterministic coefficients are measurable for every σ-algebra).

noncomputable def riemann (F : Filtration ℝ≥0 mΩ) (g : ℝ → ℝ) (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 ((t * (k.castSucc : ℕ) / n : ℝ≥0) : ℝ)
  measurable_coeff := fun _ ↦ measurable_const
  bound := ∑ k : Fin n, |g ((t * (k.castSucc : ℕ) / n : ℝ≥0) : ℝ)|
  abs_coeff_le := fun k _ ↦
    Finset.single_le_sum (f := fun k : Fin n ↦ |g ((t * (k.castSucc : ℕ) / n : ℝ≥0) : ℝ)|)
      (fun _ _ ↦ abs_nonneg _) (Finset.mem_univ k)

Uses 1 · Used by 7

Statement usesElementary integrand

Used byThe Itô form of the Ornstein–Uhlenbeck solution · Wiener's integration by parts · Itô integral of a Riemann step approximation · \(L^2\) convergence of left-point approximations of a continuous function · Itô–Riemann sums of a deterministic C¹ integrand · Covariance of the Wiener integrals · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremItô integral of a Riemann step approximation#✓fully proved

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

theorem itoIntegral_riemann (F : Filtration ℝ≥0 mΩ) (g : ℝ → ℝ) (t : ℝ≥0) (n : ℕ)
    (B : ℝ≥0 → Ω → ℝ) (ω : Ω) :
    (riemann F g t n).itoIntegral B t ω = ∑ k ∈ Finset.range n,
      g (t * k / n) *
        (B (Real.toNNReal (t * (k + 1) / n)) ω - B (Real.toNNReal (t * k / n)) ω)

Uses 2 · Used by 2

Statement usesItô integral of an elementary integrand · Left-point step approximation of a deterministic integrand

Used byItô–Riemann sums of a deterministic C¹ integrand · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremItô–Riemann sums of a deterministic C¹ integrand#✓fully proved

Along every continuous path of B, the elementary Itô integrals at time t of the left-point approximations of g converge to Wiener's integration-by-parts expression g t B t - g 0 B 0 - ∫_0^t g'(u) B u du.

theorem tendsto_itoIntegral_riemann (F : Filtration ℝ≥0 mΩ) {g : ℝ → ℝ} (hg : ContDiff ℝ 1 g)
    {B : ℝ≥0 → Ω → ℝ} {ω : Ω} (hω : Continuous (B · ω)) (t : ℝ≥0) :
    Tendsto (fun n ↦ (riemann F g t n).itoIntegral B t ω) atTop
      (𝓝 (g t * B t ω - g 0 * B 0 ω - ∫ u in (0 : ℝ)..t, deriv g u * B u.toNNReal ω))

Uses 4 · Used by 2

Statement usesItô integral of an elementary integrand · Left-point step approximation of a deterministic integrand

Proof usesItô integral of a Riemann step approximation · Riemann–Stieltjes integration by parts, uniform partitions

Used byThe Itô form of the Ornstein–Uhlenbeck solution · Wiener's integration by parts

TheoremOrnstein–Uhlenbeck path solution by integration by parts#✓fully proved

The pathwise Ornstein–Uhlenbeck solution in integration-by-parts form: with g u = e^{θu}, ouPathSolution θ σ x₀ w t = e^{-θt} x₀ + σ e^{-θt} (g t w t - g 0 w 0 - ∫_0^t g'(u) w u du), for any path w and any real θ, σ, x₀, t.

theorem ouPathSolution_eq_integration_by_parts (θ σ x₀ : ℝ) (w : ℝ → ℝ) (t : ℝ) :
    ouPathSolution θ σ x₀ w t = exp (-θ * t) * x₀ + σ * exp (-θ * t) *
      (exp (θ * t) * w t - exp (θ * 0) * w 0 -
        ∫ u in (0 : ℝ)..t, deriv (fun u ↦ exp (θ * u)) u * w u)

Uses 1 · Used by 2

Statement usesPathwise solution of the Langevin equation

Used byThe Itô form of the Ornstein–Uhlenbeck solution · The Ornstein–Uhlenbeck solution in Itô form

TheoremThe Itô form of the Ornstein–Uhlenbeck solution#✓fully proved

For a Brownian motion B, almost surely, for every t ≥ 0 and every initial value X₀, the Itô–Riemann sums e^{-θt} X₀ + σ e^{-θt} ∑_{k < n} e^{θ t k / n} (B (t (k + 1) / n) - B (t k / n)) of e^{-θt} X₀ + σ ∫_0^t e^{-θ(t-s)} dB_s converge to the pathwise solution ouPathSolution (any real θ, σ).

theorem IsBrownianReal.ae_tendsto_ou_itoIntegral_riemann {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsBrownianReal B P) (F : Filtration ℝ≥0 mΩ)
    (θ σ : ℝ) (X₀ : Ω → ℝ) :
    ∀ᵐ ω ∂P, ∀ t : ℝ≥0, Tendsto (fun n ↦ exp (-θ * t) * X₀ ω + σ * exp (-θ * t) *
        (ElementaryIntegrand.riemann F (fun u ↦ exp (θ * u)) t n).itoIntegral B t ω)
      atTop (𝓝 (ouPathSolution θ σ (X₀ ω) (fun u ↦ B u.toNNReal ω) t))

Uses 5 · Used by 1

Statement usesItô integral of an elementary integrand · Left-point step approximation of a deterministic integrand · Pathwise solution of the Langevin equation

Proof usesItô–Riemann sums of a deterministic C¹ integrand · Ornstein–Uhlenbeck path solution by integration by parts

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian

DefinitionSquared \(L^2\) distance between integrands#✓fully proved

The squared L²(P ⊗ du) distance on (0, t] × Ω between two processes, in ℝ≥0∞: ∫⁻ ω, ∫⁻ u in (0, t], |H u ω - K u ω|² du dP.

noncomputable def integrandDist (P : Measure Ω) (H K : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) : ℝ≥0∞ :=
  ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω - K u.toNNReal ω‖ₑ ^ 2) ∂P

Used by 26

Used byMeasurability of the \(L^2\) Itô integral · Locality of approximability · Itô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Integrand distance as a squared \(L^2\) seminorm · Quasi-triangle inequality for the integrand distance · Finite distance between elementary integrands · Integrand distance depends only on times in (0, t) · Itô-approximable process · Density of elementary integrands · Elementary integrands are Itô-approximable · Linearity (additivity) · Continuous modification · Difference isometry · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Linearity (homogeneity) · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · Convergence of the delayed averages · \(L^2\) convergence of left-point approximations of a continuous function · Truncation · The Itô integral is well defined · Itô's formula · Covariance of the Wiener integrals

DefinitionRestriction of a process to the time interval (0, t)#✓fully proved

The process H with its values at times outside (0, t] set to 0. Only the values at times in (0, t] enter the Itô integral at time t.

noncomputable def restrictIoc (H : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) (u : ℝ≥0) (ω : Ω) : ℝ :=
  (Set.Ioc 0 t).indicator (fun v ↦ H v ω) u

Used by 16

Used byMeasurability of the \(L^2\) Itô integral · Locality of approximability · Itô isometry for Itô-approximable integrands · Integrand distance as a squared \(L^2\) seminorm · Integrand distance depends only on times in (0, t) · Itô-approximable process · Density of elementary integrands · Elementary integrands are Itô-approximable · Continuous modification · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Itô isometry · Martingale property of the Itô integral · Restriction to (0, t) preserves joint measurability · The Itô integral is well defined · Covariance of the Wiener integrals

DefinitionItô-approximable process#✓fully proved

A process H is Itô-approximable on [0, t] for the filtration F if it is jointly measurable on (0, t] × Ω and is the L²(P ⊗ du)-limit on (0, t] × Ω of elementary integrands. Neither condition involves the values of H at time 0 or after t.

def IsItoApproximable (P : Measure Ω) (F : Filtration ℝ≥0 mΩ) (H : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) :
    Prop :=
  Measurable (fun p : ℝ × Ω ↦ restrictIoc H t p.1.toNNReal p.2) ∧
    ∃ Hn : ℕ → ElementaryIntegrand F,
      Tendsto (fun n ↦ integrandDist P (Hn n).toProcess H t) atTop (𝓝 0)

Uses 4 · Used by 14

Statement usesElementary integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Restriction of a process to the time interval (0, t)

Used byMeasurability of the \(L^2\) Itô integral · Locality of approximability · Itô isometry for Itô-approximable integrands · Density of elementary integrands · Elementary integrands are Itô-approximable · Linearity (additivity) · Continuous modification · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Linearity (homogeneity) · Itô isometry · Martingale property of the Itô integral · The Itô integral is well defined · Covariance of the Wiener integrals

DefinitionFunction as an element of \(L^2\)#✓fully proved

A function as an element of L²(P), or 0 if it is not square integrable.

noncomputable def toL2 (P : Measure Ω) (f : Ω → ℝ) : Lp ℝ 2 P :=
  if h : MemLp f 2 P then h.toLp f else 0

Used by 13

Used byMeasurability of the \(L^2\) Itô integral · Itô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Continuous modification · Wiener's integration by parts · Itô integral as an element of \(L^2\) · Locality of the Itô integral · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · The Itô integral is well defined · Itô's formula · The pathwise Langevin solution driven by Brownian motion is Gaussian

DefinitionItô integral as an element of \(L^2\)#✓fully proved

The Itô integral ∫_0^t H dB as an element of L²(P): the L² limit of the elementary Itô integrals of an approximating sequence of elementary integrands when H is Itô-approximable on [0, t], and 0 otherwise.

noncomputable def itoIntegralL2 (P : Measure Ω) (F : Filtration ℝ≥0 mΩ) (B H : ℝ≥0 → Ω → ℝ)
    (t : ℝ≥0) : Lp ℝ 2 P :=
  if h : IsItoApproximable P F H t then
    limUnder atTop fun n ↦ toL2 P ((h.2.choose n).itoIntegral B t)
  else 0

Uses 7 · Used by 17

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process · Itô-approximable process · Squared \(L^2\) distance between integrands · Restriction of a process to the time interval (0, t) · Function as an element of \(L^2\)

Used byMeasurability of the \(L^2\) Itô integral · Itô isometry for Itô-approximable integrands · Itô integral process · Linearity (additivity) · Itô integral process is a version of the \(L^2\) integral · Continuous modification · Wiener's integration by parts · Locality of the Itô integral · Linearity (homogeneity) · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · Square integrability of the Itô integral · The Itô integral is well defined · Itô's formula · Covariance of the Wiener integrals · The pathwise Langevin solution driven by Brownian motion is Gaussian

DefinitionItô integral process#✓fully proved

The Itô integral t ↦ ∫_0^t H dB as a real process: an F t-strongly measurable version of itoIntegralL2 P F B H t when one exists (which is the case under the hypotheses of the theorems below), and a representative of itoIntegralL2 P F B H t otherwise.

noncomputable def itoIntegral (P : Measure Ω) (F : Filtration ℝ≥0 mΩ) (B H : ℝ≥0 → Ω → ℝ)
    (t : ℝ≥0) : Ω → ℝ :=
  if h : AEStronglyMeasurable[F t] (itoIntegralL2 P F B H t) P then h.mk _
  else itoIntegralL2 P F B H t

Uses 1 · Used by 19

Statement usesItô integral as an element of \(L^2\)

Used byLinearity (additivity) · Linearity (additivity) · Itô integral process is a version of the \(L^2\) integral · Continuous modification · Wiener's integration by parts · Elementary integrands · Difference isometry · Difference isometry · Linearity (homogeneity) · Linearity (homogeneity) · Itô integral agrees with the elementary integral on elementary integrands · The Ornstein–Uhlenbeck solution in Itô form · Itô isometry · Itô isometry for progressive integrands · Martingale property of the Itô integral · Martingale property for progressive integrands · Square integrability of the Itô integral · Itô's formula · Covariance of the Wiener integrals

TheoremItô integral process is a version of the \(L^2\) integral#✓fully proved

The Itô integral process is almost surely equal to itoIntegralL2 at each time.

theorem itoIntegral_ae_eq (P : Measure Ω) (F : Filtration ℝ≥0 mΩ) (B H : ℝ≥0 → Ω → ℝ)
    (t : ℝ≥0) : itoIntegral P F B H t =ᵐ[P] itoIntegralL2 P F B H t

Uses 2 · Used by 10

Statement usesItô integral process · Itô integral as an element of \(L^2\)

Used byLinearity (additivity) · Continuous modification · Wiener's integration by parts · Linearity (homogeneity) · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · Square integrability of the Itô integral · Itô's formula · Covariance of the Wiener integrals

TheoremRestriction to (0, t) preserves joint measurability#✓fully proved

Restricting a jointly measurable process to the times (0, t] keeps it jointly measurable.

theorem measurable_restrictIoc {H : ℝ≥0 → Ω → ℝ}
    (hH : Measurable fun p : ℝ × Ω ↦ H p.1.toNNReal p.2) (t : ℝ≥0) :
    Measurable fun p : ℝ × Ω ↦ restrictIoc H t p.1.toNNReal p.2

Uses 1 · Used by 12

Statement usesRestriction of a process to the time interval (0, t)

Used byItô isometry for Itô-approximable integrands · Density of elementary integrands · Elementary integrands are Itô-approximable · Continuous modification · Wiener's integration by parts · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · The Itô integral is well defined · Itô's formula · Covariance of the Wiener integrals · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremIntegrand distance depends only on times in (0, t)#✓fully proved

integrandDist P X Y t only depends on X and Y at times in (0, t].

theorem integrandDist_restrictIoc (P : Measure Ω) (X Y : ℝ≥0 → Ω → ℝ) (t : ℝ≥0) :
    integrandDist P (restrictIoc X t) (restrictIoc Y t) t = integrandDist P X Y t

Uses 2 · Used by 4

Statement usesSquared \(L^2\) distance between integrands · Restriction of a process to the time interval (0, t)

Used byLocality of approximability · Integrand distance as a squared \(L^2\) seminorm · Locality of the Itô integral · The Itô integral is well defined

TheoremLocality of approximability#✓fully proved

Itô-approximability on [0, t] only depends on the integrand at times in (0, t].

theorem IsItoApproximable.congr {P : Measure Ω} {F : Filtration ℝ≥0 mΩ} {H K : ℝ≥0 → Ω → ℝ}
    {t : ℝ≥0} (h : IsItoApproximable P F H t) (hHK : ∀ u ∈ Set.Ioc 0 t, ∀ ω, H u ω = K u ω) :
    IsItoApproximable P F K t

Uses 6 · Used by 1

Statement usesItô-approximable process

Proof usesElementary integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Integrand distance depends only on times in (0, t) · Restriction of a process to the time interval (0, t)

Used byLocality of the Itô integral

TheoremElementary integrands are jointly measurable#✓fully proved

An elementary integrand is jointly measurable in (u, ω) (reading u : ℝ through Real.toNNReal).

theorem measurable_toProcess (H : ElementaryIntegrand F) :
    Measurable (fun p : ℝ × Ω ↦ H.toProcess p.1.toNNReal p.2)

Uses 2 · Used by 9

Statement usesElementary integrand · Elementary integrand as a process

Used byItô isometry for elementary integrands · Itô isometry for Itô-approximable integrands · Finite distance between elementary integrands · Density of elementary integrands · Elementary integrands are Itô-approximable · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Convergence of the delayed averages · The Itô integral is well defined

TheoremUniform bound on an elementary integrand#✓fully proved

An elementary integrand with n intervals is bounded by n * bound.

theorem abs_toProcess_le (H : ElementaryIntegrand F) (u : ℝ≥0) (ω : Ω) :
    |H.toProcess u ω| ≤ H.n * H.bound

Uses 2 · Used by 2

Statement usesElementary integrand · Elementary integrand as a process

Used byItô isometry for elementary integrands · Finite distance between elementary integrands

TheoremSquare integrability of the elementary Itô integral#✓fully proved

The elementary Itô integral against a pre-Brownian motion is square integrable.

theorem memLp_itoIntegral (H : ElementaryIntegrand F) {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (t : ℝ≥0) :
    MemLp (H.itoIntegral B t) 2 P

Uses 2 · Used by 8

Statement usesElementary integrand · Itô integral of an elementary integrand

Used byMeasurability of the \(L^2\) Itô integral · Itô isometry for elementary integrands · Continuous modification · Wiener's integration by parts · Itô integral agrees with the elementary integral on elementary integrands · Martingale property of the Itô integral · Itô's formula · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremFinite distance between elementary integrands#✓fully proved

The L²(P ⊗ du) distance between two elementary integrands is finite.

theorem integrandDist_ne_top (H K : ElementaryIntegrand F) {P : Measure Ω} [IsFiniteMeasure P]
    (t : ℝ≥0) : integrandDist P H.toProcess K.toProcess t ≠ ⊤

Uses 5 · Used by 2

Statement usesElementary integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands

Proof usesUniform bound on an elementary integrand · Elementary integrands are jointly measurable

Used byItô isometry for elementary integrands · Itô isometry for Itô-approximable integrands

TheoremItô isometry for elementary integrands#✓fully proved

integrandDist of two elementary integrands is the squared L²(P) distance of their Itô integrals.

theorem integrandDist_eq_dist_sq (H K : ElementaryIntegrand F) {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) (t : ℝ≥0) :
    integrandDist P H.toProcess K.toProcess t =
      ENNReal.ofReal (dist (toL2 P (H.itoIntegral B t)) (toL2 P (K.itoIntegral B t)) ^ 2)

Uses 10 · Used by 3

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Function as an element of \(L^2\)

Proof usesUniform bound on an elementary integrand · Polarized Itô isometry · Finite distance between elementary integrands · Elementary integrands are jointly measurable · Square integrability of the elementary Itô integral

Used byItô isometry for Itô-approximable integrands · Itô isometry · The Itô integral is well defined

TheoremQuasi-triangle inequality for the integrand distance#✓fully proved

Pointwise |x - y|² ≤ 2 |x - z|² + 2 |y - z|², integrated: a quasi-triangle inequality for integrandDist between jointly measurable processes.

theorem integrandDist_le {P : Measure Ω} {X Y Z : ℝ≥0 → Ω → ℝ}
    (hX : Measurable fun p : ℝ × Ω ↦ X p.1.toNNReal p.2)
    (hY : Measurable fun p : ℝ × Ω ↦ Y p.1.toNNReal p.2)
    (hZ : Measurable fun p : ℝ × Ω ↦ Z p.1.toNNReal p.2) (t : ℝ≥0) :
    integrandDist P X Y t ≤ 2 * integrandDist P X Z t + 2 * integrandDist P Y Z t

Uses 1 · Used by 4

Statement usesSquared \(L^2\) distance between integrands

Used byDensity of elementary integrands · Linearity (additivity) · Difference isometry · The Itô integral is well defined

TheoremThe Itô integral is well defined#✓fully proved

For a pre-Brownian motion B adapted to F with increments independent of the past, an H jointly measurable on (0, t] × Ω, and any sequence of elementary integrands Kn converging to H in L²(P ⊗ du) on (0, t] × Ω, the elementary Itô integrals of Kn converge in L²(P) to itoIntegralL2 P F B H t.

theorem tendsto_toL2_itoIntegral {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} {t : ℝ≥0}
    (hH : Measurable fun p : ℝ × Ω ↦ restrictIoc H t p.1.toNNReal p.2)
    {Kn : ℕ → ElementaryIntegrand F}
    (hK : Tendsto (fun n ↦ integrandDist P (Kn n).toProcess H t) atTop (𝓝 0)) :
    Tendsto (fun n ↦ toL2 P ((Kn n).itoIntegral B t)) atTop (𝓝 (itoIntegralL2 P F B H t))

Uses 13 · Used by 10

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Itô integral as an element of \(L^2\) · Restriction of a process to the time interval (0, t) · Function as an element of \(L^2\)

Proof usesItô isometry for elementary integrands · Elementary integrands are jointly measurable · Itô-approximable process · Quasi-triangle inequality for the integrand distance · Integrand distance depends only on times in (0, t) · Restriction to (0, t) preserves joint measurability

Used byMeasurability of the \(L^2\) Itô integral · Itô isometry for Itô-approximable integrands · Continuous modification · Wiener's integration by parts · Locality of the Itô integral · Itô integral agrees with the elementary integral on elementary integrands · Itô isometry · Martingale property of the Itô integral · Itô's formula · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremLocality of the Itô integral#✓fully proved

The Itô integral at time t only depends on the integrand at times in (0, t].

theorem itoIntegralL2_congr {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H K : ℝ≥0 → Ω → ℝ} {t : ℝ≥0} (hHK : ∀ u ∈ Set.Ioc 0 t, ∀ ω, H u ω = K u ω) :
    itoIntegralL2 P F B H t = itoIntegralL2 P F B K t

Uses 11

Statement usesItô integral as an element of \(L^2\)

Proof usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process · Itô-approximable process · Locality of approximability · Squared \(L^2\) distance between integrands · Integrand distance depends only on times in (0, t) · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

TheoremElementary integrands are Itô-approximable#✓fully proved

An elementary integrand is Itô-approximable on every [0, t] (by itself).

theorem isItoApproximable_toProcess {F : Filtration ℝ≥0 mΩ} (P : Measure Ω)
    (K : ElementaryIntegrand F) (t : ℝ≥0) : IsItoApproximable P F K.toProcess t

Uses 7

Statement usesElementary integrand · Elementary integrand as a process · Itô-approximable process

Proof usesElementary integrands are jointly measurable · Squared \(L^2\) distance between integrands · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t)

TheoremItô integral agrees with the elementary integral on elementary integrands#✓fully proved

On an elementary integrand, the Itô integral agrees almost surely with the elementary Itô integral.

theorem itoIntegral_toProcess_ae_eq {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) (K : ElementaryIntegrand F) (t : ℝ≥0) :
    itoIntegral P F B K.toProcess t =ᵐ[P] K.itoIntegral B t

Uses 12 · Used by 1

Statement usesElementary integrand · Itô integral of an elementary integrand · Elementary integrand as a process · Itô integral process

Proof usesElementary integrands are jointly measurable · Square integrability of the elementary Itô integral · 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 · Restriction to (0, t) preserves joint measurability · The Itô integral is well defined · Function as an element of \(L^2\)

Used byElementary integrands

TheoremElementary integrands#✓fully proved

For a ≤ b and a bounded F a-measurable ξ, the Itô integral of ξ 1_{(a, b]} against a pre-Brownian motion B adapted to F with increments independent of the past is ξ (B (b ∧ t) - B (a ∧ t)) almost surely (Karatzas–Shreve 1991, Section 3.2.A).

theorem itoIntegral_indicator_Ioc {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {a b : ℝ≥0} (hab : a ≤ b) {ξ : Ω → ℝ} (hξ : Measurable[F a] ξ) (C : ℝ)
    (hξC : ∀ ω, |ξ ω| ≤ C) (t : ℝ≥0) :
    itoIntegral P F B (fun u ω ↦ Set.indicator (Set.Ioc a b) (fun _ ↦ ξ ω) u) t =ᵐ[P]
      fun ω ↦ ξ ω * (B (min b t) ω - B (min a t) ω)

Uses 7

Statement usesItô integral process

Proof usesItô integral of an elementary integrand · Elementary integrands · Single-step elementary integrand · Elementary integrand as a process · Process of a single-step elementary integrand · Itô integral agrees with the elementary integral on elementary integrands

Theorem\(L^2\) convergence of left-point approximations of a continuous function#✓fully proved

The left-point approximations of a continuous deterministic g converge to g in L²(P ⊗ du) on (0, t] × Ω.

theorem tendsto_integrandDist_riemann {F : Filtration ℝ≥0 mΩ} {P : Measure Ω}
    [IsProbabilityMeasure P] {g : ℝ → ℝ} (hg : Continuous g) (t : ℝ≥0) :
    Tendsto (fun n ↦ integrandDist P (ElementaryIntegrand.riemann F g t n).toProcess
      (fun u _ ↦ g u) t) atTop (𝓝 0)

Uses 5 · Used by 3

Statement usesLeft-point step approximation of a deterministic integrand · Elementary integrand as a process · Squared \(L^2\) distance between integrands

Proof usesElementary integrand · Elementary integrand on a partition interval

Used byWiener's integration by parts · Covariance of the Wiener integrals · The pathwise Langevin solution driven by Brownian motion is Gaussian

TheoremWiener's integration by parts#✓fully proved

For a Brownian motion B adapted to F with increments independent of the past and a deterministic C¹ integrand g, the Itô integral is ∫_0^t g dB = g t B t - g 0 B 0 - ∫_0^t g'(u) B u du almost surely (Karatzas–Shreve 1991, Section 3.3; the right side is a pathwise Riemann integral).

theorem itoIntegral_deterministic_eq {F : Filtration ℝ≥0 mΩ} {P : Measure Ω}
    {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) {g : ℝ → ℝ} (hg : ContDiff ℝ 1 g) (t : ℝ≥0) :
    itoIntegral P F B (fun u _ ↦ g u) t =ᵐ[P]
      fun ω ↦ g t * B t ω - g 0 * B 0 ω -
        ∫ u in (0 : ℝ)..t, deriv g u * B (Real.toNNReal u) ω

Uses 11 · Used by 1

Statement usesItô integral process

Proof usesItô integral of an elementary integrand · Square integrability of the elementary Itô integral · Left-point step approximation of a deterministic integrand · Itô–Riemann sums of a deterministic C¹ integrand · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Restriction to (0, t) preserves joint measurability · \(L^2\) convergence of left-point approximations of a continuous function · The Itô integral is well defined · Function as an element of \(L^2\)

Used byThe Ornstein–Uhlenbeck solution in Itô form

TheoremThe Ornstein–Uhlenbeck solution in Itô form#✓fully proved

For a Brownian motion B adapted to F with increments independent of the past, any initial value X₀ and any real θ, σ, the Itô form e^{-θt} X₀ + σ e^{-θt} ∫_0^t e^{θs} dB_s = e^{-θt} X₀ + σ ∫_0^t e^{-θ(t-s)} dB_s of the solution of dX = -θ X dt + σ dB (Karatzas–Shreve 1991, Section 5.6) agrees almost surely with the pathwise solution ouPathSolution, which solves X t = X₀ - θ ∫_0^t X + σ (B t - B 0) path by path (ProbabilityTheory.ouPathSolution_integral_eq).

theorem ito_ou_solution_eq_ouPathSolution {F : Filtration ℝ≥0 mΩ} {P : Measure Ω}
    {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) (θ σ : ℝ) (X₀ : Ω → ℝ) (t : ℝ≥0) :
    (fun ω ↦ exp (-θ * t) * X₀ ω +
        σ * exp (-θ * t) * itoIntegral P F B (fun u _ ↦ exp (θ * u)) t ω) =ᵐ[P]
      fun ω ↦ ouPathSolution θ σ (X₀ ω) (fun u ↦ B (Real.toNNReal u) ω) t

Uses 4

Statement usesItô integral process · Pathwise solution of the Langevin equation

Proof usesWiener's integration by parts · Ornstein–Uhlenbeck path solution by integration by parts

TheoremMeasurability of the \(L^2\) Itô integral#✓fully proved

The L² Itô integral is (almost surely equal to) an F t-measurable function.

theorem aestronglyMeasurable_itoIntegralL2 {F : Filtration ℝ≥0 mΩ} {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} {t : ℝ≥0} (hH : IsItoApproximable P F H t) :
    AEStronglyMeasurable[F t] (itoIntegralL2 P F B H t) P

Uses 11 · Used by 1

Statement usesItô-approximable process · Itô integral as an element of \(L^2\)

Proof usesElementary integrand · Itô integral of an elementary integrand · Martingale property · Square integrability of the elementary Itô integral · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

Used byMartingale property of the Itô integral

TheoremMartingale property of the Itô integral#✓fully proved

For a pre-Brownian motion B adapted to F with increments independent of the past and an integrand H that is Itô-approximable on every [0, t], the Itô integral t ↦ ∫_0^t H dB is an F-martingale (Karatzas–Shreve 1991, Proposition 3.2.10).

theorem martingale_itoIntegral {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} (hH : ∀ t, IsItoApproximable P F H t) :
    Martingale (itoIntegral P F B H) F P

Uses 15 · Used by 2

Statement usesItô-approximable process · Itô integral process

Proof usesElementary integrand · Itô integral of an elementary integrand · Martingale property · Square integrability of the elementary Itô integral · Elementary integrand as a process · Measurability of the \(L^2\) Itô integral · 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 · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

Used byMartingale property for progressive integrands · Covariance of the Wiener integrals

TheoremIntegrand distance as a squared \(L^2\) seminorm#✓fully proved

The integrand distance on (0, t] is the square of the L² seminorm on Ω × (0, t].

theorem integrandDist_eq_eLpNorm_sq {P : Measure Ω} [IsFiniteMeasure P]
    {X Y : ℝ≥0 → Ω → ℝ} {t : ℝ≥0}
    (hX : Measurable fun p : ℝ × Ω ↦ restrictIoc X t p.1.toNNReal p.2)
    (hY : Measurable fun p : ℝ × Ω ↦ restrictIoc Y t p.1.toNNReal p.2) :
    integrandDist P X Y t = eLpNorm (fun p : Ω × ℝ ↦ X p.2.toNNReal p.1 - Y p.2.toNNReal p.1) 2
      (P.prod (volume.restrict (Set.Ioc (0 : ℝ) t))) ^ 2

Uses 3 · Used by 2

Statement usesSquared \(L^2\) distance between integrands · Restriction of a process to the time interval (0, t)

Proof usesIntegrand distance depends only on times in (0, t)

Used byItô isometry for Itô-approximable integrands · Itô isometry

TheoremItô isometry#✓fully proved

Itô isometry for the L² Itô integral, in ℝ≥0∞ form: for a pre-Brownian motion B adapted to F with increments independent of the past and an integrand H that is Itô-approximable on [0, t], E[(∫_0^t H dB)²] = E ∫_0^t H_u² du (Karatzas–Shreve 1991, Section 3.2).

theorem lintegral_itoIntegral_sq {F : Filtration ℝ≥0 mΩ} {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} {t : ℝ≥0} (hH : IsItoApproximable P F H t) :
    ∫⁻ ω, ‖itoIntegral P F B H t ω‖ₑ ^ 2 ∂P =
      ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P

Uses 15 · Used by 4

Statement usesItô-approximable process · Itô integral process

Proof usesElementary integrand · Itô isometry for elementary integrands · Itô integral of an elementary integrand · Elementary integrands are jointly measurable · Elementary integrand as a process · Squared \(L^2\) distance between integrands · Integrand distance as a squared \(L^2\) seminorm · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

Used byLinearity (additivity) · Linearity (homogeneity) · Itô isometry for progressive integrands · Covariance of the Wiener integrals

TheoremLebesgue differentiation along shrinking off-center intervals#✓fully proved

For a locally integrable f : ℝ → ℝ, for almost every u, the averages of f over intervals [a n, b n] converge to f u whenever the lengths b n - a n > 0 tend to 0 and the distance from u to the midpoint of [a n, b n] is at most twice the length.

theorem MeasureTheory.LocallyIntegrable.ae_tendsto_average_Icc {f : ℝ → ℝ}
    (hf : LocallyIntegrable f volume) :
    ∀ᵐ u, ∀ a b : ℕ → ℝ, (∀ᶠ n in atTop, a n < b n) →
      (∀ᶠ n in atTop, |u - (a n + b n) / 2| ≤ 2 * (b n - a n)) →
      Tendsto (fun n ↦ b n - a n) atTop (𝓝 0) →
      Tendsto (fun n ↦ ⨍ x in Set.Icc (a n) (b n), f x) atTop (𝓝 (f u))

Used by 1

Used byConvergence of the delayed averages

TheoremProgressive processes are jointly measurable#✓fully proved

A progressive process is jointly measurable in (u, ω) (reading u : ℝ through Real.toNNReal).

theorem IsProgressive.measurable_toNNReal {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ}
    (hH : IsProgressive F H) : Measurable fun p : ℝ × Ω ↦ H p.1.toNNReal p.2

Used by 5

Used byDensity of elementary integrands · Linearity (additivity) · Continuous modification · Difference isometry · Convergence of the delayed averages

TheoremTruncation of a progressive process is progressive#✓fully proved

Truncating a progressive process at level M (Mathlib's ProbabilityTheory.truncation, which keeps the values in (-M, M] and sets the others to 0) gives a progressive process.

theorem IsProgressive.truncation {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ}
    (hH : IsProgressive F H) (M : ℝ) : IsProgressive F (fun u ↦ truncation (H u) M)

Used by 1

Used byDelayed-average approximation of a progressive process

TheoremMeasurability of time averages of a progressive process#✓fully proved

For a progressive H and b ≤ T, the average of u ↦ H u ω over [a, b] is F T-measurable in ω.

theorem IsProgressive.measurable_average_Icc {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ}
    (hH : IsProgressive F H) {a b : ℝ} {T : ℝ≥0} (hbT : b ≤ T) :
    Measurable[F T] fun ω ↦ ⨍ s in Set.Icc a b, H s.toNNReal ω

Used by 1

Used byDelayed-average approximation of a progressive process

DefinitionDelayed-average approximation of a progressive process#✓fully proved

The delayed-average approximation of a progressive process H on [0, t], truncated at level M, with n + 1 intervals: on (t_k, t_{k+1}], with t_k = k t / (n + 1), it equals the average of truncation (H ·) M over [t_{k-1}, t_k] for k ≥ 1, and 0 for k = 0. For M ≤ 0 the truncation, and hence the approximation, is 0.

ProbabilityTheory.delayedAverage · 23 lines

noncomputable def delayedAverage {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ}
    (hH : IsProgressive F H) (M : ℝ) (t : ℝ≥0) (n : ℕ) : ElementaryIntegrand F where
  n := n + 1
  time := fun i ↦ t * ((i : ℝ≥0) / (n + 1))
  monotone_time := fun i j hij ↦ by
    dsimp only
    gcongr
    exact_mod_cast hij
  coeff := fun i ω ↦ if (i : ℕ) = 0 then 0 else
    ⨍ s in Set.Icc ((t : ℝ) * (((i : ℕ) : ℝ) - 1) / (n + 1)) ((t : ℝ) * ((i : ℕ) : ℝ) / (n + 1)),
      truncation (H s.toNNReal) M ω
  measurable_coeff := fun i ↦ by
    by_cases hi : (i : ℕ) = 0
    · simp only [hi, ↓reduceIte]
      exact measurable_const
    · simp only [hi, ↓reduceIte]
      refine IsProgressive.measurable_average_Icc (IsProgressive.truncation hH M) ?_
      simp [mul_div_assoc]
  bound := |M|
  abs_coeff_le := fun i ω ↦ by
    split_ifs
    · simp
    · exact abs_average_Icc_le (fun x ↦ abs_truncation_le_bound _ M ω) _ _

Uses 3 · Used by 2

Statement usesElementary integrand · Measurability of time averages of a progressive process · Truncation of a progressive process is progressive

Used byDensity of elementary integrands · Convergence of the delayed averages

TheoremConvergence of the delayed averages#✓fully proved

For a progressive H and a finite measure P, the delayed-average approximations of the truncation of H at level M converge to it in L²(P ⊗ du) on (0, t] × Ω as the mesh t / (n + 1) tends to 0 (Karatzas–Shreve 1991, proof of Lemma 3.2.4(b)).

theorem tendsto_integrandDist_delayedAverage {P : Measure Ω} [IsFiniteMeasure P]
    {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H) (M : ℝ) (t : ℝ≥0) :
    Tendsto (fun n ↦ integrandDist P (delayedAverage hH M t n).toProcess
      (fun u ↦ truncation (H u) M) t) atTop (𝓝 0)

Uses 8 · Used by 1

Statement usesElementary integrand as a process · Delayed-average approximation of a progressive process · Squared \(L^2\) distance between integrands

Proof usesLebesgue differentiation along shrinking off-center intervals · Elementary integrand · Elementary integrands are jointly measurable · Elementary integrand on a partition interval · Progressive processes are jointly measurable

Used byDensity of elementary integrands

TheoremTruncation#✓fully proved

For a jointly measurable H with E ∫_0^t H_u² du < ∞, the truncations of H at levels M → ∞ converge to H in L²(P ⊗ du) on (0, t] × Ω (Karatzas–Shreve 1991, proof of Lemma 3.2.4(c)).

theorem tendsto_integrandDist_truncation {P : Measure Ω} {H : ℝ≥0 → Ω → ℝ}
    (hHm : Measurable fun p : ℝ × Ω ↦ H p.1.toNNReal p.2) (t : ℝ≥0)
    (hH2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    Tendsto (fun M : ℕ ↦ integrandDist P (fun u ↦ truncation (H u) M) H t) atTop (𝓝 0)

Uses 1 · Used by 1

Statement usesSquared \(L^2\) distance between integrands

Used byDensity of elementary integrands

TheoremDensity of elementary integrands#✓fully proved

A progressive integrand H with E ∫_0^t H_u² du < ∞ is the L²(P ⊗ du)-limit on (0, t] × Ω of elementary integrands (Karatzas–Shreve 1991, Lemma 3.2.4 and Proposition 3.2.6).

theorem isItoApproximable_of_isProgressive {P : Measure Ω} [IsFiniteMeasure P]
    {F : Filtration ℝ≥0 mΩ} {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H) (t : ℝ≥0)
    (hH2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    IsItoApproximable P F H t

Uses 12 · Used by 5

Statement usesItô-approximable process

Proof usesElementary integrand · Elementary integrands are jointly measurable · Elementary integrand as a process · Progressive processes are jointly measurable · Delayed-average approximation of a progressive process · Squared \(L^2\) distance between integrands · Quasi-triangle inequality for the integrand distance · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · Convergence of the delayed averages · Truncation

Used byLinearity (additivity) · Continuous modification · Linearity (homogeneity) · Itô isometry for progressive integrands · Martingale property for progressive integrands

TheoremSquare integrability of the Itô integral#✓fully proved

The Itô integral at each time is square integrable: it is a version of the element itoIntegralL2 P F B H t of L²(P) (which is 0 when H is not Itô-approximable).

theorem memLp_itoIntegral (P : Measure Ω) (F : Filtration ℝ≥0 mΩ) (B H : ℝ≥0 → Ω → ℝ)
    (t : ℝ≥0) : MemLp (itoIntegral P F B H t) 2 P

Uses 3 · Used by 3

Statement usesItô integral process

Proof usesItô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral

Used byLinearity (additivity) · Difference isometry · Linearity (homogeneity)

TheoremItô isometry for progressive integrands#✓fully proved

For a pre-Brownian motion B adapted to F with increments independent of the past and an F-progressive integrand H with E ∫_0^t H_u² du < ∞, E[(∫_0^t H dB)²] = E ∫_0^t H_u² du (Karatzas–Shreve 1991, Section 3.2).

theorem lintegral_itoIntegral_sq_of_isProgressive {P : Measure Ω} {F : Filtration ℝ≥0 mΩ}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H) (t : ℝ≥0)
    (hH2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    ∫⁻ ω, ‖itoIntegral P F B H t ω‖ₑ ^ 2 ∂P =
      ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P

Uses 3 · Used by 1

Statement usesItô integral process

Proof usesDensity of elementary integrands · Itô isometry

Used byDifference isometry

TheoremMartingale property for progressive integrands#✓fully proved

For a pre-Brownian motion B adapted to F with increments independent of the past and an F-progressive integrand H with E ∫_0^t H_u² du < ∞ for every t, the Itô integral t ↦ ∫_0^t H dB is an F-martingale (Karatzas–Shreve 1991, Proposition 3.2.10).

theorem martingale_itoIntegral_of_isProgressive {P : Measure Ω} {F : Filtration ℝ≥0 mΩ}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P) {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H)
    (hH2 : ∀ t : ℝ≥0, ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    Martingale (itoIntegral P F B H) F P

Uses 3

Statement usesItô integral process

Proof usesDensity of elementary integrands · Martingale property of the Itô integral

TheoremContinuous modification#✓fully proved

The Itô integral admits a modification with continuous paths: there is a process J with continuous paths such that J t = ∫_0^t H dB almost surely for each t (Karatzas–Shreve 1991, Section 3.2). ProbabilityTheory.itoIntegral chooses its version separately at each time, so it is only determined up to a null set that may depend on t; the statement therefore asks for a modification rather than for a process indistinguishable from this particular choice. Any two continuous modifications are indistinguishable.

public theorem itoIntegral_continuous_modification {Ω : 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)
    {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H)
    (hH2 : ∀ t : ℝ≥0, ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t,
      ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    ∃ J : ℝ≥0 → Ω → ℝ, (∀ ω, Continuous fun t ↦ J t ω) ∧
      ∀ t, J t =ᵐ[P] itoIntegral P F B H t

Uses 16

Statement usesItô integral process

Proof usesElementary integrand · Itô integral of an elementary integrand · Martingale property · Square integrability of the elementary Itô integral · Elementary integrand as a process · Itô-approximable process · Progressive processes are jointly measurable · Squared \(L^2\) distance between integrands · Density of elementary integrands · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

TheoremItô isometry for Itô-approximable integrands#✓fully proved

The squared L²(P ⊗ du) distance between two Itô-approximable integrands is the squared L²(P) distance between their Itô integrals.

theorem integrandDist_eq_dist_sq_itoIntegralL2 {F : Filtration ℝ≥0 mΩ} {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep
      (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance) (F s) P)
    {H K : ℝ≥0 → Ω → ℝ} {t : ℝ≥0} (hH : IsItoApproximable P F H t)
    (hK : IsItoApproximable P F K t) :
    integrandDist P H K t = ENNReal.ofReal
      (dist (itoIntegralL2 P F B H t) (itoIntegralL2 P F B K t) ^ 2)

Uses 14 · Used by 2

Statement usesItô-approximable process · Squared \(L^2\) distance between integrands · Itô integral as an element of \(L^2\)

Proof usesElementary integrand · Itô isometry for elementary integrands · Finite distance between elementary integrands · Itô integral of an elementary integrand · Elementary integrands are jointly measurable · Elementary integrand as a process · Integrand distance as a squared \(L^2\) seminorm · Restriction to (0, t) preserves joint measurability · Restriction of a process to the time interval (0, t) · The Itô integral is well defined · Function as an element of \(L^2\)

Used byLinearity (additivity) · Linearity (homogeneity)

TheoremLinearity (additivity)#✓fully proved

The Itô integral is additive in the integrand: for F-progressive integrands H₁, H₂ with E ∫_0^t H_i² du < ∞, the integral of the sum is almost surely the sum of the integrals. Together with homogeneity and the difference isometry this pins down the integral on the whole L² space of progressive integrands. Only the pre-Brownian finite-dimensional laws are used; path continuity is not required.

public theorem itoIntegral_add_of_isPreBrownianReal {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {F : Filtration ℝ≥0 mΩ} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P)
    (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P)
    {H₁ H₂ : ℝ≥0 → Ω → ℝ} (hH₁ : IsProgressive F H₁) (hH₂ : IsProgressive F H₂) (t : ℝ≥0)
    (hH₁2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₁ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞)
    (hH₂2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₂ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    itoIntegral P F B (H₁ + H₂) t =ᵐ[P]
      fun ω ↦ itoIntegral P F B H₁ t ω + itoIntegral P F B H₂ t ω

Uses 11 · Used by 2

Statement usesItô integral process

Proof usesItô-approximable process · Progressive processes are jointly measurable · Squared \(L^2\) distance between integrands · Itô isometry for Itô-approximable integrands · Quasi-triangle inequality for the integrand distance · Density of elementary integrands · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Itô isometry · Square integrability of the Itô integral

Used byLinearity (additivity) · Difference isometry

TheoremLinearity (additivity)#✓fully proved

The Itô integral is additive in the integrand: for F-progressive integrands H₁, H₂ with E ∫_0^t H_i² du < ∞, the integral of the sum is almost surely the sum of the integrals. Together with homogeneity and the difference isometry this pins down the integral on the whole L² space of progressive integrands.

public theorem itoIntegral_add {Ω : 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)
    {H₁ H₂ : ℝ≥0 → Ω → ℝ} (hH₁ : IsProgressive F H₁) (hH₂ : IsProgressive F H₂) (t : ℝ≥0)
    (hH₁2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₁ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞)
    (hH₂2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₂ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    itoIntegral P F B (H₁ + H₂) t =ᵐ[P]
      fun ω ↦ itoIntegral P F B H₁ t ω + itoIntegral P F B H₂ t ω

Uses 2

Statement usesItô integral process

Proof usesLinearity (additivity)

TheoremLinearity (homogeneity)#✓fully proved

The Itô integral is homogeneous in the integrand for a pre-Brownian integrator; path continuity is not required.

public theorem itoIntegral_smul_of_isPreBrownianReal {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {F : Filtration ℝ≥0 mΩ} {B : ℝ≥0 → Ω → ℝ}
    (hB : IsPreBrownianReal B P)
    (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P)
    {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H) (a : ℝ) (t : ℝ≥0)
    (hH2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    itoIntegral P F B (a • H) t =ᵐ[P] fun ω ↦ a * itoIntegral P F B H t ω

Uses 9 · Used by 2

Statement usesItô integral process

Proof usesItô-approximable process · Squared \(L^2\) distance between integrands · Itô isometry for Itô-approximable integrands · Density of elementary integrands · Itô integral as an element of \(L^2\) · Itô integral process is a version of the \(L^2\) integral · Itô isometry · Square integrability of the Itô integral

Used byDifference isometry · Linearity (homogeneity)

TheoremLinearity (homogeneity)#✓fully proved

The Itô integral is homogeneous in the integrand.

public theorem itoIntegral_smul {Ω : 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)
    {H : ℝ≥0 → Ω → ℝ} (hH : IsProgressive F H) (a : ℝ) (t : ℝ≥0)
    (hH2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    itoIntegral P F B (a • H) t =ᵐ[P] fun ω ↦ a * itoIntegral P F B H t ω

Uses 2

Statement usesItô integral process

Proof usesLinearity (homogeneity)

TheoremDifference isometry#✓fully proved

For two F-progressive integrands with E ∫_0^t H_i² du < ∞, the difference of the integrals is square-integrable and E[(∫ H₁ dB - ∫ H₂ dB)²] = E ∫ (H₁ - H₂)² du. With linearity this is the two-integrand isometry that, together with the elementary-integrand formula, determines the construction on the whole L² space. Only the pre-Brownian finite-dimensional laws are used; path continuity is not required.

public theorem itoIntegral_isometry_sub_of_isPreBrownianReal {Ω : Type*}
    {mΩ : MeasurableSpace Ω} {P : Measure Ω} {F : Filtration ℝ≥0 mΩ}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P)
    (hBF : Adapted F B)
    (hInd : ∀ s t, s ≤ t → Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (F s) P)
    {H₁ H₂ : ℝ≥0 → Ω → ℝ} (hH₁ : IsProgressive F H₁) (hH₂ : IsProgressive F H₂) (t : ℝ≥0)
    (hH₁2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₁ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞)
    (hH₂2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₂ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    MemLp (fun ω ↦ itoIntegral P F B H₁ t ω - itoIntegral P F B H₂ t ω) 2 P ∧
      ∫⁻ ω, ‖itoIntegral P F B H₁ t ω - itoIntegral P F B H₂ t ω‖ₑ ^ 2 ∂P =
        ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t,
          ‖H₁ u.toNNReal ω - H₂ u.toNNReal ω‖ₑ ^ 2) ∂P

Uses 8 · Used by 1

Statement usesItô integral process

Proof usesProgressive processes are jointly measurable · Squared \(L^2\) distance between integrands · Quasi-triangle inequality for the integrand distance · Linearity (additivity) · Linearity (homogeneity) · Itô isometry for progressive integrands · Square integrability of the Itô integral

Used byDifference isometry

TheoremDifference isometry#✓fully proved

For two F-progressive integrands with E ∫_0^t H_i² du < ∞, the difference of the integrals is square-integrable and E[(∫ H₁ dB - ∫ H₂ dB)²] = E ∫ (H₁ - H₂)² du. With linearity this is the two-integrand isometry that, together with the elementary-integrand formula, determines the construction on the whole L² space.

public theorem itoIntegral_isometry_sub {Ω : 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)
    {H₁ H₂ : ℝ≥0 → Ω → ℝ} (hH₁ : IsProgressive F H₁) (hH₂ : IsProgressive F H₂) (t : ℝ≥0)
    (hH₁2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₁ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞)
    (hH₂2 : ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t, ‖H₂ u.toNNReal ω‖ₑ ^ 2) ∂P ≠ ∞) :
    MemLp (fun ω ↦ itoIntegral P F B H₁ t ω - itoIntegral P F B H₂ t ω) 2 P ∧
      ∫⁻ ω, ‖itoIntegral P F B H₁ t ω - itoIntegral P F B H₂ t ω‖ₑ ^ 2 ∂P =
        ∫⁻ ω, (∫⁻ u in Set.Ioc (0 : ℝ) t,
          ‖H₁ u.toNNReal ω - H₂ u.toNNReal ω‖ₑ ^ 2) ∂P

Uses 2

Statement usesItô integral process

Proof usesDifference isometry

68 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.