- 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 \(\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 \(\mu , \nu \) be two finite measures in a standard Borel space \(E\). Let \(\mathcal{A}\) be a subalgebra of \(C_b(E, \mathbb {R})\) that separates points. If for all \(g \in \mathcal A\), \(\mu [g] = \nu [g]\), then for all \(f \in C_b(E, \mathbb {R})\) and all \(\varepsilon {\gt} 0\),
If two probability measures \(\mu , \nu \) have same characteristic function, then for all exponential polynomial \(f \in \mathcal M\), \(\mu [f] = \nu [f]\).
Let \(\mu \) be a finite measure on a Borel space \(E\) and let \(K\) be a measurable compact set such that \(\mu (K^c) \le \varepsilon \). Let \(f \in C(E, \mathbb {R})\). Then
Let \((\mu _n)_{n \in \mathbb {N}}\) be a sequence of measures on a finite-dimensional inner product space \(E\). Let \(b_1, \ldots , b_k\) be an orthonormal basis of \(E\). Then the set \(\{ \mu _n \mid n \in \mathbb {N}\} \) is tight iff for all \(i \in \{ 1, \ldots , k\} \), \(\lim _{r \to +\infty }\limsup _{n \to \infty } \mu _n\{ \vert \langle b_i, x\rangle \vert {\gt} r\} = 0\).
Let \(S\) be a set of measures on a finite-dimensional inner product space \(E\). Let \(b_1, \ldots , b_k\) be an orthonormal basis of \(E\). The \(S\) is tight iff for all \(i \in \{ 1, \ldots , k\} \), \(\lim _{r \to +\infty }\sup _{\mu \in S} \mu \{ \vert \langle b_i, x\rangle \vert {\gt} r\} = 0\).
If two probability measures \(\mu , \nu \) of an inner product space \(E\) are such that \(\mu [f] = \nu [f]\) for all exponential polynomials \(f \in \mathcal M\), then \(\mu = \nu \).
If \(\mu _1, \mu _2, \ldots \) converge weakly to \(\mu \), then \(\{ \mu _n \mid n \in \mathbb {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 pseudo-metric space. Let \(\mathcal A \subseteq C_b(E, \mathbb {C})\) be a star-subalgebra that separates points. Then if two probability measures \(\mu , \nu \) of \(E\) are such that \(\mu [f] = \nu [f]\) for all \(f \in \mathcal A\), then \(\mu = \nu \).
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\).