ThmDex – An index of mathematical definitions, results, and conjectures.
Set of symbols
Alphabet
Deduction system
Theory
Zermelo-Fraenkel set theory
Set
Collection of sets
Set union
Successor set
Inductive set
Set of inductive sets
Set of natural numbers
Set of integers
Set of rademacher integers
Rademacher integer
Rademacher random integer
Standard rademacher random integer
Standard gaussian random real number
Gaussian random real number
Definition D4614
Log-gaussian random basic real number
Formulation 0
Let $\exp$ be the D1932: Standard natural real exponential function.
Let $G \in \text{Gaussian}(\mu, \sigma)$ be a D210: Gaussian random real number.
A D3161: Random real number $X \in \text{Random}(\mathbb{R})$ is a log-gaussian random basic real number with parameters $\mu$ and $\sigma$ if and only if \begin{equation} X \overset{d}{=} \exp( G ) \end{equation}