8 Debut Theorem
8.1 Choquet’s capacitability theorem
This section is devoted to the proof of Choquet’s capacitability theorem, which is a key ingredient in the proof of the debut theorem. The presentation follows [ Bic02 ] for the definition of analytic sets (that definition changes a lot between sources) and for the general proof steps, and [ HWY19 ] and the PlanetMath website for many of the proofs of individual lemmas. Although the definition of analytic sets in [ HWY19 ] is different, the proofs follow the same general steps and the same ideas, and that book is much more detailed than [ Bic02 ] .
8.1.1 Pavings and Compact systems
A paving is simply a set of sets.
The product of two pavings \(S\) and \(T\) is the set of sets of the form \(s \times t\) where \(s \in S\) and \(t \in T\). We denote that product by \(S \times T\).
For a paving \(S\), we denote by \(S^{\cup f}\) the set of finite unions of sets in \(S\).
For a paving \(S\), we denote by \(S^{\cap f}\) the set of finite intersections of sets in \(S\).
We denote by \(S_\sigma \) the set of countable unions of sets in \(S\).
We denote by \(S_\delta \) the set of countable intersections of sets in \(S\).
If a paving \(S\) is closed under pairwise intersection, then a set \(s\) is in \(S_\delta \) if and only if there exists a monotone decreasing family of sets \((A_n)_{n\in \mathbb {N}}\) in \(S\) such that \(s = \bigcap _{n\in \mathbb {N}} A_n\).
The “monotone decreasing” condition is the only non-trivial part of the statement: without it it would just be the definition of \(S_\delta \). If \(s \in S_\delta \) there exists a family \((B_n)\) that satisfies the condition but may not be monotone. We can then define \(A_n = \bigcap _{k \le n} B_k\), and the family \((A_n)\) is monotone decreasing and satisfies \(\bigcap _{n\in \mathbb {N}} A_n = \bigcap _{n\in \mathbb {N}} B_n = s\).
If a paving \(S\) is closed under pairwise union, then a set \(s\) is in \(S_\sigma \) if and only if there exists a monotone increasing family of sets \((A_n)_{n\in \mathbb {N}}\) in \(S\) such that \(s = \bigcup _{n\in \mathbb {N}} A_n\).
Similar to the proof of Lemma 8.6.
A set of sets \(K\) is a compact system if for every countable family \((C_n)_{n \in \mathbb {N}}\) of sets in \(K\) such that \(\bigcap _{n \in \mathbb {N}} C_n = \emptyset \), there exists a finite subset \(S\) of \(\mathbb {N}\) such that \(\bigcap _{n \in S} C_n = \emptyset \).
The family of compact closed sets of a topological space is a compact system.
The family of compact sets of a T2 topological space is a compact system.
The T2 assumption ensures that compact sets are closed, so the family of compact sets is the family of compact closed sets, which is a compact system by Lemma 8.9.
If \(S \subseteq T\) and \(T\) is a compact system, then \(S\) is a compact system.
Any sequence of sets in \(S\) is a sequence of sets in \(T\), so if the intersection of the sequence is empty, then there is a finite subset of the sequence whose intersection is empty by the compact system property of \(T\).
The family of closed compact intervals of \(\mathbb {R}\) is a compact system.
The product of a countable family of compact systems is a compact system.
The sum of a countable family of compact systems is a compact system.
The product of two compact systems \(S \times T\) is a compact system.
If \(S\) is a compact system, then \(S^{\cup f}\) is a compact system.
If \(S\) is a compact system, then \(S_\delta \) is a compact system.
If \(S\) is a compact system, then \(S^{\cap f}\) is a compact system.
Let \(S\) be a paving of \(\mathcal{X}\) and \(T\) be a compact system of \(\mathcal{K}\). Let \((B_n)_{n \in \mathbb {N}}\) be a monotone decreasing sequence of sets in \((S \times T)^{\cup f}\). Let \(\pi _{\mathcal{X}} : \mathcal{X} \times \mathcal{K} \to \mathcal{X}\) be the projection on \(\mathcal{X}\). Then
8.1.2 Analytic sets
Let \(F\) be a paving of a type \(\mathcal{X}\). A set \(s\) of \(\mathcal{X}\) is said to be \(F\)-analytic if there exists a nonempty type \(\mathcal{K}\) and a compact system \(K\) of \(\mathcal{K}\) with \(\emptyset \in K\) such that \(s\) is the projection on \(\mathcal{X}\) of a set in \((F \times K)_{\sigma \delta }\).
We denote the set of \(F\)-analytic sets by \(\mathcal{A}(F)\).
Lean note: we can’t quantify over universes, so we have to restrict \(\mathcal{K}\) to Type. We have an auxiliary definition IsPavingAnalyticFor that specifies which \(\mathcal{K}\) is used.
Every set in \(F\) is \(F\)-analytic: \(F \subseteq \mathcal{A}(F)\).
If \(F \subseteq G\) and \(s\) is \(F\)-analytic, then \(s\) is \(G\)-analytic: \(\mathcal{A}(F) \subseteq \mathcal{A}(G)\).
If \(s\) is \(F\)-analytic, then there exists a set \(t\) in \(F_\sigma \) such that \(s \subseteq t\).
A countable union of \(F\)-analytic sets is \(F\)-analytic.
A countable intersection of \(F\)-analytic sets is \(F\)-analytic.
Let \(F\) be a set of sets of \(\mathcal{X}\) and \(K\) be a compact system of \(\mathcal{K}\), with \(\emptyset \in K\). If a set \(s\) of \(\mathcal{X} \times \mathcal{K}\) is \(F \times K\)-analytic, then its projection on \(\mathcal{X}\) is \(F\)-analytic.
If \(t \in T\) and \(s\) is \(F\)-analytic, then \(t \times s\) is \((T \times F)\)-analytic: \(T \times \mathcal{A}(F) \subseteq \mathcal{A}(T \times F)\).
If \(s\) is \(F\)-analytic and \(t\) is \(G\)-analytic, then \(s \times t\) is \((F \times G)\)-analytic: \(\mathcal{A}(F) \times \mathcal{A}(G) \subseteq \mathcal{A}(F \times G)\).
\(\mathcal{A}(\mathcal{A}(F)) = \mathcal{A}(F)\).
8.1.3 Analytic sets in measurable spaces
We denote by \(K_{\mathbb {R}}\) the paving of compact sets of \(\mathbb {R}\) and let \(I_{\mathbb {R}}\) be the paving of closed compact intervals of \(\mathbb {R}\). For a measurable space \(\mathcal{X}\), we denote by \(M_{\mathcal{X}}\) the paving of measurable sets of \(\mathcal{X}\).
Let \(F\) be a paving with \(\emptyset \in F\) and let \(\sigma (F)\) be the \(\sigma \)-algebra generated by \(F\). Suppose that for every \(t \in F\), \(t^c\) is \(F\)-analytic. Then every set in \(\sigma (F)\) is \(F\)-analytic: \(\sigma (F) \subseteq \mathcal{A}(F)\).
A measurable set of \(\mathbb {R}\) is \(I_{\mathbb {R}}\)-analytic. That is, \(M_{\mathbb {R}} \subseteq \mathcal{A}(I_{\mathbb {R}})\).
A set of \(\mathbb {R}\) is \(M_{\mathbb {R}}\)-analytic if and only if it is \(I_{\mathbb {R}}\)-analytic.
Let \(\mathcal{X}\) be a measurable space and \(s\) be a measurable set of \(\mathcal{X} \times \mathbb {R}\). Then \(s\) is \((M_{\mathcal{X}} \times I_{\mathbb {R}})\)-analytic.
Let \(\mathcal{X}\) be a measurable space and \(s\) be a set of \(\mathcal{X} \times \mathbb {R}\) which is \((M_{\mathcal{X}} \times I_{\mathbb {R}})\)-analytic. Then the projection \(\pi _{\mathcal{X}}(s)\) is \(M_{\mathcal{X}}\)-analytic.
Let \(\mathcal{X}\) be a measurable space and \(s\) be a measurable set of \(\mathcal{X} \times \mathbb {R}\). Then the projection of \(s\) on \(\mathcal{X}\) is \(M_{\mathcal{X}}\)-analytic.
We say that a set \(s\) of a measurable space \(\mathcal{X}\) is measurably analytic for a measurable space \(\mathcal{K}\) if it is the projection of a measurable set of \(\mathcal{X} \times \mathcal{K}\).
We say that \(s\) is measurably analytic if it is measurably analytic for \(\mathbb {R}\).
Let \(\mathcal{K}\) be a standard Borel space. If a set \(s\) of \(\mathcal{X}\) is measurably analytic for \(\mathcal{K}\), then it is measurably analytic.
There is a measurable embedding of \(\mathcal{K}\) into \(\mathbb {R}\).
If a set \(s\) of \(\mathcal{X}\) is measurably analytic, then it is \(M_{\mathcal{X}}\)-analytic.
8.1.4 Capacities and capacitable sets
Let \(F\) be a set of sets of a type \(\mathcal{X}\). An \(F\)-capacity is a function \(I\) from the sets of \(\mathcal{X}\) to \(\mathbb {R}_{+,\infty }\) such that
\(I\) is monotone for set inclusion: for \(s \subseteq t\), \(I(s) \le I(t)\),
if \((s_n)_{n\in \mathbb {N}}\) is an increasing sequence of sets of \(\mathcal{X}\), then \(I(s_n)\) tends to \(I(\bigcup _{n\in \mathbb {N}} s_n)\) at infinity,
if \((s_n)_{n\in \mathbb {N}}\) is a decreasing sequence of sets in \(F\), then \(I(s_n)\) tends to \(I(\bigcap _{n\in \mathbb {N}} s_n)\) at infinity.
Let \(F\) be a set of sets of \(\mathcal{X}\) and let \(I\) be an \(F\)-capacity. Suppose that \(\emptyset \in F\) and \(F\) is closed under pairwise unions. Let \(K\) be a compact system of \(\mathcal{K}\). Let \(\pi _{\mathcal{X}} : \mathcal{X} \times \mathcal{K} \to \mathcal{X}\) be the projection on the first coordinate. Then the function \(I_{\mathcal{X}}(u) = I(\pi _{\mathcal{X}}(u))\) is a capacity for \((F \times K)^{\cup f}\).
Let \(F\) be a set of sets of \(\mathcal{X}\) and let \(I\) be an \(F\)-capacity. Suppose that \(\emptyset \in F\) and \(F\) is closed under pairwise unions. Let \(K\) be a compact system of \(\mathcal{K}\). Let \(\pi _{\mathcal{X}} : \mathcal{X} \times \mathcal{K} \to \mathcal{X}\) be the projection on the first coordinate. Then we define a capacity for \((F \times K)^{\cup f}\) by \(I_{\mathcal{X}}(u) = I(\pi _{\mathcal{X}}(u))\) (it is indeed a capacity by Lemma 8.40).
Let \(F\) be a set of sets of \(\mathcal{X}\) and let \(I\) be an \(F\)-capacity. A set \(s\) of \(\mathcal{X}\) is said to be \(I\)-capacitable if for all \(a {\lt} I(s)\), there exists a set \(t \in F_\delta \) such that \(t \subseteq s\) and \(a \le I(t)\).
For \(I\) an \(F\)-capacity, every set in \(F\) is \(I\)-capacitable.
Suppose that \(F\) contains the empty set and is closed under pairwise intersections and unions, and let \(I\) be an \(F\)-capacity. Then every set of \(F_{\sigma \delta }\) is \(I\)-capacitable.
Suppose that \(F\) contains the empty set and is closed under pairwise intersections and unions, and let \(I\) be an \(F\)-capacity. Let \(K\) be a compact system which is also closed under pairwise intersections. Let \(s \in ((F \times K)^{\cup f})_\delta \). Then \(\pi _{\mathcal{X}}(s) \in F_\delta \).
Let \(F\) be a set of sets of \(\mathcal{X}\) and let \(I\) be an \(F\)-capacity. Suppose that \(F\) contains the empty set and is closed under pairwise intersections and unions. Let \(K\) be a compact system of \(\mathcal{K}\) which is also closed under pairwise intersections. If a set \(s\) of \(\mathcal{X} \times \mathcal{K}\) is capacitable with respect to the capacity \(I_{\mathcal{X}}\) of Definition 8.41, then its projection on \(\mathcal{X}\) is capacitable with respect to \(I\).
Let \(F\) be a set of sets of \(\mathcal{X}\) and let \(I\) be an \(F\)-capacity. Suppose that \(F\) contains the empty set and is closed under pairwise intersections and unions. Then every \(F\)-analytic set is \(I\)-capacitable.
8.1.5 Capacities and measures
Every finite measure defines a capacity by \(I(s) = \mu (s)\) (where \(\mu (s)\) is the value of the outer measure defined by \(\mu \), but in Lean that’s how \(\mu (s)\) is defined already).
A set is capacitable with respect to the capacity defined by a finite measure if and only if it is null-measurable for this measure.
An \(M_{\mathcal{X}}\)-analytic set of a measurable space \(\mathcal{X}\) is universally measurable: it is null-measurable for every finite measure on \(\mathcal{X}\).
A measurably analytic set of a measurable space \(\mathcal{X}\) is universally measurable: it is null-measurable for every finite measure on \(\mathcal{X}\).
Let \(\mathcal{X}\) and \(\mathcal{Y}\) be measurable spaces, with \(\mathcal{Y}\) standard Borel. Then the projection of a measurable set of \(\mathcal{X} \times \mathcal{Y}\) on \(\mathcal{X}\) is universally measurable.
8.2 Monotone class theorem
Let \(\mathcal{M}\) be a collection of subsets of a set \(X\). We say that \(\mathcal{M}\) is a monotone class if it is closed under countable monotone unions and countable monotone intersections, i.e.:
if \( A_1, A_2, \ldots \in M \) and \( A_1 \subseteq A_2 \subseteq \cdots \), then \( \bigcup _{i=1}^\infty A_i \in M \),
if \( B_1, B_2, \ldots \in M \) and \( B_1 \supseteq B_2 \supseteq \cdots \), then \( \bigcap _{i=1}^\infty B_i \in M \).
Given a collection \(\mathcal{F}\) of subsets of \(X\), we call the smallest monotone class containing \(\mathcal{F}\) the monotone class generated by \(\mathcal{F}\).
Let \(G\) be an algebra of subsets of a set \(X\). Then the monotone class generated by \(G\) coincides with the \(\sigma \)-algebra generated by \(G\).
8.3 Debut Theorem
A subset of \([0, \infty ) \times \Omega \) is progressively measurable if its indicator is a progressively measurable process.
Let \(E \subseteq {} [0, \infty ) \times \Omega \), define \(D_E = \inf \left\lbrace t \geq 0\ :\ (t, \omega ) \in E\right\rbrace \), the debut of \(E\).
If \(E\) is a progressively measurable set and the filtration satisfies the usual conditions, then \(D_E\) is a stopping time.
8.4 Hitting times
If \(X : T \to \Omega \to E\) is a progressively measurable process with respect to a filtration satisfying the usual conditions and \(B\) is a Borel-measurable subset of \(E\), then the hitting time of \(X\) in \(B\) is a stopping time.
Since \(B\) is a Borel subset of \(\mathcal{S}\) and \(X\) is progressively measurable, then \(\mathbf{1}_B(X_t)\) is also progressively measurable. The hitting time is then the debut of the set \(E = \{ (s,\omega ) : \mathbf{1}_B(X_s(\omega )) = 1\} \), and therefore is a stopping time by Theorem 8.57.
Let \(T\) be a conditionally complete linear order with a bottom element and let \(R\) be a preorder. For a process \(X : T \to Ω \to R\) and \(a \in R\), define the random time
in which the infimum is infinite if the set is empty.
Let \(T\) be a conditionally complete linear order with a bottom element, which is a Polish space for its order topology, on which we put the Borel \(\sigma \)-algebra. Let \(R\) be a preorder with a metrizable topology for which sets of the form \(\{ x \in R \mid x \ge a\} \) are closed, with its Borel \(\sigma \)-algebra. If \(X : T \to Ω \to R\) is a progressively measurable process with respect to a filtration satisfying the usual conditions, then for any \(a \in R\), the random time \(\tau _{X \ge a}\) is a stopping time.
This is a direct application of Theorem 8.58 with the set \(B = [a, +\infty )\).
If \(X : ι \to Ω \to ℝ\) is a right-continuous and adapted process with respect to a filtration satisfying the usual conditions, then for any \(a \in \mathbb {R}\), the random time \(\tau _{X \ge a}\) is a stopping time.
Let \(T\) be a conditionally complete linear order with a bottom element and let \(R\) be a preorder. For a process \(X : T \to Ω \to R\) and \(a \in R\), define the random time
in which the infimum is infinite if the set is empty.
Let \(T\) be a conditionally complete linear order with a bottom element, which is a Polish space for its order topology, on which we put the Borel \(\sigma \)-algebra. Let \(R\) be a preorder with a metrizable topology for which sets of the form \(\{ x \in R \mid x \ge a\} \) are closed, with its Borel \(\sigma \)-algebra. If \(X : T \to Ω \to R\) is a progressively measurable process with respect to a filtration satisfying the usual conditions, then for any \(a \in R\), the random time \(\tau _{X {\gt} a}\) is a stopping time.
This is a direct application of Theorem 8.58 with the set \(B = (a, +\infty )\).
For \(t \in T\), \(\tau _{X {\gt} a} {\lt} t\) if and only if there exists \(s {\lt} t\) such that \(X_s {\gt} a\).