Let $Z_x \sim \mathcal{N}(x,1)$, $D_1 = [0,c]$, and $D=[-c,c]$. Can we determine $x$ from $$f(x) = \mathbb{P}(Z_x\in D_1 | Z_x\in D) = \frac{\Phi(c - x) - \Phi(-x)}{\Phi(c - x) - \Phi(-c-x)}?$$ In particular, can we validate the (numerically obvious) claim that $f$ is monotone, ranging from $0$ to $1$? Even $\lim_{x\to\infty}f(x) = 1$ doesn't seem obvious to me; L'Hospital's rule isn't illuminating there.
A clear approach to this is to consider the derivative $$ \begin{align*} f'(x) &= \frac{f(x)\bigl(\phi(c-x)-\phi(-c-x)\bigr) - \bigl(\phi(c-x) - \phi(-x)\bigr)}{\mathbb{P}(Z_x\in D)}\\ &\propto f(x)\bigl(\phi(c-x)-\phi(-c-x)\bigr) - \bigl(\phi(c-x) - \phi(-x)\bigr), \end{align*} $$ and show that $f'>0$ uniformly, but I can't seem to bound this either. Answers to either would be extremely helpful, but injectivity of $f$ is more important for my application. If you could come up with a version of this that works for higher dimensional Gaussians ($D_i$ are orthants/quadrants of spheres then) that would be perfect.
First of all assume $c=1$ and $x>0$
now call
$$I_1(x) \equiv \sqrt{2\pi}\mathbb{P}(Z_x\in D_1)=\int_0^1e^{-\frac{(t-x)^2}{2}}dt$$
and
$$I(x) \equiv \sqrt{2\pi} \mathbb{P}(Z_x\in D)=\int_{-1}^1e^{-\frac{(t-x)^2}{2}}dt$$
then $$I(x)-I_1(x) = \int_{-1}^0e^{-\frac{(t-x)^2}{2}}dt \leq e^{-x^2/2}$$
But now choose an arbitrary $0<\epsilon<1$ then
$$I_1(x) \geq \int_{\epsilon}^1e^{-\frac{(t-x)^2}{2}}dt \geq (1-\epsilon)e^{-(x-\epsilon)^2/2}$$
but $e^{-x^2/2} = o_{x\rightarrow+\infty}(e^{-(x-\epsilon)^2/2})$
so it's easy to conclude that $I(x) - I_1(x) = o(I_1(x))$ in other words
$$\lim_{x\rightarrow+\infty} f(x) = 1$$
By a similar argument one has $\lim_{x\rightarrow-\infty}f(x)=0$.
Next for monotonicity:
$$f' = \frac{I_1'I-I_1I'}{I^2}$$
so we want to show that $\frac{I'_1}{I_1}\geq \frac{I'}{I}$, so first let's write
$$I'(x) = \int_{-1}^1(t-x)e^{-\frac{(t-x)^2}{2}}dt = -xI(x) + \int_{-1}^1te^{-\frac{(t-x)^2}{2}}dt$$
and
$$I_1'(x) = \int_{0}^1(t-x)e^{-\frac{(t-x)^2}{2}}dt = -xI_1(x) + \int_{0}^1te^{-\frac{(t-x)^2}{2}}dt$$
therefore
$$\frac{I_1'}{I_1} - \frac{I'}{I} = \frac{1}{I_1}\int_{0}^1te^{-\frac{(t-x)^2}{2}}dt - \frac{1}{I}\int_{-1}^1te^{-\frac{(t-x)^2}{2}}dt \geq 0$$
where the inequality holds because $I_1<I$ and $\int_{0}^1te^{-\frac{(t-x)^2}{2}}dt > \int_{-1}^1te^{-\frac{(t-x)^2}{2}}dt$
So in 1D the function is a monotonic bijection from $\mathbb{R}\rightarrow ]0,1[$
It is pretty clear that this line of argument extends to higher dimensions essentially by doing similar explicit tricks on the edge of the octant domain in each direction and evaluating the gradient of f(x) explicitly