Quadratic variation of Brownian motion

DefinitionWeighted quadratic-variation error of Brownian motion#✓fully proved

The weighted quadratic-variation error along the uniform partition of [0, t] into n cells: ∑_{k < n} φ(B (t k / n)) ((B (t (k + 1) / n) - B (t k / n))² - t / n).

noncomputable def weightedQVError {Ω : Type*} (φ : ℝ → ℝ) (B : ℝ≥0 → Ω → ℝ) (t : ℝ≥0)
    (n : ℕ) (ω : Ω) : ℝ :=
  ∑ k ∈ Finset.range n, φ (B (t * k / n) ω) *
    ((B (t * (k + 1) / n) ω - B (t * k / n) ω) ^ 2 - ((t : ℝ) / n))

Used by 4

Used byItô's formula · Second moment of the weighted quadratic-variation error · Quadratic variation of Brownian motion · Weighted quadratic variation of Brownian motion

TheoremSecond moment of the weighted quadratic-variation error#✓fully proved

For a pre-Brownian motion B adapted to F with increments independent of the past, and a measurable weight φ bounded by C, E[(∑_{k < n} φ(B_{t_k}) ((ΔB_k)² - Δt))²] ≤ 2 C² t² / n on the uniform partition t_k = t k / n (n ≥ 1).

theorem integral_weightedQVError_sq_le
    {Ω : 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φ : Measurable φ) {C : ℝ} (hφC : ∀ x, |φ x| ≤ C) (t : ℝ≥0) {n : ℕ}
    (hn : 0 < n) :
    ∫ ω, weightedQVError φ B t n ω ^ 2 ∂P ≤ 2 * C ^ 2 * (t : ℝ) ^ 2 / n

Uses 1 · Used by 1

Statement usesWeighted quadratic-variation error of Brownian motion

Used byWeighted quadratic variation of Brownian motion

TheoremWeighted quadratic variation of Brownian motion#✓fully proved

Under the hypotheses of integral_weightedQVError_sq_le, ∑_{k < n} φ(B_{t_k}) ((ΔB_k)² - Δt) → 0 in L²(P).

theorem tendsto_eLpNorm_weightedQVError
    {Ω : 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φ : Measurable φ) {C : ℝ} (hφC : ∀ x, |φ x| ≤ C) (t : ℝ≥0) :
    Tendsto (fun n ↦ eLpNorm (weightedQVError φ B t n) 2 P) atTop (𝓝 0)

Uses 2 · Used by 2

Statement usesWeighted quadratic-variation error of Brownian motion

Proof usesSecond moment of the weighted quadratic-variation error

Used byItô's formula · Quadratic variation of Brownian motion

TheoremIncrements are independent of the past#✓fully proved

For a pre-Brownian motion with measurable coordinates, each increment B t - B s (s ≤ t) is independent of the natural filtration at time s (a consequence of IsPreBrownianReal.indepFun_shift, the weak Markov property).

theorem IsPreBrownianReal.indep_natural {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
    {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (hBm : ∀ t, Measurable (B t)) (s t : ℝ≥0)
    (hst : s ≤ t) :
    Indep (MeasurableSpace.comap (fun ω ↦ B t ω - B s ω) inferInstance)
      (Filtration.natural B (fun t ↦ (hBm t).stronglyMeasurable) s) P

Used by 2

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian · Quadratic variation of Brownian motion

TheoremProcesses with measurable coordinates are adapted to their natural filtration#✓fully proved

A process with measurable coordinates is adapted to its natural filtration.

theorem adapted_natural_of_measurable {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {B : ℝ≥0 → Ω → ℝ} (hBm : ∀ t, Measurable (B t)) :
    Adapted (Filtration.natural B (fun t ↦ (hBm t).stronglyMeasurable)) B

Used by 2

Used byThe pathwise Langevin solution driven by Brownian motion is Gaussian · Quadratic variation of Brownian motion

TheoremQuadratic variation of Brownian motion#✓fully proved

Quadratic variation of Brownian motion, [B]_t = t: along the uniform partitions of [0, t], ∑_{k < n} (B (t (k + 1) / n) - B (t k / n))² → t in L²(P), for every pre-Brownian motion B (no filtration and no measurability of the coordinates is assumed; Øksendal 2003, Exercise 2.17; Karatzas–Shreve 1991, Theorem 1.5.8 treats continuous square-integrable martingales in probability).

theorem IsPreBrownianReal.tendsto_eLpNorm_sum_sq_sub {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (t : ℝ≥0) :
    Tendsto (fun n : ℕ ↦ eLpNorm (fun ω ↦ ∑ k ∈ Finset.range n,
      (B (t * (k + 1) / n) ω - B (t * k / n) ω) ^ 2 - t) 2 P) atTop (𝓝 0)

Uses 4 · Used by 1

Proof usesIncrements are independent of the past · Processes with measurable coordinates are adapted to their natural filtration · Weighted quadratic variation of Brownian motion · Weighted quadratic-variation error of Brownian motion

Used byQuadratic variation of Brownian motion in probability

TheoremQuadratic variation of Brownian motion in probability#✓fully proved

Along the uniform partitions of [0, t], ∑_{k < n} (B (t (k + 1) / n) - B (t k / n))² → t in probability.

theorem IsPreBrownianReal.tendstoInMeasure_sum_sq {Ω : Type*} {mΩ : MeasurableSpace Ω}
    {P : Measure Ω} {B : ℝ≥0 → Ω → ℝ} (hB : IsPreBrownianReal B P) (t : ℝ≥0) :
    TendstoInMeasure P (fun (n : ℕ) ω ↦ ∑ k ∈ Finset.range n,
      (B (t * (k + 1) / n) ω - B (t * k / n) ω) ^ 2) atTop (fun _ ↦ (t : ℝ))

Uses 1

Proof usesQuadratic variation of Brownian motion

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.