AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariation

- A Brownian increment is square-integrable.

theorem increment_memLp_two
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (s t : ℝ≥0) :
    MemLp (fun omega => B t omega - B s omega) 2 mu := by
  have hpre := hB.isBrownian.toIsPreBrownianReal
  exact (hpre.isGaussianProcess.hasGaussianLaw_eval t |>.memLp_two).sub
    (hpre.isGaussianProcess.hasGaussianLaw_eval s |>.memLp_two)

/-- The square of a Brownian increment is integrable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:31published source at 0e31a3cda412

- The square of a Brownian increment is integrable.

theorem increment_sq_integrable
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (s t : ℝ≥0) :
    Integrable (fun omega => (B t omega - B s omega) ^ 2) mu := by
  have hmem := increment_memLp_two hB s t
  have hmul : Integrable
      ((fun omega => B t omega - B s omega) *
        (fun omega => B t omega - B s omega)) mu :=
    hmem.integrable_mul hmem
  exact hmul.congr (ae_of_all mu fun omega => by simp [pow_two])

/-- The compensated square of one future Brownian increment is integrable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:40published source at 0e31a3cda412

- The compensated square of one future Brownian increment is integrable.

theorem centered_increment_sq_integrable
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {s t : ℝ≥0} (_hst : s ≤ t) :
    Integrable
      (fun omega =>
        (B t omega - B s omega) ^ 2 - ((t - s : ℝ≥0) : ℝ)) mu := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  exact (increment_sq_integrable hB s t).sub (by fun_prop)

/-- The basic compensated-increment identity behind Brownian quadratic
variation: `E[(B_t-B_s)^2-(t-s)] = 0`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:52published source at 0e31a3cda412

- The basic compensated-increment identity behind Brownian quadratic variation: `E[(B_t-B_s)^2-(t-s)] = 0`.

theorem integral_centered_increment_sq_eq_zero
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {s t : ℝ≥0} (hst : s ≤ t) :
    ∫ omega,
        ((B t omega - B s omega) ^ 2 - ((t - s : ℝ≥0) : ℝ)) ∂mu = 0 := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  rw [integral_sub (increment_sq_integrable hB s t) (by fun_prop)]
  rw [hB.integral_increment_sq hst]
  simp

/-- One compensated cell of a deterministic finite time grid. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:63published source at 0e31a3cda412

- One compensated cell of a deterministic finite time grid.

noncomputable def centeredSquaredIncrement
    {n : ℕ} (B : ℝ≥0 → Omega → ℝ)
    (times : Fin (n + 1) → ℝ≥0) (i : Fin n) (omega : Omega) : ℝ :=
  (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
    ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)

/-- Finite-grid error in the Brownian quadratic-variation rule. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:74published source at 0e31a3cda412

- Finite-grid error in the Brownian quadratic-variation rule.

noncomputable def quadraticVariationError
    {n : ℕ} (B : ℝ≥0 → Omega → ℝ)
    (times : Fin (n + 1) → ℝ≥0) (omega : Omega) : ℝ :=
  ∑ i : Fin n, centeredSquaredIncrement B times i omega

/-- The uncompensated finite-grid quadratic-variation sum. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:81published source at 0e31a3cda412

- The uncompensated finite-grid quadratic-variation sum.

noncomputable def quadraticVariationSum
    {n : ℕ} (B : ℝ≥0 → Omega → ℝ)
    (times : Fin (n + 1) → ℝ≥0) (omega : Omega) : ℝ :=
  ∑ i : Fin n,
    (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:87published source at 0e31a3cda412

No declaration docstring.

private theorem grid_cell_le
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) (i : Fin n) :
    times i.castSucc ≤ times i.succ :=
  hmono Fin.castSucc_lt_succ.le

/-- Every compensated grid cell is integrable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:93published source at 0e31a3cda412

- Every compensated grid cell is integrable.

theorem centeredSquaredIncrement_integrable
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) (i : Fin n) :
    Integrable (centeredSquaredIncrement B times i) mu := by
  change Integrable
    (fun omega =>
      (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
        ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)) mu
  exact centered_increment_sq_integrable hB (grid_cell_le hmono i)

/-- Every deterministic finite partition has zero-mean compensated quadratic
variation error.  This is the finite-sum identity that precedes the mesh-limit
argument in Chewi's quadratic-variation calculation. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:100published source at 0e31a3cda412

- Every deterministic finite partition has zero-mean compensated quadratic variation error. This is the finite-sum identity that precedes the mesh-limit argument in Chewi's quadratic-variation calculation.

theorem integral_quadraticVariationError_eq_zero
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, quadraticVariationError B times omega ∂mu = 0 := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  calc
    ∫ omega, quadraticVariationError B times omega ∂mu =
        ∑ i : Fin n, ∫ omega, centeredSquaredIncrement B times i omega ∂mu := by
          change
            (∫ omega, ∑ i : Fin n, centeredSquaredIncrement B times i omega ∂mu) =
              ∑ i : Fin n, ∫ omega, centeredSquaredIncrement B times i omega ∂mu
          rw [integral_finsetSum]
          intro i _
          exact centeredSquaredIncrement_integrable hB hmono i
    _ = 0 := by
      apply Finset.sum_eq_zero
      intro i _
      change
        (∫ omega,
          ((B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
            ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)) ∂mu) = 0
      exact integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)

/-- Expected quadratic variation on a finite deterministic grid is exactly the
sum of the cell lengths. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:114published source at 0e31a3cda412

- Expected quadratic variation on a finite deterministic grid is exactly the sum of the cell lengths.

theorem integral_quadraticVariationSum_eq_sum_cellLengths
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, quadraticVariationSum B times omega ∂mu =
      ∑ i : Fin n, ((times i.succ - times i.castSucc : ℝ≥0) : ℝ) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  calc
    ∫ omega, quadraticVariationSum B times omega ∂mu =
        ∑ i : Fin n,
          ∫ omega,
            (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 ∂mu := by
          change
            (∫ omega,
              ∑ i : Fin n,
                (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 ∂mu) =
              ∑ i : Fin n,
                ∫ omega,
                  (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 ∂mu
          rw [integral_finsetSum]
          intro i _
          exact increment_sq_integrable hB _ _
    _ = ∑ i : Fin n,
        ((times i.succ - times i.castSucc : ℝ≥0) : ℝ) := by
      apply Finset.sum_congr rfl
      intro i _
      exact hB.integral_increment_sq (grid_cell_le hmono i)

end BrownianQuadraticVariation
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean:140published source at 0e31a3cda412