Gauss lemma

Openness in [F1] gives $\eta >0$ such that $v+sw\in {\mathcal{E}}_p$ for $\mathrm{\mid }s\mathrm{\mid }<\eta$. Star-shapedness then makes $F(s,t)={\exp }_p(t(v+sw))={\gamma }_{p,v+sw}(t)$ a smooth map for $\mathrm{\mid }s\mathrm{\mid }<\eta$ and $0\le t\le 1$. Put $J={\mathrm{\partial }}_{s}F{\mathrm{\mid }}_{s=0}$ and $R={\mathrm{\partial }}_{t}F{\mathrm{\mid }}_{s=0}$. Then $J(1)=d({\exp }_p{)}_v(w)$ and $R(t)={\dot{\gamma }}_{p,v}(t)$.

For $f(t)=g(J(t),R(t))$, metric compatibility gives $f^{\mathrm{\prime }}=g(D_{t}J,R)+g(J,D_{t}R)\mathrm{.}$ Each longitudinal curve of $F$ is a geodesic, so the second term is zero. In local coordinates, mixed-partial equality and the Christoffel symmetry in [F2] give $D_t{\mathrm{\partial }}_{s}F=D_s{\mathrm{\partial }}_{t}F$. Therefore [F3] yields $f^{\mathrm{\prime }}(t)=g(D_s{\mathrm{\partial }}_{t}F,R){\mathrm{\mid }}_{s=0}={\frac{1}{2}{\mathrm{\partial }}_s\mid }_0\mathrm{\mid }{\mathrm{\partial }}_{t}F{\mathrm{\mid }}_g^2={\frac{1}{2}{\mathrm{\partial }}_s\mid }_0\mathrm{\mid }v+sw{\mathrm{\mid }}_g^2=g_p(v,w)\mathrm{.}$

Since $F(s,0)=p$, one has $J(0)=0$ and hence $f(0)=0$. Subtracting $t{g}_p(v,w)$ from $f$ gives a function with zero derivative, so [F3] gives $f(t)=t{g}_p(v,w)$. At $t=1$ this is $g_{{\exp }_p(v)}(d({\exp }_p{)}_v(w),{\dot{\gamma }}_{p,v}(1))=g_p(v,w)\mathrm{.}$

Differentiating the scaling identity ${\exp }_p((1+s)v)={\gamma }_{p,v}(1+s)$ at $s=0$ gives $d({\exp }_p{)}_v(v)={\dot{\gamma }}_{p,v}(1)$. Substitution in step 3.1 proves the asserted bilinear identity. Taking $w=v$ proves $\mathrm{\mid }d({\exp }_p{)}_v(v){\mathrm{\mid }}_g^2=\mathrm{\mid }v{\mathrm{\mid }}_g^2$.

Let $v\mathrm{\ne }0$ and $r=\mathrm{\mid }v{\mathrm{\mid }}_g$. If a smooth curve $c(s)$ in the radius-$r$ sphere has $c(0)=v$ and $c^{\mathrm{\prime }}(0)=w$, differentiating $\mathrm{\mid }c(s){\mathrm{\mid }}_g^2=r^2$ gives $g_p(v,w)=0$. Conversely, when $g_p(v,w)=0$, the curve $c(s)=r(v+sw)\mathrm{/}\mathrm{\mid }v+sw{\mathrm{\mid }}_g$ is defined near zero, lies in that sphere, and has derivative $w$ at zero. Thus the tangent space is exactly $v^{\perp }$, and step 4.1 proves the orthogonality assertion.

At $v=0$ the radial vector and its image are zero, so both identities hold; the radius-zero sphere claim was explicitly restricted to $v\mathrm{\ne }0$. In dimension zero only this case occurs; in dimension one a positive-radius sphere has zero tangent space. An empty manifold has no $p$. The parameter endpoints $t=0,1$ lie in the smooth variation supplied by star-shapedness, and no exponential-domain boundary point is used. Assumption [A1] is used exactly through [F1] for the global exponential construction; the finite-dimensional calculation adds no choice.