Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized

Theorem 5

There is a Hippocratic $μ_{p}$ -test such that if $Y$ passes this test then $Y$ computes an accumulation point $q$ of the sequence of sample averages

{{\overset{―}{Y}}_{n}}_{n \in ω} .

LaTeX

Definition 1

The Bernoulli measure $μ_{p}$ is defined by the stipulation that for each $n \in ω = {0, 1, 2, \dots}$ ,

μ_{p} ({X : X (n) = 1}) = p and

μ_{p} ({X : X (n) = 0}) = 1 - p

and $X (0), X (1), X (2), \dots$ are mutually independent random variables.

LaTeX Lean

Definition 10

Let $k \in N$ . An automorphisms of $Z / k Z$ is a bijection $f$ that preserves addition:

f (x + y) = f (x) + f (y)

LaTeX Lean

Definition 11

The additive structure $Z / k Z$ is rigid if it has no nontrivial automorphisms.

LaTeX Lean

Corollary 7

If $Y$ is Hippocrates $μ_{p}$ -random then $Y$ Turing computes $p$ .

LaTeX

Proposition 3

Consider a sequence $Y = {Y_{n}}_{n \in ω}$ of independent Bernoulli( $p$ ) random variables, with the sample average

{\overset{―}{Y}}_{n} := \frac{1}{n} \sum_{i = 0}^{n - 1} Y_{i} .

Let $N (b) = 2^{3 b - 1}$ and let

U_{d} = ⋃_{b \geq d} {Y : | {\overset{―}{Y}}_{N (b)} - p | \geq 2^{- b}} .

Then $U_{d}$ is uniformly $Σ_{1}^{0} (p)$ , and $μ_{p} (U_{d}) \leq 2^{- d}$ , i.e., ${U_{d}}_{d \in ω}$ is a $μ_{p}$ -ML-test.

LaTeX

Definition 2

A $μ_{p}$ -ML-randomness test is a sequence ${U_{n}^{p}}_{n}$ that is uniformly $Σ_{1}^{0} (p)$ with $μ (U_{n}^{p}) \leq 2^{- n}$ , where $2^{- n}$ may be replaced by any computable function that goes to zero effectively.

A $μ_{p}$ -ML-randomness test is Hippocratic if there is a $Σ_{1}^{0}$ class $S \subseteq 2^{ω} \times ω$ such that $S = {(X, n) : X \in U_{n}^{p}}$ . Thus, $U_{n} = U_{n}^{p}$ does not depend on $p$ and is uniformly $Σ_{1}^{0}$ . If $X$ passes all $μ_{p}$ -randomness tests then $X$ is $μ_{p}$ -random. If $X$ passes all Hippocratic tests then $X$ is Hippocrates $μ$ -random.

LaTeX

Theorem 8

For all $p$ , if there is a Hippocratic $μ_{p}$ -test ${U_{n}}_{n \in ω}$ such that ${X : X ≱_{T} p} \subseteq \cap_{n} U_{n}$ , then $p$ is computable.

LaTeX

Corollary 9

There is no universal Hippocratic $μ_{p}$ -test, unless $p$ is computable.

LaTeX

Theorem 4

If $Y$ is $μ_{p}$ -ML-random then $Y$ Turing computes $p$ .

LaTeX

Theorem 6

If $Y$ is Hippocrates $μ_{p}$ -random then $Y$ satisfies the Strong Law of Large Numbers for $p$ .

LaTeX

Theorem 12

The additive structure $Z / 2 Z$ is rigid.

LaTeX Lean