We have been working on the formalization of the probability and the randomness. In [15] and [16], we formalized some theorems concerning the real-valued random variables and the product of two probability spaces. In this article, we present the generalized formalization of [15] and [16]. First, we formalize the random variables of arbitrary set and prove the equivalence between random variable on Σ, Borel sets and a real-valued random variable on Σ. Next, we formalize the product of countably infinite...

In this paper, the authors introduce the notion of conditional expectation of an observable $x$ on a logic with respect to a sublogic, in a state $m$, relative to an element $a$ of the logic. This conditional expectation is an analogue of the expectation of an integrable function on a probability space.

The ring $B\left(R\right)$ of all real-valued measurable functions, carrying the pointwise convergence, is a sequential ring completion of the subring $C\left(R\right)$ of all continuous functions and, similarly, the ring $𝔹$ of all Borel measurable subsets of $R$ is a sequential ring completion of the subring ${𝔹}_0$ of all finite unions of half-open intervals; the two completions are not categorical. We study ${ℒ}_0^{*}$-rings of maps and develop a completion theory covering the two examples. In particular, the $\sigma$-fields of sets form an epireflective...