ThmDex – An index of mathematical definitions, results, and conjectures.
Result R4901 on D214: Exponential random positive real number
Subresult of R3778: Probability density function for exponential random positive real number
Probability density function for standard exponential random positive real number
Formulation 0
Let $T \in \text{Exp}(1)$ be a D4000: Standard exponential random positive real number.
Let $B \in \mathcal{B}(\mathbb{R})$ be a D5113: Standard real Borel set.
Then \begin{equation} \mathbb{P}(T \in B) = \int_B e^{- t} I_{[0, \infty)}(t) \, d t \end{equation}
Formulation 1
Let $T \in \text{Exp}(1)$ be a D4000: Standard exponential random positive real number such that
(i) $\mu_T$ is a D204: Probability distribution measure for $T$
Let $\ell$ be the D5645: Real Lebesgue measure.
Let $t \in \mathbb{R}$ be a D993: Real number.
Then \begin{equation} \frac{d \mu_T}{d \ell} (t) = e^{- t} I_{[0, \infty)} (t) \end{equation}
Proofs
Proof 0
Let $T \in \text{Exp}(1)$ be a D4000: Standard exponential random positive real number.
Let $B \in \mathcal{B}(\mathbb{R})$ be a D5113: Standard real Borel set.