Extending the concept of distribution function to any totally or partially ordered measurable space

Question

Let $(\Omega,\mathcal A, P)$ be a probability space. Let $(Y,\Sigma)$ be a measurable space. Let $X:(\Omega,\mathcal A) \to (Y, \Sigma)$ be a random variable. Then $X$ has probability measure $\mu_X = P \circ X^{-1}$, also called the distribution of $X$, in the probability space, also called the distribution space, $(Y, \Sigma, \mu_X)$.

In Wikipedia and other Google search, the concept of a distribution function $F_X: Y \to [0,1]$ in measure theory and probability theory seems to be limited to the case where $Y = \Re$, where

$$F_X(t) = P(\{\omega \in \Omega : X(\omega) \leq t\})$$

For example this Wikipedia definition of distribution function is limited to $Y= \Re$:

Let $ \mu $ be a measure on the real numbers, equipped with the Borel $\sigma$-algebra. Then the function $$ F_\mu \colon \Re \to \Re \cup \{ +\infty, - \infty \} $$ defined by $$ F_\mu(t)= \begin{cases} \mu((0,t]) & \text{if } t\geq 0 \\ -\mu((t,0]) & \text{if } t < 0\end{cases}$$ is called the (right continuous) distribution function of the measure $ \mu $.

Similarly, in these lecture notes on measure theory, the concept of a distribution function $F: Y \to [0,1]$ is limited to domain $\Re$:

Definition 4. A map $F:\Re\to[0,1]$ is said to be a distribution function if it is increasing, right continuous and $F(-\infty) = 0 = 1-F(\infty)$.

even though the concept of a distribution $\mu: \Sigma \to [0,1]$ is stated more generally:

Definition 7. Let $Y$ be a metric space. A $Y$-valued random variable on a probability space $(X,\Sigma,p)$ induces a Borel probability measure on $Y$ as follows: $$p_x(S) = p(x^{-1}(S))$$ for every $S \in B(Y)$. This is the distribution of $x$. If $Y =\Re$, then we call this the distribution function of $x$.

Q. Can the restriction of $Y$ to $\Re$ be lifted in case $Y$ has a total or partial order? This is exactly the point I am trying to generalize. In place of "If $Y=\Re$" I want to say "If $Y$ is totally ordered" or "If $Y$ is partially ordered" or something of this nature which indicates that $Y$ has enough order to define a distribution function as opposed to a distribution. This is the essence of the question, no more no less. The above definition seems to work fine for any totally ordered $Y$. Actually, since only $\leq$ is involved, it seems that we really only need $Y$ to be partially ordered.

Answer 1

Straw man answer. This question isn't attracting answers, so I'll do the best I can. If you downvote this answer, please give your rationale in the comments or provide a better answer.

Let

• $(Y, d)$ be a metric space
• $(X, \Sigma, P)$ be a probability space
• $V: (X, \Sigma) \to (Y,d)$ be a $Y$-valued random variable
• $V^{-1}(E) = \{x \in X: V(x) \in E\}$ be the generalized inverse of $V$
• $\mu_V(E) = P(V^{-1}(E))$ be the distribution
• $F_V(E) = P(\{x \in X: V(x) \leq e\})$ be the distribution function

Clearly $F_V(E)$ is well defined for any metric space $(Y,d)$ provided with a relation $a \leq b$ for all $a,b \in Y$.

From this question:

• All metric spaces can be totally ordered.
• Not all metric spaces have a total order which is "compatible with the ring structure". (So: not sensible or useful in that specific sense.) For example, the complex numbers $\mathbb C$.

So in the strict sense that all metric spaces can be totally ordered, the distribution function always exists, but it may be "uninteresting".

So to be "obviously useful", it is only necessary to stipulate that the metric space $(Y,d)$ is an "obviously useful" ordered metric space. Here we have range of possible more or less useful orderings:

• $Y$ is a partially ordered set
• $Y$ has a partial order compatible with the ring structure
• $Y$ is a totally ordered set
• $Y$ is a Complete metric space

