ThmDex – An index of mathematical definitions, results, and conjectures.
Result R5656 on D5207: Real poisson process
Real poisson process is increasing
Formulation 0
Let $X \in \text{PoissonProcess}(\theta)$ be a D5207: Real poisson process.
Then \begin{equation} \forall \, s, t \in [0, \infty) \left( s \leq t \quad \Longrightarrow \quad X_s \leq X_t \right) \end{equation}
Proofs
Proof 0
Let $X \in \text{PoissonProcess}(\theta)$ be a D5207: Real poisson process.
Let $T_1, T_2, T_3, \, \ldots \overset{d}{=} \text{Exponential}(\theta)$ be an independent sequence of exponential variables that defines $X$ and let $\omega \in \Omega$ be an outcome. Then we have the inclusion \begin{equation} \left\{ M \in \mathbb{N} : \sum_{m = 1}^M T_m (\omega) \leq s \right\} \subseteq \left\{ M \in \mathbb{N} : \sum_{m = 1}^M T_m (\omega) \leq t \right\} \end{equation} Using result R1110: Isotonicity of maximum, therefore \begin{equation} X_s (\omega) = \max \left\{ M \in \mathbb{N} : \sum_{m = 1}^M T_m (\omega) \leq s \right\} \leq \max \left\{ M \in \mathbb{N} : \sum_{m = 1}^M T_m (\omega) \leq t \right\} = X_t (\omega) \end{equation} Since $\omega \in \Omega$ was arbitrary, the result follows. $\square$