Continous time process

Stream: new members

[Joshua Banks]

Hi all,

I am working with random variables and trying to define a basic stochastic process as a sequence of random variables.
I have currently defined X as X : ℕ → Ω → ℝ and trying to achieve a definition where a process is defined as
{ω | X t ω } where t is some point in time. I am struggling to progress on how to write this, any help is really appreciated.

[Alistair Tucker]

I don't know what you mean by {ω | X t ω}. But X : ℕ → Ω → ℝ is indeed correct for a discrete time process and X : ℝ≥0 → Ω → ℝ would describe a continuous time process.

[Joshua Banks]

It was supposed to a representation for the collection of random variables in the stochastic process, as it defined on paper as {X(t) : t ∈ T} where for a continuous process T = [0, ∞)

[Alistair Tucker]

I think X : ℝ≥0 → Ω → ℝ achieves that?

[Alistair Tucker]

You will need to import data.real.nnreal and open_locale nnreal for the notation.