**I just realized a problem with my 'counterexample', so I no longer claim that the desired inequality does not hold on $\mathrm{SO}(3)$. The proof that it does hold on the quaternions is still OK. I'll point out my error below and will try to see whether either a proof or counterexample can be constructed that avoids this error.** The goal is to prove or disprove the inequality $\|\log(RS)\|\le\|\log(R)+\log(S)\|$ for all $R,S\in\mathrm{SO}(3)$ for which $\log(RS)$, $\log(R)$, and $\log(S)$ are defined. (In what follows, I'm taking the Frobenius norm to be $\|B\|^2 = \tfrac12\,\mathrm{tr}(B^TB)$, but this normalization clearly does not affect the argument.) Notice that the function $B\mapsto \|\log(B)\|$ is actually a continuous function on $\mathrm{SO}(3)$, because of the easily checked identity $$ \cos\bigl(\|\log(B)\|\bigr) = \tfrac12\bigl(\mathrm{tr}(B)-1\bigr) $$ and the fact that $\cos^{-1}:[-1,1]\to[0,\pi]$ is a continuous, strictly decreasing function on $[-1,1]$. So even though $\log(B)$ is not defined when $\mathrm{tr}(B)=-1$, we can extend $\|\log(B)\|$ continuously (though not smoothly) to $\mathrm{SO}(3)$ by setting $\|\log(B)\|=\pi$ when $\mathrm{tr}(B)=-1$. Thus, since the inequality trivially holds if $\|\log(R)+\log(S)\|\ge\pi$, one only needs to consider the cases where $\|\log(R)+\log(S)\|\le\pi$. **In this case**, because $\cos:[0,\pi]\to[-1,1]$ is a strictly decreasing function on $[0,\pi]$, the desired inequality is equivalent to $$ \tfrac12\bigl(\mathrm{tr}(RS)-1\bigr) \ge \cos\bigl(\|\log(R)+\log(S)\|\bigr). $$ In the rest of my (flawed) analysis, I constructed $R$ and $S$ in $\mathrm{SO}(3)$ that violated this latter inequality. **However**, the example that I constructed has $\|\log(R)+\log(S)\|>\pi$, so it is *not* a counterexample to the original inequality. It remains to be seen whether there exist $R$ and $S$ in $\mathrm{SO}(3)$ with $\|\log(R)+\log(S)\|<\pi$ that violate the above inequality. The situation turns out to be better for the unit quaternions (which can also be thought of as $\mathrm{SU}(2)$, but I won't go there.) In this case, we do indeed have $|\log(pq)|\le |\log(p) + \log(q)|$ for unit quaternions $p$ and $q$ different from $-1$, so long as we make the convention that $|\log(-1)| = \pi$, even though $\log(-1)$ cannot be defined continuously. Consider the quaternions, i.e., expressions of the form $q = x_0 + x_1\,i + x_2\,j + x_3\,k$, where the $x_i$ are real numbers and $i$, $j$, and $k$ satisfy the usual relations $i^2=j^2=k^2=-1$ and $ij-k=jk-i=ki-j=ji+k=kj+i=ji+k=0$. The *real part* of $q$ is $x_0$ and the *imaginary part* of $q$ is $x_1\,i + x_2\,j + x_3\,k$. As usual, set $|q| = (x_0^2+x_1^2+x_2^2+x_3^2)^{1/2}$. If $u$ is a unit imaginary quaternion then $u^2=-1$, so that, when $a$ is real, we have $\exp(a\,u) = \cos a + \sin a \,u$. Every unit quaternion $q$ other than $-1$ is of the form $\exp(x)$ for some *unique* purely imaginary quaterion $x$ with $|x|<\pi$. Then setting $x := \log q $ defines $\log$ as a smooth function on the unit quaternions minus the single element $-1$. Note that $|\log q|) = |x| = |a|$, so $\cos\bigl(|\log q|\bigr) = \cos a $, which is the real part of $q$. Suppose that $q = \cos a + \sin a \,u$ while $p=\cos b + \sin b \,v$ where $0\le a,b<\pi$ and $u$ and $v$ are unit quaternions, with $u\cdot v = \cos c$ for some $c$. Note that the real part of $uv$ is $-\cos c$. Thus, we have the product expansion $$ qp = (\cos a + \sin a \,u)(\cos b + \sin b \,v) = (\cos a\cos b-\sin a\sin b\cos c) + X $$ where $X$ is imaginary. Thus $$ \cos\bigl(|\log(qp)|\bigr) = (\cos a\cos b-\sin a\sin b\cos c). $$ Meanwhile $$ |\log q + \log p| = |au+bv| = \sqrt{a^2+2ab\cos c+b^2}. $$ Since $|\log(qp)|\le\pi$, in order to verify the inequality $|\log(qp)|\le |\log q + \log p|$, one only needs to deal with the cases in which $0\le |\log q + \log p|\le \pi$, which may as well be assumed. In this case, since $\cos$ is a strictly decreasing function on the interval $[0,\pi]$, the inequality $|\log(qp)|\le |\log q + \log p|$ is equivalent to $\cos\bigl(|\log(qp)|\bigr)\ge \cos\bigl(|\log q + \log p|\bigr)$, i.e., $$ (\cos a\cos b-\sin a\sin b\cos c) \ge \cos\bigl(\sqrt{a^2+2ab\cos c+b^2}\bigr). $$ Now, it can be shown that this inequality does indeed hold for all $c$ and all $a$ and $b$ with $|a|,|b|<\pi$ (not just when $a^2+2ab\cos c+b^2\le \pi^2$). (In fact, by continuity, it holds for $|a|,|b|\le \pi$ and all $c$. Moreover, equality holds in this range of the variables only when $a=0$, $b=0$ or $\cos c = \pm 1$.) Thus, the desired inequality $|\log(qp)|\le |\log q + \log p|$ follows. (Note that $qp=-1$ would imply that $p=-\bar q$, so $\cos(a)+\cos(b)=0$ and $\sin a\,u=\sin b\,v$. But then $|\sin a|=|\sin b|$. This forces $a+b = \pi$ (since we can assume that $0\le a,b <\pi$) and $u=v$, i.e., $c=0$. Thus, the inequality holds even when $\log (qp)$ does not exist.)