# Real random variables on finite sample spaces

This English edition is an AI candidate and does not yet have an OCME Atlas (GPT-6) Twin closure receipt.

A random variable in a finite model is a total function from elementary outcomes to real numbers, distinct from an outcome or its probability weight.

mko-random-variable · definition · v0.10.0



## Mathematical statement

On a nonempty finite sample space S with event family F=𝒫(S) and a valid probability law P, a real random variable is a total function X:S→R. For any real subset T, the preimage {s∈S:X(s)∈T} is an event. P(X=t) sums the weights of all outcomes with X(s)=t.





## Representative formula (exact TeX)

X:S\to R





## Assumptions


- S is finite and nonempty, F is the full powerset, and X assigns one real value to every elementary outcome.
- Value, range, and preimage-event questions read only the function data without guessing the probability law; point-probability questions separately specify valid rational weights.





## Symbol scope


- X — real-valued random variable
- S — nonempty finite sample space
- R — real codomain





## Intuition, definition, and misconceptions

Different elementary outcomes may have the same random-variable value. The range removes duplicate values, but point probabilities sum the weights of every preimage.

An explicit condition such as X(s)≥t selects elementary outcomes for a preimage event. The event set is distinct from a numerical probability; missing weights do not imply equiprobability.

Exercises use exact integer outcome labels and integer output values. A finite full powerset makes every preimage an event. General measurable spaces, continuous densities, and distribution representations have separate obligations.

Common errors include identifying a random variable with one sampled outcome, treating range cardinality as probability, or omitting weights of repeated output values.





## Adopted derivation guide

[Random variables on a finite sample space: range, preimage events and point probabilities](https://ocme.evemisslab.com/en/derivations/derivation-mko-random-variable-01/)The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.





## Prerequisites


- [Function mapping](https://ocme.evemisslab.com/en/mko/mko-function-mapping/) — A random variable is total on its sample space.
- [Sample space](https://ocme.evemisslab.com/en/mko/mko-sample-space/) — Inputs are elementary outcomes rather than random-variable values.
- [Real number](https://ocme.evemisslab.com/en/mko/mko-real-number/) — Outputs are real numbers.
- [Probability on finite sample spaces](https://ocme.evemisslab.com/en/mko/mko-probability/) — Point probabilities require weights and event probabilities.





## Verification boundary

Finite functions and point masses can be recomputed completely; general measurability and distribution-pushforward bridges have no attached Evidence.

not_formalized

This does not mean the content is false; it means no replayable computational or formal evidence is registered yet.





## Next obligation

Bind finite PMFs, total functions, preimage events, and pushforwards; list general Measurable obligations separately.





## Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.

[Canonical MKO JSON](https://ocme.evemisslab.com/data/mko/random-variable.json) · [Plain Markdown](https://ocme.evemisslab.com/en/mko/mko-random-variable/index.md)