Absolute value based AM envelope detection viewed in the frequency domain

In my understanding when a passband AM signal is demodulated with an envelope detector taking the absolute value restores the original baseband version of the signal and the low-pass filter removes all the (passband) high frequency content.

It is intuitively obvious when represented graphically that after we rectify the signal we get the envelope in the upper part of the graph.

But mathematically in the frequency domain it is not so obvious how taking the absolute value of an AM passband signal would recreate the baseband signal.

How does one derive mathematically that taking the absolute value of an AM pass-band signal would recreate the modulating signal at baseband?

$$\DeclareMathOperator{\sgn}{sgn}$$ The modulating signal in AM is

$$s(t) = C + a(t)\text,$$

where $$a(t)$$ is the (audio) amplitude, and $$C$$ is a constant so that $$s(t) \ge 0 \;\forall t$$. (Otherwise, your audio amplitude would just frequently "switch" the wave's sign, not really modulate the envelope.) That means, $$C > - \min_t(s(t))$$.

Therefore, the passband (around frequency $$f$$) signal is

$$r(t) = s(t) \sin(2\pi f t) = \left(C + a(t)\right) \sin(2\pi f t)\text.$$

As said, $$C+a(t)$$ is never negative; therefore the sign of $$r(t)$$ is

\begin{align} \sgn(r(t)) &=\sgn(s(t) \sin(2\pi f t))\\ &=\sgn(s(t))\sgn(\sin(2\pi ft))\\ &=+1\cdot\sgn(\sin(2\pi ft))\\ &=\sgn(\sin(2\pi ft)) \end{align}

That tells us one way to write the absolute value of $$r(t)$$, because for any $$x$$:

\begin{align} |x| &= x\cdot \sgn(x)\\ \implies\\ |r(t)|&=r(t)\cdot \sgn(r(t))\\ &= r(t)\cdot \underbrace{\sgn(\sin(2\pi ft))}_{:=w(t)} \end{align}

This introduces us to a new function $$w(t)$$, which is always positive one when the carrier wave is, and negative when the carrier is negative. A square wave with the same frequency as the carrier! Thus, knowing that the square wave has a Fourier series representation $$w_f(t)= \frac{4}{\pi} \sum\limits_{k\in\{1,3,5,\ldots\}} \frac{\sin\left(2\pi k ft\right)}k$$

\begin{align} |x| &= r(t)\cdot w(t) \\ &= r(t) \cdot \frac{4}{\pi} \sum\limits_{k\in\{1,3,5,\ldots\}} \frac{\sin\left(2\pi k ft\right)}k\\ &= \frac{4}{\pi} s(t) \sin(2\pi f t) \sum\limits_{k\in\{1,3,5,\ldots\}} \frac{\sin\left(2\pi k ft\right)}k\\ &= \frac4\pi s(t){\left[ \frac11\underbrace{\sin(2\pi f t)\sin(2\pi \,1f\, t)}_ {=\frac12(\cos(2\pi (f-f)t)-\cos(2\pi(f+f)t))} + \frac13\underbrace{\sin(2\pi f t) \sin(2\pi \,3f\, t)}_ {=\frac12(\cos(2\pi (f-3f)t)-\cos(2\pi(f+3f)t))} + \frac15\underbrace{\sin(2\pi f t) \sin(2\pi \,5f\, t)}_ {=\frac12(\cos(2\pi (f-5f)t)-\cos(2\pi(f+5f)t))} + \ldots \right]}\\ &= \frac4\pi s(t)\left[{ {\frac12(1-\cos(2\pi2ft))} +{\frac13\frac12(\cos(2\pi2ft)-\cos(2\pi4ft))} +{\frac15\frac12(\cos(2\pi4ft)-\cos(2\pi6ft))} + \ldots} \right]\\ &=\frac2\pi s(t)\left[{ {1-\cos(2\pi2ft)} +\frac{\cos(2\pi2ft)-\cos(2\pi4ft)}3 +\frac{\cos(2\pi4ft)-\cos(2\pi6ft)}5 + \ldots} \right]\\ &= \frac2\pi s(t) - \frac2\pi s(t)\left[{\frac23\cos(2\pi2ft)+\frac25{\cos(2\pi4ft)}+\frac27{\cos(2\pi6ft)} + \ldots} \right]\\ \end{align}

That looks familiar: the first term in the square bracket, $$\sin(2\pi f t)\sin(2\pi \,1f\, t)$$ is simply mixing the carrier with the carrier, the second is mixing the carrier with a sine thrice its frequency and so on.

Thus, the first term yields, due to $$\sin(a)\sin(b) =\frac12(\cos(a-b)-\cos(a+b))$$, the baseband signal.

The rest of the terms mix up the passband to $$2f$$, $$4f$$, $$6f$$ and so on and are suppressed with a low-pass filter.