Let $X$ and $Y$ be two bivariate normally distributed random variables with means $\mu_X$ and $\mu_Y$ and variances $\sigma_X^2$ and $\sigma_Y^2$. The covariance is $Cov(X,Y) = \rho\sigma_X\sigma_Y$, where $\rho$ measures the correlation between $X$ and $Y$.
Suppose you receive a single measurement of the specific value of $X$, which is generated by a random process $z = x + \epsilon$, where $\epsilon$ is normally distributed (and independent of $X,Y$) with mean zero and variance $\sigma_\epsilon^2$.
One can pretty straightforwardly apply known results from the multivariate normal distribution (e.g. here) to derive the updated mean and variance of $X$ and $Y$:
$$ E(X|z) = \mu_X + \frac{\sigma_X^2}{\sigma_X^2+\sigma_\epsilon^2}(z - \mu_X),\quad E(Y|z) = \mu_Y + \frac{\rho\sigma_X\sigma_Y}{\sigma_X^2+\sigma_\epsilon^2}(z - \mu_X),\quad Var(X|z) = \frac{\sigma_X^2\sigma_\epsilon^2}{\sigma_X^2+\sigma_\epsilon^2},\quad Var(Y|z) = \frac{\sigma_Y^2\sigma_\epsilon^2}{\sigma_X^2+\sigma_\epsilon^2}\left(1 + (1-\rho^2)\sigma_X^2/\sigma_\epsilon^2\right).$$ How would I go about deriving the covariance term $Cov(X,Y|z)$ in this case? I am pretty sure (and it also seems intuitive) that the following equality holds: $$ \frac{Cov(X,Y|z)}{Var(X|z)} = \frac{Cov(X,Y)}{Var(X)}.$$ If this equality is true, one can solve for the updated correlation coefficient which becomes $$\rho|z = \frac{\rho}{\sqrt{1+ (1-\rho^2)\sigma_X^2/\sigma_\epsilon^2}}.$$
Is this calculation correct? What would be a way to explicitly derive the updated correlation coefficient and covariance?
After thinking about the problem a bit more I was able to show that the updated correlation coefficient is indeed equal to the one stated in the question. This unfortunately included lengthy algebraic derivations. The answer below does not always give the detailed calculation steps.
Our aim is to derive the conditional distribution $f(x,y | s)$. The pdf of the bivariate normal is \begin{equation*} f(x,y) = \frac{1}{2\pi\sigma_X\sigma_Y\sqrt{(1-\rho^2)}}\text{exp}\left\{ - \frac{1}{2(1-\rho^2)}\left[ \left(\frac{x - \mu_X}{\sigma_X}\right)^2 - 2\rho\left(\frac{x - \mu_X}{\sigma_X}\right)\left(\frac{y - \mu_Y}{\sigma_Y}\right) + \left(\frac{y - \mu_Y}{\sigma_Y}\right)^2 \right] \right\}. \end{equation*} The conjugate prior is \begin{equation*} f(x,y | s) \propto f(x,y)g(s | x). \end{equation*} Plugging in and simplifying brings \begin{equation}\label{e-conj} f(x,y | s) \propto \text{exp}\left\{ - \frac{1}{2(1-\rho^2)}\left[ \left(\frac{x - \mu_X}{\sigma_X}\right)^2 - 2\rho\left(\frac{x - \mu_X}{\sigma_X}\right)\left(\frac{y - \mu_Y}{\sigma_Y}\right) + \left(\frac{y - \mu_Y}{\sigma_Y}\right)^2 + (1 - \rho^2)\left(\frac{s - x}{\sigma_\epsilon}\right)^2 \right] \right\}. \end{equation} Suppose that the initial conjecture about the updated correlation coefficient is correct, i.e., that \begin{equation*} \begin{split} \rho' &= \rho \frac{1}{\sqrt{1 + (1 - \rho^2)\sigma_X^2 / \sigma_\epsilon^2}}. \end{split} \end{equation*} Note that \begin{equation*} \begin{split} \rho'^2 &= \rho^2 \frac{1}{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2} \\ \Rightarrow 1 - \rho'^2 &= \frac{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2 - \rho^2}{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2} \\ &= \frac{(1 - \rho^2)(1 + \sigma_X^2/\sigma_\epsilon^2)}{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2} \\ \Rightarrow \frac{1}{1 - \rho'^2} &= \frac{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2}{(1 - \rho^2)(1 + \sigma_X^2/\sigma_\epsilon^2)} \\ \Rightarrow \frac{1}{1 - \rho^2} &=\frac{1}{1 - \rho'^2} \frac{1 + \sigma_X^2/\sigma_\epsilon^2}{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2} \\ \Rightarrow \frac{1}{1 - \rho^2} &=\frac{1}{1 - \rho'^2}\frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2} \frac{1}{1 + (1 - \rho^2)\sigma_X^2/\sigma_\epsilon^2} \frac{\rho^2}{\rho^2} \\ \Rightarrow \frac{1}{1 - \rho^2} &=\frac{1}{1 - \rho'^2}\frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\frac{\rho'^2}{\rho^2}. \end{split} \end{equation*} We can plug this into the formula for the conjugate prior: \begin{equation*} f(x,y | s) \propto \text{exp}\left\{ - \frac{1}{2(1-\rho'^2)}\frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\frac{\rho'^2}{\rho^2}\left[ \left(\frac{x - \mu_X}{\sigma_X}\right)^2 - 2\rho\left(\frac{x - \mu_X}{\sigma_X}\right)\left(\frac{y - \mu_Y}{\sigma_Y}\right) + \left(\frac{y - \mu_Y}{\sigma_Y}\right)^2 + (1 - \rho^2)\left(\frac{s - x}{\sigma_\epsilon}\right)^2 \right] \right\}. \end{equation*} Using \begin{equation*} \begin{split} \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\left(\frac{y - \mu_Y}{\sigma_Y}\right)^2 =& \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\left(\frac{y^2 - 2y\mu_Y + \mu_Y^2}{\sigma_Y^2}\right) \\ =& \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\left(\frac{y^2 - 2y\mu_Y + \mu_Y^2 - 2y\mu_Y' + \mu_Y'^2 + 2y\mu_Y' - \mu_Y'^2}{\sigma_Y^2}\right) \\ =& \left(\frac{y - \mu_Y}{\frac{\sigma_\epsilon\sigma_Y}{\sqrt{\sigma_X^2 + \sigma_\epsilon^2}} \frac{\rho}{\rho'}}\right)^2 + \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\frac{\mu_Y^2 - \mu_Y'^2 + 2y\mu_Y' - 2y\mu_Y}{\sigma_Y^2} \\ =& \left(\frac{y - \mu_Y}{\sigma_Y'}\right)^2 + \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\frac{\mu_Y^2 - \mu_Y'^2 + 2y\mu_Y' - 2y\mu_Y}{\sigma_Y^2}, \end{split} \end{equation*} and after similar steps \begin{equation*} \begin{split} \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^22\rho\left(\frac{x - \mu_X}{\sigma_X}\right)\left(\frac{y - \mu_Y}{\sigma_Y}\right) =& 2\rho'\left(\frac{x - \mu_X'}{\sigma_X'}\right)\left(\frac{y - \mu_Y'}{\sigma_Y'}\right) + \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^22\rho \\ &\times\left( \frac{(x - \mu_X')(\mu_Y' - \mu_Y) + (y - \mu_Y')(\mu_X' - \mu_X) + (\mu_X - \mu_X')(\mu_Y' -\mu_Y)}{\sigma_X\sigma_Y} \right) \end{split} \end{equation*} and \begin{equation*} \begin{split} \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\left(\frac{x - \mu_X}{\sigma_X}\right)^2 =& \left( \frac{x - \mu_X'}{\sigma_X'} \right)^2 - \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2} \left(\frac{\rho'}{\rho}\right)^2(1-\rho^2) \left(\frac{x - \mu_X'}{\sigma_\epsilon}\right)^2 \\ &+ \frac{\sigma_X^2 + \sigma_\epsilon^2}{\sigma_\epsilon^2}\left(\frac{\rho'}{\rho}\right)^2\left( \frac{\mu_X^2 - \mu_X'^2 + 2x\mu_X' - 2x\mu_X}{\sigma_X^2} \right) \end{split} \end{equation*} we can write the conjugate prior as \begin{equation*} \begin{split} f(x,y | s) \propto& \text{exp}\left\{ - \frac{1}{2(1-\rho'^2)}\left[ \left(\frac{x - \mu_X'}{\sigma_X'}\right)^2 - 2\rho'\left(\frac{x - \mu_X'}{\sigma_X'}\right)\left(\frac{y - \mu_Y'}{\sigma_Y'}\right) + \left(\frac{y - \mu_Y'}{\sigma_Y'}\right)^2 \right] \right\} \\ &\times\text{exp}\bigg\{ - \frac{1}{2(1-\rho^2)}\bigg[ - (1-\rho^2) \left(\frac{x - \mu_X'}{\sigma_\epsilon}\right)^2 + \frac{\mu_X^2 - \mu_X'^2 + 2x\mu_X' - 2x\mu_X}{\sigma_X^2} \\ & -2\rho \left( \frac{(x - \mu_X')(\mu_Y' - \mu_Y) + (y - \mu_Y')(\mu_X' - \mu_X) + (\mu_X - \mu_X')(\mu_Y' -\mu_Y)}{\sigma_X\sigma_Y} \right) \\ &+ \frac{\mu_Y^2 - \mu_Y'^2 + 2y\mu_Y' - 2y\mu_Y}{\sigma_Y^2} + (1 - \rho^2)\left(\frac{s - x}{\sigma_\epsilon}\right)^2 \bigg] \bigg\}. \end{split} \end{equation*} The term \begin{equation*} \begin{split} &- (1-\rho^2) \left(\frac{x - \mu_X'}{\sigma_\epsilon}\right)^2 + \frac{\mu_X^2 - \mu_X'^2 + 2x\mu_X' - 2x\mu_X}{\sigma_X^2} \\ & -2\rho \left( \frac{(x - \mu_X')(\mu_Y' - \mu_Y) + (y - \mu_Y')(\mu_X' - \mu_X) + (\mu_X - \mu_X')(\mu_Y' -\mu_Y)}{\sigma_X\sigma_Y} \right) \\ &+ \frac{\mu_Y^2 - \mu_Y'^2 + 2y\mu_Y' - 2y\mu_Y}{\sigma_Y^2} + (1 - \rho^2)\left(\frac{s - x}{\sigma_\epsilon}\right)^2 \end{split} \end{equation*} simplifies to a function that is independent of $x$ and $y$. We conclude that \begin{equation*} \begin{split} f(x,y | s) \propto& \text{exp}\left\{ - \frac{1}{2(1-\rho'^2)}\left[ \left(\frac{x - \mu_X'}{\sigma_X'}\right)^2 - 2\rho'\left(\frac{x - \mu_X'}{\sigma_X'}\right)\left(\frac{y - \mu_Y'}{\sigma_Y'}\right) + \left(\frac{y - \mu_Y'}{\sigma_Y'}\right)^2 \right] \right\}. \end{split} \end{equation*} It then follows from the definition of the bivariate normal distribution that $\rho' = \frac{\rho}{\sqrt{1 + (1-\rho^2)\sigma_X^2/\sigma_\epsilon^2}}$.