[proofplan] We prove that the open star-shaped domain $\Omega_p$ is exactly the set of nonzero tangent vectors whose radial geodesics have not yet reached the cut locus. Before the cut time, the radial geodesic is the unique minimizing geodesic from $p$, and the cut locus theorem implies that no conjugate point has occurred; hence the exponential map has invertible differential there. Local invertibility follows from the [inverse function theorem](/page/Inverse%20Function%20Theorem), and uniqueness of minimizing geodesics patches these local inverses into a global diffeomorphism onto $U$. Finally, the Gauss lemma gives orthogonality between radial and angular directions, so the polar-coordinate expression of the metric has no mixed terms and decomposes as $dr \otimes dr + g_r$. [/proofplan]

[step:Identify the image of $\Omega_p$ with the complement of the point and cut locus] For $v \in S_pM$, let \begin{align*} \gamma_v: [0,\infty) &\to M \\ s &\mapsto \exp_p(sv) \end{align*} be the unit-speed geodesic with $\gamma_v(0)=p$ and $\dot{\gamma}_v(0)=v$. Since $M$ is complete, $\gamma_v$ is defined for all $s \geq 0$ by geodesic completeness. By the definition of $c(v)$, if $0<r<c(v)$, then $\gamma_v|_{[0,r]}$ is minimizing from $p$ to $\gamma_v(r)$, and $\gamma_v(r)$ is not the cut point $\gamma_v(c(v))$. Hence \begin{align*} \exp_p(\Omega_p) \subset M \setminus \bigl(\{p\}\cup \operatorname{Cut}(p)\bigr)=U. \end{align*} Conversely, let $q \in U$. Since $M$ is complete and connected, the Hopf-Rinow theorem gives a minimizing unit-speed geodesic \begin{align*} \gamma: [0,\ell] &\to M \end{align*} from $p$ to $q$, where $\ell=d_g(p,q)>0$. Let $v:=\dot{\gamma}(0) \in S_pM$. Then $\gamma(s)=\exp_p(sv)$ for $0\leq s\leq \ell$. If $\ell \geq c(v)$, then either $\ell=c(v)$ and $q=\exp_p(c(v)v)\in \operatorname{Cut}(p)$, or $\ell>c(v)$ and the point $\exp_p(c(v)v)$ lies on the minimizing segment from $p$ to $q$, contradicting the definition of $c(v)$ as the first endpoint beyond which the radial geodesic ceases to minimize. Therefore $\ell<c(v)$, so $\ell v \in \Omega_p$ and $q=\exp_p(\ell v)$. Thus \begin{align*} \exp_p(\Omega_p)=U. \end{align*} Here the Hopf-Rinow theorem and the standard existence of minimizing geodesics on complete connected Riemannian manifolds are used as background results not yet resolved to wiki theorem IDs. [/step]

[step:Prove uniqueness of the polar representation before the cut time]Suppose \begin{align*} \exp_p(rv)=\exp_p(sw) \end{align*} with $v,w\in S_pM$, $0<r<c(v)$, and $0<s<c(w)$. Since $r<c(v)$ and $s<c(w)$, both geodesic segments \begin{align*} \gamma_v|_{[0,r]}: [0,r] &\to M, & t &\mapsto \exp_p(tv), \\ \gamma_w|_{[0,s]}: [0,s] &\to M, & t &\mapsto \exp_p(tw) \end{align*} are minimizing from $p$ to the common endpoint $q:=\exp_p(rv)=\exp_p(sw)$. Therefore \begin{align*} r=d_g(p,q)=s. \end{align*} If $v\neq w$, then two distinct minimizing geodesics from $p$ reach the same point $q$ at time $r$. By the standard cut locus characterization, the first time along a radial geodesic at which either a second minimizing geodesic reaches the same endpoint or a conjugate point occurs is precisely the cut time. Hence $q$ would lie at or beyond the cut point along $\gamma_v$, forcing $r\geq c(v)$, contrary to $r<c(v)$. Thus $v=w$, and the representation is unique.[/step]

[guided]Assume that the same point has two polar representations before the corresponding cut times: \begin{align*} \exp_p(rv)=\exp_p(sw), \end{align*} where $v,w\in S_pM$, $0<r<c(v)$, and $0<s<c(w)$. Define the common endpoint by \begin{align*} q:=\exp_p(rv)=\exp_p(sw). \end{align*} The two radial curves are the maps \begin{align*} \gamma_v|_{[0,r]}: [0,r] &\to M, & t &\mapsto \exp_p(tv), \\ \gamma_w|_{[0,s]}: [0,s] &\to M, & t &\mapsto \exp_p(tw). \end{align*} Because $r<c(v)$ and $s<c(w)$, the definition of the cut time says that both of these segments are minimizing geodesics from $p$ to $q$. Therefore their lengths equal the Riemannian distance from $p$ to $q$: \begin{align*} r=d_g(p,q)=s. \end{align*} It remains to rule out $v\neq w$. If $v\neq w$, then the two maps $\gamma_v|_{[0,r]}$ and $\gamma_w|_{[0,r]}$ are distinct minimizing geodesics from $p$ to the same endpoint $q$. The standard cut locus characterization says that the first loss of uniqueness or nonsingularity of the radial exponential map occurs at the cut time: before $c(v)$, the radial geodesic is the unique minimizing geodesic from $p$ to its endpoint and has no conjugate endpoint. Thus the existence of a second minimizing geodesic to $q=\gamma_v(r)$ would force $r\geq c(v)$. This contradicts $r<c(v)$. Hence $v=w$, and since we already proved $r=s$, the polar representation is unique. This step uses the standard cut locus characterization as a background result not yet resolved to a wiki theorem ID.[/guided]

