Tests.ItoIntegralProcess

- A one-cell deterministic unit integrand used to exercise the complete general-Ito construction rather than only checking its declaration names.

noncomputable def unitElementary (hT : 0 < T) :
    ElementaryAdaptedProcess filtration 1 where
    times := regularGridTimes T 1
    times_strictMono := regularGridTimes_strictMono hT 1
    coeff := fun _ _ => 1
    coeff_stronglyMeasurable := fun _ => stronglyMeasurable_const
    coeff_bounded := fun _ => ⟨1, fun _ => by simp⟩

Tests/ItoIntegralProcess.lean:41published source at 77184245109a

No declaration docstring.

noncomputable def unitDyadic (hT : 0 < T) :
    DyadicElementaryProcess filtration T where
  level := 0
  process := unitElementary hT
  times_eq := by simp [unitElementary, dyadicMesh]

Tests/ItoIntegralProcess.lean:49published source at 77184245109a

No declaration docstring.

theorem unitDyadic_elementaryItoProcess
    (hT : 0 < T) {t : ℝ≥0} (htT : t ≤ T) (omega : Omega) :
    elementaryItoProcess (unitElementary (filtration := filtration) hT) B T t omega =
      B t omega - B 0 omega := by
  simp [elementaryItoProcess, elementaryItoIntegral, unitElementary,
    regularGridTimes]
  rw [min_eq_left htT]

example [IsFiniteMeasure mu]
    (hT : 0 < T) (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    {t : ℝ≥0} (ht : 0 < t) (htT : t ≤ T) :
    ItoIntegralProcess.itoIntegralProcess
        (elementaryIntegrand (unitDyadic (filtration := filtration) hT) hB)
        hT hB hUsual t =ᵐ[mu]
      fun omega => B t omega - B 0 omega := by
  have hprocess :=
    ItoIntegralProcess.itoIntegralProcess_at_eq_terminal
      (elementaryIntegrand (unitDyadic (filtration := filtration) hT) hB)
      hT hB hUsual htT
  have helementary :=
    ItoIntegralProcess.itoIntegralTerminal_restrictAt_elementary_ae
      (unitDyadic (filtration := filtration) hT) hT hB ht htT
  exact hprocess.trans (helementary.trans
    (Filter.Eventually.of_forall fun omega => by
      simpa [unitDyadic] using unitDyadic_elementaryItoProcess hT htT omega))

example [IsFiniteMeasure mu]
    (hT : 0 < T) (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    {t : ℝ≥0} (htT : t ≤ T) :
    ItoIntegralProcess.itoIntegralProcess
        (ProgressiveL2Algebra.zero : ProgressiveL2Integrand filtration mu T)
        hT hB hUsual t =ᵐ[mu] fun _ => 0 :=
  ItoIntegralProcess.itoIntegralProcess_zero hT hB hUsual htT

example [IsFiniteMeasure mu]
    (eta xi : ProgressiveL2Integrand filtration mu T)
    (hT : 0 < T) (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    {t : ℝ≥0} (htT : t ≤ T) :
    ItoIntegralProcess.itoIntegralProcess
        (ProgressiveL2Algebra.add eta xi) hT hB hUsual t =ᵐ[mu]
      fun omega =>
-- Source excerpt truncated; follow the exact source link.

Tests/ItoIntegralProcess.lean:55published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.