Following this discussion in Zulip, for random variable whose codomain is a a measurable space with a preorder, the generalized distribution function can be constructed in Lean as follows:

import measure_theory.lebesgue_measure
import tactic

noncomputable theory

open measure_theory

class probability_space (α : Type*) extends measure_space α :=
(is_probability_measure :  probability_measure volume)

namespace probability_space
variables {α : Type*} [probability_space α]

lemma volume_univ : volume (set.univ : set α) = 1 :=
is_probability_measure.measure_univ

lemma volume_le_one (S : set α) : volume S ≤ 1 :=
by rw ← @volume_univ α; exact measure_mono (set.subset_univ _)

def prob (S : set α) : ℝ := (volume S).to_real

def nnprob (S : set α) : nnreal := (volume S).to_nnreal

theorem volume_eq_nnprob (S : set α) : volume S = nnprob S :=
(ennreal.coe_to_nnreal $ ne_top_of_le_ne_top (by rintro ⟨⟩) (volume_le_one S)).symm

theorem prob_eq_nnprob (S : set α) : prob S = nnprob S := rfl

theorem nnprob_le_one (S : set α) : nnprob S ≤ 1 :=
ennreal.coe_le_coe.1 $ by rw ← volume_eq_nnprob; exact volume_le_one S

theorem prob_le_one (S : set α) : prob S ≤ 1 := nnprob_le_one _

theorem zero_le_prob (S : set α) : 0 ≤ prob S := nnreal.zero_le_coe

theorem nnprob_mono {S T : set α} (h : S ⊆ T) : nnprob S ≤ nnprob T :=
ennreal.coe_le_coe.1 $ by simpa only [← volume_eq_nnprob] using measure_mono h

theorem prob_mono {S T : set α} (h : S ⊆ T) : prob S ≤ prob T :=
nnreal.coe_le_coe.2 $ nnprob_mono h

end probability_space

theorem measurable.map_probability_measure {α β} [probability_space α] [measurable_space β]
  {f : α → β} (hf : measurable f) :
  probability_measure (measure.map f volume) :=
⟨by rw measure_theory.measure.map_apply hf is_measurable.univ;
    exact probability_space.volume_univ⟩

structure random_variable (α β : Type*) [probability_space α] [measurable_space β] :=
(outcome : α → β)
(is_measurable_outcome : measurable outcome)

variables {α β : Type*} [probability_space α] [measurable_space β]

namespace random_variable
instance : has_coe_to_fun (random_variable α β) := ⟨_,outcome⟩
variable (X : random_variable α β)
lemma measurable : measurable X := X.is_measurable_outcome

-- distribution of X
def induced (X : random_variable α β) : probability_space β :=
{ volume := measure.map X volume,
  is_probability_measure := X.measurable.map_probability_measure }

variables [preorder β]

-- distribution function of X
def CDF (x : β) : 
  ℝ := @probability_space.prob _ X.induced {c | c ≤ x}

lemma prob_eq_CDF (x : β) : X.CDF x = @probability_space.prob β X.induced {c | c ≤ x} := rfl

theorem zero_le_CDF (x : β) : 0 ≤ X.CDF x := 
begin
  rw prob_eq_CDF,
  exact (@probability_space.zero_le_prob β X.induced {c : β | c ≤ x}),
end
 
theorem CDF_le_one (x : β) : X.CDF x ≤ 1 := 
begin
  rw prob_eq_CDF,
  exact (@probability_space.prob_le_one β X.induced {c : β | c ≤ x}),
end

-- distribution function of X with codomain correctly restricted to [0,1]
def CDF_in_01 (x: β) : set.Icc (0 : ℝ) 1 := ⟨ X.CDF x, X.zero_le_CDF x, X.CDF_le_one x⟩

-- Example of a measurable codomain

variables [topological_space β] [order_closed_topology β] [opens_measurable_space β]

example (b : β) : is_measurable {c | c ≤ b} := is_closed.is_measurable is_closed_Iic

end random_variable