[step:Show that the exponential map is locally invertible on $\Omega_p$] Let $a=rv\in \Omega_p$, where $v\in S_pM$ and $0<r<c(v)$. By the standard cut locus theorem, no point $\gamma_v(t)=\exp_p(tv)$ with $0<t<c(v)$ is conjugate to $p$ along $\gamma_v$. In particular, $a$ is not a conjugate vector, so the [linear map](/page/Linear%20Map) \begin{align*} d(\exp_p)_a: T_a(T_pM) \to T_{\exp_p(a)}M \end{align*} is an isomorphism. The [inverse function theorem](/theorems/51) applied to the smooth map \begin{align*} \exp_p: T_pM \supset \Omega_p \to M \end{align*} therefore gives open neighbourhoods $V_a\subset \Omega_p$ of $a$ and $W_a\subset M$ of $\exp_p(a)$ such that \begin{align*} \exp_p|_{V_a}: V_a \to W_a \end{align*} is a diffeomorphism. The inverse function theorem and the equivalence between non-conjugacy and invertibility of $d(\exp_p)_a$ are used as background results not yet resolved to wiki theorem IDs. [/step]

[step:Patch the local inverses into a global diffeomorphism] The map $\exp_p|_{\Omega_p}:\Omega_p\to U$ is smooth, surjective by the first step, and injective by uniqueness of the polar representation. The preceding step shows that it is a local diffeomorphism at every point of $\Omega_p$. Therefore its inverse \begin{align*} (\exp_p|_{\Omega_p})^{-1}:U\to \Omega_p \end{align*} is smooth locally on each coordinate neighbourhood $W_a$, because on $W_a$ it agrees with the smooth inverse of $\exp_p|_{V_a}$. Hence $\exp_p|_{\Omega_p}$ is a global diffeomorphism from $\Omega_p$ onto $U$. [/step]

[step:Use the Gauss lemma to eliminate radial-angular cross terms] Define the polar coordinate domain \begin{align*} D_p:=\{(r,v)\in (0,\infty)\times S_pM:0<r<c(v)\} \end{align*} and the polar coordinate map \begin{align*} P:D_p&\to U\\ (r,v)&\mapsto \exp_p(rv). \end{align*} For $(r,v)\in D_p$, the tangent space splits as \begin{align*} T_{(r,v)}D_p = \mathbb{R}\partial_r \oplus T_vS_pM. \end{align*} The radial derivative is \begin{align*} dP_{(r,v)}(\partial_r)=\dot{\gamma}_v(r), \end{align*} so, since $\gamma_v$ is unit-speed, \begin{align*} g_{P(r,v)}\bigl(dP_{(r,v)}(\partial_r),dP_{(r,v)}(\partial_r)\bigr)=1. \end{align*} For $\xi\in T_vS_pM$, differentiating the map $(r,v)\mapsto rv$ in the angular direction gives the tangent vector $r\xi\in T_{rv}(T_pM)$, hence \begin{align*} dP_{(r,v)}(\xi)=d(\exp_p)_{rv}(r\xi). \end{align*} The Gauss lemma states that the differential of the exponential map sends radial and angular tangent directions to $g$-orthogonal tangent vectors. Therefore \begin{align*} g_{P(r,v)}\bigl(dP_{(r,v)}(\partial_r),dP_{(r,v)}(\xi)\bigr)=0 \end{align*} for every $\xi\in T_vS_pM$. Define, for each $r>0$ and $v\in S_pM$ with $r<c(v)$, the angular [bilinear form](/page/Bilinear%20Form) \begin{align*} (g_r)_v:T_vS_pM\times T_vS_pM&\to \mathbb{R}\\ (\xi,\eta)&\mapsto g_{\exp_p(rv)}\bigl(d(\exp_p)_{rv}(r\xi),d(\exp_p)_{rv}(r\eta)\bigr). \end{align*} Since $P$ is a diffeomorphism, $dP_{(r,v)}$ is injective; hence $(g_r)_v$ is positive definite on $T_vS_pM$. Smoothness of $g_r$ follows from smoothness of $g$, of $\exp_p$, and of the multiplication map $(r,v)\mapsto rv$. Thus, with respect to the decomposition $\mathbb{R}\partial_r\oplus T_vS_pM$, the pulled-back metric satisfies \begin{align*} P^*g = dr\otimes dr + g_r. \end{align*} This is the asserted geodesic polar coordinate form. The Gauss lemma is used here as a background result not yet resolved to a wiki theorem ID. [/step]