- 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
Let \(X_1, X_2, \ldots \) be i.i.d. real random variables with mean 0 and variance 1, and let \(Z\) be a random variable with law \(\mathcal N(0,1)\). Then
Let \(\mu \) be a measure on a real inner product space \(E\). The characteristic function of \(\mu \), denoted by \(\hat{\mu }\), is the function \(E \to \mathbb {C}\) defined by
The characteristic function of a random variable \(X\) is defined as the characteristic function of \(\mathcal L(X)\).
We say that \(X_n\) converges in distribution to \(X\) and write \(X_n \xrightarrow {d} X\) if \(\mathcal L(X_n) \xrightarrow {w} \mathcal L(X)\).
We say that \((X_i)_{i \in \mathbb {N}}\) tends to \(X\) in probability (or in measure) in a space with distance function \(d\) if for all \(\varepsilon {\gt} 0\)
We write \(X_n \xrightarrow {p} X\).
In a topological space \(S\) in which the opens are measurable, we say that a sequence of probability measures \(\mu _n\) converges weakly to a probability measure \(\mu \) and write \(\mu _n \xrightarrow {w} \mu \) if \(\mu _n[f] \to \mu [f]\) for every bounded continuous function \(f : S \to \mathbb {R}\).
Let \(X\) be a random variable with law \(\mu \). Then for any \(s, t\),
In a Borel space \(E\), the set \(C_b(E, \mathbb {C})\) of bounded continuous functions from \(E\) to \(\mathbb {C}\) is separating in \(\mathcal P(E)\).
Let \(\mathcal A\) be a subalgebra of \(C_b(E, \mathbb {C})\) that separates points. Let \(\mu , \nu \) be two probability measures. If for all \(f \in \mathcal A\), \(\mu [f] = \nu [f]\), then for all \(g \in C_b(E, \mathbb {C})\), \(\mu [g] = \nu [g]\).
If two random variables \(X, Y : \Omega \to S\) are independent, then \(X+Y\) has characteristic function \(\phi _{X+Y} = \phi _X \phi _Y\).
For \(\mu \) a probability measure on \(\mathbb {R}\) and \(r {\gt} 0\),
For \(a \in \mathbb {R}\), the characteristic function of \(a X\) is \(t \mapsto \phi _X(at)\).
Let \(X\) be a real random variable with characteristic function \(\phi \), with \(\mathbb {E}[\vert X \vert ^n] {\lt} \infty \). Then as \(t \to 0\),
Let \(\mathcal A\) be a separating subalgebra of \(C_b(E, \mathbb {C})\). Let \(\mu , \mu _1, \mu _2, \ldots \) be probability measures, with \((\mu _n)\) tight. If for all \(f \in \mathcal A\), \(\mu _n[f] \to \mu [f]\), then \(\mu _n \xrightarrow {w} \mu \).
Let \(X\) be a real random variable with characteristic function \(\phi \) with \(\mathbb {E}[\vert X \vert ^n] {\lt} \infty \) and let \(k \le n\). Then the \(k\)th derivative of \(\phi \) is \(\phi ^{(k)}(t) = \mathbb {E}[i X]^k e^{i t X}\) .
If two probability measures \(\mu , \nu \) have same characteristic function, then for all exponential polynomial \(f \in \mathcal M\), \(\mu [f] = \nu [f]\).
Let \((U_n)_{n \in \mathbb {N}}\) be open sets in a complete separable metric space \(E\) such that \(\bigcup _{n=1}^{+ \infty } U_n = E\). Let \(\Gamma \) be a relatively compact set of probability measures on \(E\) for the topology of weak convergence of measures. Then for all \(\varepsilon {\gt} 0\) there exists a finite set \(S \subseteq \mathbb {N}\) such that for all \(\mu \in \Gamma \), \(\mu (\bigcup _{n \in S} U_n) {\gt} 1 - \varepsilon \).
For \(f \in \mathcal A\) a subalgebra of \(C_b(E, \mathbb {C})\), \(\varepsilon \ge 0\) and \(n \in \mathbb {N}\), \(f (1 - \frac{\varepsilon }{n} f)^n \in \mathcal A\). Furthermore, for a measure \(\mu \),
Two probability measures on a TODO space are equal iff they have the same characteristic function.
The Gaussian distribution \(\mathcal N(m, \sigma ^2)\) has characteristic function \(\phi (t) = e^{itm - \sigma ^2 t^2 /2}\).
Let \(\mu \) be a measure on \(E\) and \(K\) be a compact set such that \(\mu (K^c) \le \varepsilon \). Let \(f \in C_b(E, \mathbb {C})\). Then
where \(C = \sup _{x \ge 0} x e^{-x^2}\).
For any \(f \in C_b(E, \mathbb {C})\) and probability measures \(\mu , \nu \),
If \(E\) is a compact metric space, then \(\mathcal P(E)\) with the Prokhorov metric is a compact metric space.
Let \(E\) be a complete separable metric space and let \(S \subseteq \mathcal P(E)\). If the closure of \(S\) is compact, then \(S\) is tight.
Let \(E\) be a metric space and let \(S \subseteq \mathcal P(E)\) be tight. Then the closure of \(S\) is compact.
A family of measures \((\mu _a)\) on a finite dimensional inner product space is tight iff the family of functions \((\hat{\mu }_a)\) is equi-continuous at 0.
If \(\mu _1, \mu _2, \ldots \) converge weakly to \(\mu \), then \(\{ \mu _n \mid n \in \mathbb {N}\} \) is tight.
Let \((\mu _n)_{n \in \mathbb {N}}\) be measures on \(\mathbb {R}^d\) with characteristic functions \((\hat{\mu }_n)\). If \(\hat{\mu }_n\) converges pointwise to a function \(f\) which is continuous at 0, then \((\mu _n)\) is tight.
Let \(\mu , \mu _1, \mu _2, \ldots \) be probability measures on \(\mathbb {R}^d\) with characteristic functions \(\hat{\mu }, \hat{\mu }_1, \hat{\mu }_2, \ldots \). Then \(\mu _n \xrightarrow {w} \mu \) iff for all \(t\), \(\hat{\mu }_n(t) \to \hat{\mu }(t)\).
Let \(E\) be a complete separable metric space and let \(S \subseteq \mathcal P(E)\). Then the following are equivalent:
\(S\) is tight.
the closure of \(S\) is compact.
Let \(E\) be a compact T2 space and let \(\psi \) be a positive linear functional on \(C(E, \mathbb {C})\). There exists a regular measure \(\mu \) finite on compacts such that
Let \(E\) be a complete separable pseudo-metric space. Let \(\mathcal A \subseteq C_b(E, \mathbb {C})\) be a star-subalgebra that separates points. Then \(\mathcal A\) is separating in \(\mathcal P(E)\).
For random variables \((X_i)_{i \in \mathbb {N}}\) (TODO in which kind of space?), the two following conditions are equivalent:
\((\mathcal L(X_n))\) is tight,
For all \((c_n) \ge 0\) with \(c_n \to 0\), \(c_n X_n \xrightarrow {p} 0\).