Christodoulou actually doesn't give the complete proof (which is why I said a proof needs to be extracted). Here let me give a proof of the geometric fact (the connection with the analysis will have to be made via suitable definitions of space-like and time-like).
Fix a smooth manifold $M$. A causal structure $\mathcal{C}$ on $M$ is the ordered pair of two open subsets $(C,C') \subset TM\times T^*M$ with the following properties
- For any point $p\in M$, $C_p := C \cap T_pM$ is an open convex cone in $T_pM$. Similarly $C'_p$ is an open convex cone in $T^*_pM$.
- For any $v\in C_p$ and $\xi\in C'_p$, we have $\xi(v) > 0$
A vector $v\in C_p$ is said to be future time-like. A hyperplane $S\subset T_pM$ is said to be space-like if there exists $\xi\in C'_p$ such that $\xi|_S \equiv 0$. A vector is said to be space-like if it lies in a space-like hyperplane. (Claim: the set of space-like vectors is an open set.)
Denote by $(C'_p)^*$ the convex dual of $C'_p$. That is:
$$ T_pM \supset (C'_p)^* := \{ w : \xi(w) > 0 \quad \forall \xi\in C'_p\} $$
So by definition we assumed $C\subset (C'_p)^*$. This in particular implies that the set of space-like and time-like vectors are disjoint. (Note that we allow the possibility that a vector is neither space-like nor time-like: that is if $w\in (C'_p)^* \setminus C_p$.)
(Note that this definition of time-like and space-like corresponds to what gives good energy estimates.)
We take the following definitions:
Defn A lens-shaped domain $D\subset M$ based on $\Sigma$ is the image of a smooth map $\Phi: \Sigma\times (-1,1) \to M$ where $\Sigma\subset M$ is a compact, codimension 1 submanifold with boundary, with the property that
- $\Phi(\cdot,0):\Sigma\to\Sigma$ is the identity map.
- $\Phi(x,t) = \Phi(x,s)$ for any $x\in\partial\Sigma$, $t,s\in (-1,1)$.
- for any fixed $s\in (-1,1)$, $\Phi(\Sigma, s)$ is a space-like hypersurface.
- away from $\partial\Sigma\times (-1,1)$, $\Phi$ is a diffeomorphism.
(the last condition I think is technical. One may be able to remove it. But for proving energy estimates, this induced foliation is used in the Gronwall inequality, so we might as well keep it.)
Now, a curve $\gamma\subset M$ is said to be causal if $T\gamma \subset \overline{ (C')^* \cup -(C')^*}$.
Defn A globally hyperbolic development of $\Sigma$ is a subset $I\subset M$ such that for any inextensible causal curve $\gamma$
- $\gamma \cap I$ has at most one connected component
- if $\gamma\cap I\neq \emptyset$, then $\gamma$ intersects the interior of $\Sigma$.
Note that by the definition $\partial\Sigma$ cannot be in $I$.
Rmrk If in the definition of causal curve we use $C$ instead of $(C')^*$, the number of admissible curves $\gamma$ decreases, and so would give a looser definition.
Prop A lens shaped domain $D(\Sigma)\setminus \partial\Sigma$ is a globally hyperbolic development $I(\Sigma)$.
Proof Using that $\Phi$ restricts to a diffeomorphism, $\gamma\cap D(\Sigma)\setminus\partial\Sigma$ lifts to a curve $\tilde\gamma$ in the interior of $\Sigma\times(-1,1)$. Let $\tilde\gamma_0$ be a connected component. If the desired conclusion were to not hold, WLOG we can assume that the infimum of the projection onto $(-1,1)$ of $\tilde\gamma_0$ is not $t_m > -1$. That $\gamma$ is causal implies that $\tilde\gamma$ is transveral to the constant time surfaces, and so along the curve the projection is monotonic. Hence by inextendibility of $\gamma$ one can continuously extend $\tilde\gamma_0$ to intersect $\partial\Sigma\times\{t_m\}$. But this implies that $\gamma$ intersects $\partial\Sigma$ with $T\gamma$ there being space-like, a contradiction.
Off the top of my head I don't have a good proof for the reverse implication. There are two problems involved: to properly develop causal relations and be able to take limits seems to require dealing with $C^0$ but piecewise smooth curves, and with this developed one can indeed connect the notion of a development to Leray's notion of global hyperbolicity (see, e.g. O'Neill Semi-Riemannian Geometry; the proofs there if suitably modified should also work to show that a development in the sense of time-like curves is globally hyperbolic). The problem then is to bring this notion back to the notion of lens-shaped spaces. Presumeably this was already done by Leray, since he was able to prove well-posedness of hyperbolic equations on such domains.
But what I want to emphasize again here is that any possible dual implications must use the set $(C')^*$ to define causal curves, and not $C$ (the set of "globally hyperbolic domains defined relative to $C$" is strictly bigger than that for $(C')^*$, if the two are not equal). On the other hand, $C$ constitutes the natural set of "time-like" vectors with regards to which we can use Garding's inequality to get energy estimates. So one must be careful with the definitions to say that the two notions agree.
