class or structure for stochastic process

Stream: general

[Frederick Pu]

Is there any nice structure that wraps all of the information for stochastic processes? I'm trying to formalize risk free pricing of Derivatives and i found that making StochasticProcess that wraps in the filtration, measurablespace an measure allowed me to avoid typing implcit parameters constantly:

structure StochasticProcess (Ω : Type*) (m0 : MeasurableSpace Ω) (P : Measure Ω)
 (𝒻 : Filtration ℕ m0) where
  val : ℕ → Ω → ℝ

Here is some usage examples:

import Mathlib.Probability.Martingale.Basic

open ProbabilityTheory MeasureTheory
open scoped BigOperators

namespace GeneralizedArbitrage

variable {Ω : Type*} {m0 : MeasurableSpace Ω} {P : Measure Ω} [IsProbabilityMeasure P]
  {𝒻 : Filtration ℕ m0}


structure StochasticProcess (Ω : Type*) (m0 : MeasurableSpace Ω) (P : Measure Ω)
 (𝒻 : Filtration ℕ m0) where
  val : ℕ → Ω → ℝ

instance : FunLike (StochasticProcess Ω m0 P 𝒻) ℕ (Ω → ℝ) := {
  coe := (·.val)
  coe_injective' := by
    intro x y
    cases x
    cases y
    simp
}

/-- A stock price process: `Stock Ω` is a function from time and world-state to price. -/
abbrev Stock (Ω : Type*) := ℕ → Ω → ℝ

/--
**Arbitrage**: a trading strategy that requires no upfront capital, never loses
money in any scenario, but generates positive expected profit.
-/
structure Arbitrage (stock bond : StochasticProcess Ω m0 P 𝒻) where
  periods : ℕ
  holdings : Stock Ω
  noLookAhead : ∀ n, StronglyMeasurable[𝒻 n] (holdings (n + 1))
  noCostToEnter : ∀ ω, holdings 0 ω = 0
  neverLoseMoney : ∀ᵐ ω ∂P, 0 ≤
    ∑ t ∈ Finset.range periods,
      holdings (t+1) ω * ((stock (t+1) ω / bond (t+1) ω) - (stock t ω / bond t ω))
  positiveExpectedProfit : 0 < ∫ ω,
    ∑ t ∈ Finset.range periods,
      holdings (t+1) ω * ((stock (t+1) ω / bond (t+1) ω) - (stock t ω / bond t ω)) ∂P

/--
Two measures are **equivalent** if they agree on which events are possible:
neither can declare an event impossible that the other considers possible.
-/
def Equivalent (Q P : Measure Ω) : Prop :=
  ∀ s : Set Ω, MeasurableSet s → (Q s = 0 ↔ P s = 0)

/--
A **risk-neutral measure** `Q` is a probability measure equivalent to the real-world
measure `P` under which the discounted stock price is a martingale — i.e. there is
no expected profit from trading beyond the risk-free rate.
-/
def IsRiskNeutralMeasure (Q : Measure Ω) (stock bond : StochasticProcess Ω m0 P 𝒻) : Prop :=
  IsProbabilityMeasure Q ∧
  Equivalent Q P ∧
  Martingale (fun t ω => stock t ω / bond t ω) 𝒻 Q

/--
**Fundamental Theorem of Asset Pricing** (discrete time):

A market admits no arbitrage if and only if there exists a risk-neutral measure.

(Harrison–Pliska 1981; Dalang–Morton–Willinger 1990)
-/
theorem noArbitrage_iff_riskNeutralMeasure (stock bond : StochasticProcess Ω m0 P 𝒻)
    (hBond : ∀ t ω, bond t ω ≠ 0) :
    IsEmpty (Arbitrage stock bond) ↔
    ∃ Q : Measure Ω, IsRiskNeutralMeasure Q stock bond := by
  sorry -- Harrison–Pliska / Dalang–Morton–Willinger

[Etienne Marion]

I don't see how this structure is useful in practice compared to just having a ℕ → Ω → ℝ variable (also it's a detail but you don't necessarily index by ℕ but with a general type). Introducing names for things that can be simply expressed without it is generally not a good idea, it creates a barrier that can hinder the existing API.