L02E05.tex

\documentclass[solutions.tex]{subfiles}

\xtitle

% XXX/TODO: \bm doesn't work with bare mathjax, so we
% tweak things around here. \bm from the bm package seems
% to be the recommended solution for bold math fonts.
% (https://tex.stackexchange.com/a/596)
\renewcommand{\bm}[1]{\pmb{#1}}

% XXX/TODO: similar issue for \qed
% In case we're using \begin{proof}, \qed will be quietly
% called, without math mode, but \Box expects it.
%\renewcommand{\qed}{\,\boxed{\,}}
\renewcommand{\qed}{\,\relax\ifmmode\Box\else$\Box$\fi}

\begin{document}
\maketitle
\begin{remark} This is a WIP; some intermediate results are missing.
\end{remark}
\begin{exercise} Prove each of the formulas in Eq.s $(2)$.
\textit{Hint}: Look up trigonometric identities and limit
properties in a reference book.
\end{exercise}

Let's recall the formulas of Eq.s $(2)$:
\begin{equation*} \begin{aligned}
	\frac{d}{dt}(\sin t) &&=&& \cos t \\
	\frac{d}{dt}(\cos t) &&=&& \sin t \\
	\frac{d}{dt}(e^t) &&=&& e^t \\
	\frac{d}{dt}(\ln t) &&=&& \frac{1}{t}
\end{aligned} \end{equation*}

\begin{remark}
Interestingly, there are multiple ways of \textit{defining}
those functions\footnote{For instance, consider this page
containing $6$ equivalent definitions of the exponential:
\url{https://en.wikipedia.org/wiki/Characterizations\_of\_the\_exponential\_function}}.
As a result, there are different ways to compute the derivatives,
depending on which definitions we choose. \\

As the definitions given in the book for $\sin$, $\cos$ and
the exponential are rather standard, we'll recall them and use
those. The natural logarithm hasn't been clearly defined though,
so we'll have to do it.
\end{remark}

\begin{remark} The book suggests to look up trigonometric
identities and common properties in some reference material, but
we're going to take the time to prove almost all intermediate results
here. \\

As far as I can tell, to compute the derivative of either $\sin$
or $\cos$, starting from a geometrical (triangle-based) definition,
while keeping the definition of $\pi$ as a measure of angle in radians,
one need to start from basic Euclidean geometry, derive
some specific limits, and lightly touch on elementary integration
results. This is a good occasion to refresh basic real analysis. \\

To say it otherwise, we will go \textbf{far beyond} what is expected
for this exercise by the authors. That being said, take what follows with a
grain of salt: there's a lot of results, which can be subtle, so you may
want to refer to a more thorough treatment by \textit{real} mathematicians
in case of doubts.
\end{remark}

Let's start by recalling that a function $\varphi : E \rightarrow \mathbb{R}$
is said to be differentiable at a point $e\in E$ if the following limit exists:
\[
	\varphi'(e) = \frac{d}{dx}\varphi(e) =
		\boxed{\lim_{\epsilon \rightarrow 0}\frac{\varphi(e+\epsilon)-\varphi(e)}{\epsilon}}
\]

\hr
$\pmb{d\sin t/dt}$\,\\
Then, let's remind ourselves of the common definitions of $\cos$ and $\sin$,
in the context of a right triangle:

%\begin{equation*}
\begin{figure}[H]
	\centering
%\vcenter{\hbox{
	\begin{tikzpicture}
		\coordinate (angleat) at (4, 0);
		\draw (0, 0) -- (angleat) node (a) [midway,yshift=-10] {$a$};
		\draw (0, 0) -- (0, 3) node (b) [midway,xshift=-10] {$b$};
		\draw (0, 3) -- (4, 0) node (c) [midway,xshift=10,yshift=2] {$c$};
		\node[draw] at (5, 2) {$\cos \theta \triangleq \frac{c}{a}$};
		\node[draw] at (5, 1) {$\sin \theta \triangleq \frac{b}{c}$};
		% right angle
		\draw [gray] (0,.5)-|(.5,0);
		% \theta angle
		\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = c--angleat--a};
	\end{tikzpicture}
%	}}
\end{figure}
%\quad\quad
%\begin{aligned}
%	\boxed{\cos \theta \triangleq \frac{c}{a}} \\
%	\boxed{\sin \theta \triangleq \frac{b}{c}}
%\end{aligned}
%\end{equation*}

In particular, we can identify points on the unit-circle
by the angle between the $x$ axis and the radius connecting
the center of the circle to such points. Then, each point will
then be located in the $xy$-plane as $(\cos\theta, \sin\theta)$,
where $\theta$ is the angle previously described, associated
to the point.

\begin{figure}[H]
	\centering
	\begin{tikzpicture}
		\tikzmath{
			\xmin = -5;
			\xmax = 5;
			\ymin = -5;
			\ymax = 5;
			\r = 4;
			\rd = 2*\r; % \r * 2cm, where 2cm is the default x length
			\t = 30;
			\px = \r * cos(\t);
			\py = \r * sin(\t);
		}
		\coordinate (O) at (0, 0);
		\coordinate (p) at (\t:\r);

		\draw[color=gray!30, dashed] (\xmin,\ymin) grid (\xmax,\ymax);
		% axes
		\draw[dashed,gray,->] (\xmin,0) -- (\xmax,0) node (xaxis) [gray,right]{$\vec{x}$};
		\draw[dashed,gray,->] (0,\ymin) -- (0,\ymax) node (yaxis) [gray,right]{$\vec{y}$};

		% 8cm = \r * 2cm (which is the default x length)
		\node[draw,circle, minimum size=\rd cm,inner sep=0] (c) at (0,0){};
		\draw[->] (O) -- (p) node (pvec) [midway,yshift=10,xshift=-2]{$r=1$};

		\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = xaxis--O--pvec};
		\draw[dashed,gray] (p) -- (\px,0) node () [yshift=-10]{$\cos(\theta)$};
		\draw[dashed,gray] (p) -- (0,\py) node () [xshift=-20]{$\sin(\theta)$};
	\end{tikzpicture}
\end{figure}
Note that we have:
\begin{theorem}
\[
	(\forall x \in \mathbb{R}),\quad \boxed{\sin^2 x + \cos^2 x = 1}
\]
\end{theorem}
\begin{proof} This follows immediately from the Pythagorean theorem applied
to the right triangle formed by $r=1$, $\cos\theta$ and $\sin\theta$.
\end{proof}

% TODO: visual proof for the Pythagorean theorem

We'll need this later: this is but a variant of the previous
result where the circle isn't restricted to being unitary:

\begin{theorem}[equation of a circle]
The points $(x, y) \in \mathbb{R}^2$ describing a circle
of radius $r$ centered at the origin $O$ are tied by the
following equation
\[
	\boxed{x^2 + y^2 = r^2 }
\]
\end{theorem}
\begin{proof}
This follows directly from Pythagorean's theorem
\end{proof}

\begin{remark}\label{L02E02:rmk:circle-eq}
In particular, as $r$ is a constant, this mean we can express $y$
as a function of $x$:
\[
	\boxed{y(x) = \sqrt{r^2-x^2}}\,;\,x\in[-r, r]
\]
\end{remark}

In order to establish $\sin'$, we will need a few intermediate
results that we're going to prove now. First will be to find a formula
for $\sin(\alpha+\beta)$. Indeed, if you try to apply the definition of the
derivative to $\sin$, you should see a $\sin(x+\epsilon)$: we will need
to have it expressed differently to develop the proof.
\[
	\sin'(x) \triangleq \lim_{\epsilon \rightarrow 0}
		\frac{\sin(x+\epsilon)-\sin x}{\epsilon}
\]

\begin{theorem}[$\sin(\alpha+\beta)$]
\begin{equation}
	(\forall(\alpha, \beta)\in\mathbb{R}^2),\quad
		\boxed{\sin(\alpha+\beta) = \sin\alpha\cos\beta +\cos\alpha\sin\beta}
	\label{L02E05:thm:sinsum}
\end{equation}
\end{theorem}
There's a also a formula for the cosine of a sum of angles, that we will
need later, for the derivative of $\cos$, but that will be rather immediate
to prove along the one regarding the sine of a sum of angles.
\begin{theorem}[$\cos(\alpha+\beta)$]
\begin{equation}
	(\forall(\alpha, \beta)\in\mathbb{R}^2),\quad
		\boxed{\cos(\alpha+\beta) = \cos\alpha\cos\beta +\sin\alpha\sin\beta}
	\label{L02E05:thm:cossum}
\end{equation}
\end{theorem}
\begin{proof} This will be a "visual proof". Besides the aforementioned
definitions of $\sin$ and $\cos$, we will also use the "fact" that sum of
angles in a right triangle is $\pi$, which is actually the \textit{triangle
postulate}, an axiom of Euclidean geometry, equivalent to the
\href{https://en.wikipedia.org/wiki/Parallel\_postulate}{parallel postulate}.
\begin{figure}[H]
	% see https://tex.stackexchange.com/a/383890
	\def\rightangle[size=#1](#2,#3,#4){%
		\draw ($(#3)!#1!(#2)$) --
			($($(#3)!#1!(#2)$)!#1!90:(#2)$) --
			($(#3)!#1!(#4)$);
	}
	\centering
	\begin{tikzpicture}[scale=2]
		\tikzmath{
			\xmin = -0.5;
			\xmax = 4;
			\ymin = -0.5;
			\ymax = 5.5;
			\c = 4;
			\a = 30;
			\b = 40;
			\d = \c/cos(\b);
			\dy = \d*cos(90-\a-\b);
			\dx = \d*sin(90-\a-\b);
			\cx = \c*cos(\a);
			\cy = \c*sin(\a);
		}
		\coordinate (O) at (0, 0);
		\coordinate (pa) at (\a:\c);
		\coordinate (pb) at (\a+\b:\d);
		\coordinate (dy) at (0, \dy);
		\coordinate (dx) at (\dx, 0);
		\coordinate (cx) at (\cx, 0);
		\coordinate (cy) at (0, \cy);
		\coordinate (cxdy) at (\cx, \dy);

		\draw (O)  -- (pa) node [midway,right,xshift=15,yshift=3] {$c$};
		\draw[blue,line width=.5mm] (O) -- (pb) node [black,midway,above,xshift=-5] {$d$};
		\draw (pa) -- (pb) node [midway,above,xshift=3]  {$e$};
		\rightangle[size=10pt](pb,pa,O);

		\draw[dashed,gray] (\xmin,0)      -- (\xmax,0)   node (xaxis) []{};
		\draw[dashed,gray] (0,\ymin)      -- (0,\ymax)   node (yaxis) []{};
		\draw[dashed,gray] (-.5,\dy)        -- (\xmax,\dy) node (dyaxis) []{};
		\draw[dashed,gray] (\dx,\ymin+.5) -- (\dx,\ymax) node (dxaxis) []{};
		\draw[dashed,gray] (\cx,\ymin)    -- (\cx,\ymax) node (cxaxis) []{};
		\draw[dashed,gray] (pa)           -- (\xmax,\cy) node (cyaxis) []{};

		\draw[blue,line width=.5mm] (O) -- (\dx,0);
		\draw[blue,line width=.5mm] (\dx,0) -- (\dx,\dy);

		\draw[gray,<->] (\cx+.5,\cy) -- (\cx+.5,\dy) node (ecosa)
			[midway,right,black]{$e\cos\alpha$};
		\draw[gray,<->] (\cx+.5,0)   -- (\cx+.5,\cy) node (csina)
			[midway,right,black]{$c\sin\alpha$};

		\draw[gray,<->] (\dx,\dy+.5) -- (\cx,\dy+.5) node (esina)
			[midway,above,black]{$e\sin\alpha$};
		\draw[gray,<->] (0,-.5) -- (\cx,-.5) node (ccosa)
			[midway,above,black]{$c\cos\alpha$};

		\draw[gray,<->] (0,\dy+.5) -- (\dx,\dy+.5) node (dcosab)
			[midway,above,black]{$\bm{d\cos(\alpha+\beta)}$};
		\draw[gray,<->] (-.5,0) -- (-.5,\dy) node (dsinab)
			[midway,left,black]{$\bm{d\sin(\alpha+\beta)}$};

		\rightangle[size=10pt](O,dy,dyaxis);
		\rightangle[size=10pt](dxaxis,dx,O);
		\rightangle[size=10pt](cxaxis,cx,O);
		\rightangle[size=10pt](dy,cxdy,cx);

		\pic [draw,"$\alpha$",angle eccentricity=2,gray] {angle = xaxis--O--pa};
		\pic [draw,"$\beta$",angle eccentricity=2,gray] {angle = pa--O--pb};
		\pic [draw,"$\dfrac{\pi}2-\alpha$",angle eccentricity=2.1,gray] {angle = O--pa--cx};
		\pic [draw,"$\alpha$",angle eccentricity=2,gray] {angle = cxdy--pa--pb};
%		\pic [draw,"$\dfrac{\pi}2-\alpha$",angle eccentricity=3,gray] {angle = pa--pb--cxdy};
%		\pic [draw,"$\alpha$",angle eccentricity=2,gray] {angle = dx--pb--pa};
	\end{tikzpicture}
\end{figure}
In the previous picture, considering the right triangle formed by $c$, $d$
and $e$, we have:
\begin{equation*} \begin{aligned}
	c &&=\quad& d\cos\beta; &&\quad& e &&=\quad& d\sin\beta
\end{aligned} \end{equation*}
If we look at the blue/thick triangle right triangle (of hypotenuse
$d$, with an angle of $\beta+\alpha$, and whose other sides are
created by projecting the point formed by $d$ and $e$ down to the
bottom), we find a new relation, to which we can inject our previous
results for $c$ and $e$:
\begin{equation*} \begin{aligned}
	~ && d\sin(\alpha+\beta) &&=\quad& c\sin\alpha+e\cos\alpha \\
	\Leftrightarrow && ~ &&=\quad& (d\cos\beta)\sin\alpha+(d\sin\beta)\cos\alpha \\
	\Leftrightarrow && \sin(\alpha+\beta) &&=\quad& \boxed{\cos\beta\sin\alpha+\sin\beta\cos\alpha}
\end{aligned} \end{equation*}\\
In the same blue/thick triangle, we can also establish a relation
for $\cos(\alpha+\beta)$, using the same definition of $c$ and $e$
as before to conclude:
\begin{equation*} \begin{aligned}
	~ && d\cos(\alpha+\beta) &&=\quad& c\cos\alpha-e\sin\alpha \\
	\Leftrightarrow && ~ &&=\quad& (d\cos\beta)\cos\alpha-(d\sin\beta)\sin\alpha \\
	\Leftrightarrow && \cos(\alpha+\beta) &&=\quad& \boxed{\cos\beta\cos\alpha-\sin\beta\sin\alpha}
\end{aligned} \end{equation*}

\end{proof}

Here's an immediate consequence that we'll need in the future.
\begin{theorem}[trigonometric shifts]
Let $x\in\mathbb{R}$.

\[
	\boxed{\sin(x+\frac\pi2) = \cos x;\qquad
	\cos(x+\frac\pi2) = -\sin x}
	\label{L02E05:thm:trig-shift}
\]

\end{theorem}
\begin{proof}
If we apply our previous formulas \eqref{L02E05:thm:sinsum} and
\eqref{L02E05:thm:cossum} regarding respectively the sine and
cosine of a sum of two angles, in the case where one angle is
$\pi/2$, we have:
\begin{equation*} \begin{aligned}
	(\forall x\in\mathbb{R}),\quad \sin(x+\frac{\pi}2) &&=\quad&
		\sin x\underbrace{\cos\frac{\pi}{2}}_{=0}
		+\cos x\underbrace{\sin \frac{\pi}{2}}_{=1} \\
	~ &&=\quad& \boxed{\cos x} \\
	(\forall x\in\mathbb{R}),\quad \cos(x+\frac{\pi}2) &&=\quad&
		\cos x\underbrace{\cos\frac{\pi}{2}}_{=0}
		-\sin x\underbrace{\sin \frac{\pi}{2}}_{=1} \\
	~ &&=\quad& \boxed{-\sin x}
\end{aligned} \end{equation*}
\end{proof}
\begin{remark} We could derive more similar formulas, but
those are the only ones we'll need.
\end{remark}

\hrr

Now if you try to write down $\sin'$ as previously suggested,
and if you decompose $\cos(x+\epsilon)$ with the formula
(\ref{L02E05:thm:sinsum}), you see that yields two limits:
\begin{equation*} \begin{aligned}
	\sin'(x) &\triangleq&& \lim_{\epsilon \rightarrow 0}
		\frac{\sin(x+\epsilon)-\sin x}{\epsilon} \\
	~ &=&& \lim_{\epsilon \rightarrow 0}
		\frac{\sin x\cos\epsilon+\cos x\sin\epsilon-\sin x}{\epsilon} \\
	~ &=&& \lim_{\epsilon \rightarrow 0}\left(
		\frac{\sin x\cos\epsilon-1}{\epsilon}+\frac{\cos x\sin\epsilon}{\epsilon}
		\right) \\
\end{aligned} \end{equation*}

As we've already explained in
\href{https://github.com/mbivert/ttm/blob/master/cm/L02E04.pdf}{L02E04},
we can recursively split the previous limits, assuming each individual
limit exists. Let's digress and review how to prove such results
on limits. Starting with the definition of a limit:

\hrr

\begin{definition}[$(\epsilon,\delta)$-definition of a limit]
Let $\varphi : \mathbb{R} \rightarrow \mathbb{R}$.
Saying that $\lim_{x\rightarrow a}\varphi(x) = L$ is the same as saying:
\[ \epsdelta{\epsilon}{\delta}{a}{x}{\varphi(x)}{L}     \]

The definition is dense, so let's unpack it. Let's fix $\epsilon$ to
some value close to zero, say $0.1$, or $0.0001$. \\

Now the idea is that, for this $\epsilon$, we will always be able to
find a distance $\delta$ such that if we pick an $x$ between
$a-\delta$ and $a+\delta$ (i.e. $\abs{x-a} < \delta$), then $\varphi(x)$
will be between $L-\epsilon$ and $L+\epsilon$
(i.e. $\abs{\varphi(x)-L} < \epsilon$). \\

\begin{figure}[H]
	\centering
	\begin{tikzpicture}[scale=3.3]
		\tikzmath{
			\xmin = 0;
			\xmax = 2;
			\ymin = -1;
			\ymax = 2;
			\xa   = 1.5;
			\ya   = 0;
			\xfa  = 0;
			\yfa  = sin(\xa r) * sin(\xa r) - cos(\xa r);
			\e    = 0.25;
			\xape = \xa + \e;
			\xame = \xa - \e;
			\yfape = sin(\xape r) * sin(\xape r) - cos(\xape r);
			\yfame = sin(\xame r) * sin(\xame r) - cos(\xame r);
		}
		\draw[->] (\xmin-.5, 0) -- (\xmax+.5, 0) node[right] {$x$};
		\draw[->] (0, \ymin-.5) -- (0, \ymax-.5) node[above] {$\varphi(x)=\sin^2x - \cos x$};
		\draw[color=gray!30, dashed]
			(\xmin-.5,\ymin-.5) grid (\xmax+.5,\ymax-.5);
		\draw[scale=1, domain=\xmin:\xmax, smooth, samples=100, variable=\t, blue]
			plot ({\t}, {sin(\t r)^2 - cos(\t r)});

		\draw[dashed] (\xa, \yfa) -- (\xa, \ya)   node[below] {$a$};
		\draw[dashed] (\xa, \yfa) -- (\xfa, \yfa) node[left]  {$L=\varphi(a)$};

		\draw[dashed, color=black!60]
			(\xape, \yfape)  -- (\xape, \ya)    node[below] {$a+\delta$};
		\draw[dashed, color=black!60]
			(\xape, \yfape)  -- (\xfa,  \yfape) node[left]  {$\varphi(a+\delta)$};

		\draw[dashed, color=black!60]
			(\xame, \yfame)  -- (\xame, \ya)    node[below] {$a-\delta$};
		\draw[dashed, color=black!60]
			(\xame, \yfame)  -- (\xfa,  \yfame) node[left]  {$\varphi(a-\delta)$};
	\end{tikzpicture}
\end{figure}

But, this is true for all strictly positive $\epsilon$. So in particular,
this is true for an ever so smaller $\epsilon$. In other words, regardless
of how close we want $\varphi(x)$ and $L$ to be, we will always be
able to achieve it if we bring $x$ and $a$ close enough.

\end{definition}

Alright, there's just one more thing we need before proving
the sum rule, and that's the
\href{https://en.wikipedia.org/wiki/Triangle\_inequality}
{triangle inequality}. This inequality is rooted in euclidean geometry:
it states that the sum of the length of any two sides of a triangle is greater
or equal than the length of the remaining side.

\begin{theorem}[triangle inequality]
\begin{equation*} \begin{aligned}
	\boxed{(\forall (x,y)\in\mathbb{R}^2),\quad \abs{x+y}\le \abs{x}+\abs{y}}
\end{aligned} \end{equation*}
\end{theorem}

\begin{figure}[H]
	\centering
	\begin{tikzpicture}
		\tikzmath{
			\ax = 0;
			\ay = 0;
			\bx = 3;
			\by = 2;
			\cx = -2;
			\cy = 5;
		}
		\draw[] (\ax, \ay) -- (\bx, \by) node[midway,right,xshift=6]
			{$\abs{x}$};
		\draw[] (\bx, \by) -- (\cx, \cy) node[midway,above,xshift=9,yshift=9]
			{$\abs{z} < \abs{x}+\abs{y}$};
		\draw[] (\cx, \cy) -- (\ax, \ay) node[midway,left]
			{$\abs{y}$};
	\end{tikzpicture}
	\caption{Unless the triangle is degenerate (i.e. all its
	edges are colinear), the length of the longest side of a triangle is
	strictly smaller than the length of the two other sides. It's trivially
	true for the shorter sides. If we allow triangles to be degenerates,
	then it's true for any sides of any triangle.}
\end{figure}
\begin{proof} Let's start by recalling the definition of the absolute
value:
\begin{equation*} \begin{aligned}
	\boxed{x\in\mathbb{R};\quad \abs{x} =
		\begin{cases}
			\hfill x & \text{if $x \ge 0$} \\
			-x & \text{otherwise}
		\end{cases}}
\end{aligned} \end{equation*}
It follows that:
\begin{equation*} \begin{aligned}
	\abs{x+y} =
		\begin{cases}
			\hfill x+y & \text{if $(x+y) \ge 0$} \\
			-(x+y)=-x-y & \text{otherwise}
		\end{cases}
\end{aligned} \end{equation*}
And that, for any $(x, y)\in\mathbb{R}^2$
\begin{equation*} \begin{aligned}
	x <= \abs{x};\quad -x \leq \abs{x};\quad
		y <= \abs{y};\quad -y \leq \abs{y};
\end{aligned} \end{equation*}
So:
\begin{equation*} \begin{aligned}
	\biggl(x+y \le \abs{x}+\abs{y};\quad
	-(x+y) = -x-y \le \abs{x}+\abs{y}\biggr)
	\Leftrightarrow\boxed{\abs{x+y}\le\abs{x}+\abs{y}}
\end{aligned} \end{equation*}
\end{proof}

Let's jump into the sum rule:
\begin{theorem}[sum rule for limits] Assuming the two following limits
exists:
\begin{equation*} \begin{aligned}
	\lim_{x \rightarrow a}\varphi(x);\qquad\lim_{x \rightarrow a}\psi(x)
\end{aligned} \end{equation*}
Then:
\begin{equation*} \begin{aligned}
	\boxed{\lim_{x \rightarrow a}\left(\varphi(x)+\psi(x)\right) =
		\lim_{x \rightarrow a}\varphi(x)
		+ \lim_{x \rightarrow a}\psi(x)}
\end{aligned} \end{equation*}
\end{theorem}
\begin{proof} Most limits proofs are presented in a "confusing"
way, starting with unexplained values that ends up doing exactly
what we want. That happens when mathematicians have thought and
drafted the proof in reverse order, but present it in the
"right" order. We're going to use the "wrong" order here, for
clarity; it should be immediate to check that there's no logical
issues anyway. Just bear in mind that "reversed implications" are
rather unorthodox. \\

Let's start by defining a few things:
\begin{equation*} \begin{aligned}
	\lim_{x \rightarrow a}\varphi(x) = L_1;\qquad\lim_{x \rightarrow a}\psi(x) = L_2 \\
\end{aligned} \end{equation*}
\[	\lim_{x \rightarrow a}\left(\varphi(x)+\psi(x)\right) = L \]

Let's explicit the two first limits via the $(\epsilon-\delta)$-definition:
\[ \epsdelta{\epsilon_1}{\delta_1}{a}{x}{\varphi(x)}{L_1}  \]
\[ \epsdelta{\epsilon_2}{\delta_2}{a}{x}{\psi(x)}{L_2}     \]

Essentially, what we want to prove is then $L = L_1 + L_2$. If this
is true, this means means that for an $\epsilon\in\mathbb{R}$, we
should be able to find a $\delta$ such that:
\begin{equation*} \begin{aligned}
	~ && \abs{\varphi(x)+\psi(x)-L} &&<& \epsilon \\
	\Leftrightarrow && \abs{\varphi(x)+\psi(x)-(L_1+L_2)} &&<\,& \epsilon
		\qquad\qquad\text{(assumption)} \\
	\Leftrightarrow && \abs{(\varphi(x)-L_1)+(\psi(x)-L_2)} &&<\,& \epsilon \\
	\Leftarrow && \abs{\varphi(x)-L_1}+\abs{\psi(x)-L_2} &&<\,& \epsilon
		\qquad\text{(triangular inequality)} \\
	\Leftrightarrow && \abs{\varphi(x)-L_1}+\abs{\psi(x)-L_2} &&<\,& \epsilon_1+\epsilon_2
		\qquad(\epsilon = \epsilon_1+\epsilon_2)
\end{aligned} \end{equation*}
\[
	\Leftarrow \begin{cases}
		\abs{\varphi(x)-L_1} < \epsilon_1 = \epsilon/2 \\
		\abs{\psi(x)-L_2} < \epsilon_2 = \epsilon/2
	\end{cases}\qquad\text{(all numbers are positive)}
\]
\[
	\Leftarrow\Bigl(\abs{x-a}<\delta=\min(\delta_1,\delta_2)\Bigr)
\]

To make things very clear, if we choose such a $\delta$, then:
\[
	\abs{x-a}<\delta \Leftrightarrow \begin{cases}
		\abs{x-a} < \delta_1 \\
		\abs{x-a} < \delta_2
	\end{cases}
\]
Which means both limits will hold. Furthermore, given any real
number, say $\epsilon_1$, we can always choose to represent it as
$\epsilon/2$, for $\epsilon\in\mathbb{R}$ too. \\

% https://en.wikipedia.org/wiki/Archimedean_property ?

And this concludes the proof: if you look at the beginning and end of
the previous derivation, we've found:

\[ \epsdelta{\epsilon}{\delta}{a}{x}{\varphi(x)+\psi(x)}{\underbrace{L_1+L_2}_L} \]
Which by definition means:
\[
	\lim_{x\rightarrow a}\left(\varphi(x)+\psi(x)\right) = L_1+L_2
\]
\end{proof}

The following is not necessary here, but it's more involved, so good
practice:
\begin{theorem}[product rule for limits] Assuming the two following limits
exists:
\begin{equation*} \begin{aligned}
	\lim_{x \rightarrow a}\varphi(x);\qquad\lim_{x \rightarrow a}\psi(x)
\end{aligned} \end{equation*}
Then:
\begin{equation*} \begin{aligned}
	\boxed{\lim_{x \rightarrow a}\left(\varphi(x)\psi(x)\right) =
		\lim_{x \rightarrow a}\varphi(x)\lim_{x \rightarrow a}\psi(x)}
\end{aligned} \end{equation*}
\end{theorem}
\begin{proof} We'll use the same unorthodox presentation; again,
let's start by defining a few things:
\begin{equation*} \begin{aligned}
	\lim_{x \rightarrow a}\varphi(x) = L_1;\qquad\lim_{x \rightarrow a}\psi(x) = L_2 \\
\end{aligned} \end{equation*}
\[	\lim_{x \rightarrow a}\left(\varphi(x)\psi(x)\right) = L \]

What we want to prove this time is that $L = L_1L_2$. If this
is true, this means means that for an $\epsilon\in\mathbb{R}$, we
should be able to find a $\delta$ such that:
\begin{equation*} \begin{aligned}
	~ && \abs{\varphi(x)\psi(x)-L} &&<& \epsilon \\
	\Leftrightarrow && \abs{\varphi(x)\psi(x)-L_1L_2} &&<\,& \epsilon
\end{aligned} \end{equation*}

Well, this is embarrassing: we can't really follow through as we did
before. Can we find an expression that we could algebraically connect
to $\varphi(x)\psi(x)-L_1L_2$? \\

Let's make a guess, and try the following product $(\varphi(x)-L_1)(\psi(x)-L_2)$.
When developed, clearly it contains the previous expression that
we desperately try to find a path to, plus two other terms:
\[
	\varphi(x)\psi(x)-L_1\psi(x)-L_2\varphi(x)+L_1L_2
\]

And we can see that in the context of $x$ being arbitrarily close
to $a$, we have, by the sum rule:
\begin{equation*} \begin{aligned}
	L_1\psi(x) \rightarrow L_1L_2;\qquad L_2\varphi(x) \rightarrow L_2L_1
\end{aligned} \end{equation*}

Which means, when $x\rightarrow a$, this product should be equal to
$\varphi(x)\psi(x)-L_1L_2$. In summary, if we can prove that
$(\varphi(x)-L_1)(\psi(x)-L_2)$ can be made as small as we want as
$x\rightarrow a$, we should have a proof. Let's, then study the
corresponding limit (that we expect to be zero):

\begin{equation*} \begin{aligned}
	\lim_{x\rightarrow a}(\varphi(x)-L_1)(\psi(x)-L_2)
\end{aligned} \end{equation*}

First, note that we have:
\begin{equation*} \begin{aligned}
	\lim_{x\rightarrow a}(\varphi(x)-L_1) &&=\quad&
		(\lim_{x\rightarrow a}\varphi(x))-L_1 &&=\quad& 0 \\
	\lim_{x\rightarrow a}(\psi(x)-L_2) &&=\quad&
		(\lim_{x\rightarrow a}\psi(x))-L_2 &&=\quad& 0 \\
\end{aligned} \end{equation*}

Which means, translated in the $(\epsilon-\delta)$ formalism (as
before, we choose the same $\epsilon$ so as to control both limits
at once)

\[ \epsdelta{\epsilon}{\delta_1}{a}{x}{\varphi(x)-L_1}{0}  \]
\[ \epsdelta{\epsilon}{\delta_2}{a}{x}{\psi(x)-L_2}{0}     \]

Let $\epsilon > 0$; let's choose $\delta=\min(\delta_1,\delta_2)$.
Then

\begin{equation*} \begin{aligned}
	\abs{x-a}<\delta \Leftrightarrow \begin{cases}
		\abs{x-a} < \delta_1 \\
		\abs{x-a} < \delta_2
	\end{cases}
\end{aligned} \end{equation*}

Which means we have both:

\begin{equation*} \begin{aligned}
	\begin{cases}
		\abs{\varphi(x)-L_1} < \epsilon \\
		\abs{\psi(x)-L_2} < \epsilon
	\end{cases}
\end{aligned} \end{equation*}

All involved numbers are positive, so let's multiply both lines:

\begin{equation*} \begin{aligned}
	~ & \abs{\varphi(x)-L_1}\times\abs{\psi(x)-L_2} < \epsilon^2 \\
	\Leftrightarrow & \abs{(\varphi(x)-L_1)(\psi(x)-L_2)} < \epsilon^2
\end{aligned} \end{equation*}

But if $\epsilon$ can be chosen arbitrarily in $\mathbb{R}^*_+$, then
so can $\epsilon'=\epsilon^2$. So we've just proved that

\[ \epsdelta{\epsilon'}{\delta}{a}{x}{(\varphi(x)-L_1)(\psi(x)-L_2)}{0}  \]

That is:
\begin{equation*} \begin{aligned}
	\lim_{x\rightarrow a}(\varphi(x)-L_1)(\psi(x)-L_2) = 0
\end{aligned} \end{equation*}

From what we've already said, this concludes the proof, but let's
make it clear:
\begin{equation*} \begin{aligned}
	~ && \varphi(x)\psi(x)-L_1\psi(x)-L_2\varphi(x)+L_1L_2 &&=\quad&
		(\varphi(x)-L_1)(\psi(x)-L_2) \\
	\Leftrightarrow &&
		\lim_{x\rightarrow a}\Bigl(\varphi(x)\psi(x)-L_1\psi(x)-L_2\varphi(x)+L_1L_2\Bigr) &&=\quad&
		\underbrace{\lim_{x\rightarrow a}(\varphi(x)-L_1)(\psi(x)-L_2)}_0 \\
	\Leftrightarrow &&
		\lim_{x\rightarrow a}(\varphi(x)\psi(x))
		-L_1\underbrace{\lim_{x\rightarrow a}(\psi(x))}_{L_2}
		-L_2\underbrace{\lim_{x\rightarrow a}(\varphi(x))}_{L_1}
		+\lim_{x\rightarrow a}(L_1L_2) &&=\quad& 0 \\
	\Leftrightarrow &&
		\lim_{x\rightarrow a}(\varphi(x)\psi(x)) &&=\quad& \boxed{L_1L_2}
\end{aligned} \end{equation*}
\end{proof}
\begin{remark} As the proof is rather elementary, we've assumed that for a
constant $k\in\mathbb{R}$,
\[
	\lim_{x\rightarrow a}(k\varphi(x))=k\lim_{x\rightarrow a}(\varphi(x))
\]

We've also assumed that the product of two absolute values is the
absolute values of the product. Again, the proof is elementary.
\end{remark}
% TODO: add proofs nevertheless, for completeness?
\hrr

So, what we did was applying the definition of the derivative
on $x\mapsto\sin x$; this yields the limit of a sum. We know we can
split it into sums of limits, provided the two individual limits exist.
So we must now try to compute those two limits. \\

We'll first need to define what a \textit{circular sector} is,
and how to express its \textit{area}, from which, you'll see, computing
the area of a circle is but a special case. We will also need to establish
another important result on limits: the \textit{squeeze theorem}.

\hrr

Let's start with circular sector:
\begin{definition}[circular arc, circular sector]
A \underline{circular arc} is a  portion of the circle between two points
of that circle. A \underline{circular sector} is a portion of disk enclosed
between two (usually distinct) radii\footnote{"radii" is the plural of "radius"}
and a circular arc.

\begin{figure}[H]
	\centering
	\begin{tikzpicture}
		\tikzmath{
			\xmin = -5;
			\xmax = 5;
			\ymin = -5;
			\ymax = 5;
			\ra = 4;
			\rad = 2*\ra; % \r * 2cm, where 2cm is the default x length
			\ta = 60;
			\rb = \ra;
			\rbd = \rad;
			\tb = 20;
		}
		\coordinate (O) at (0, 0);
		\coordinate (pa) at (\ta:\ra);
		\coordinate (pb) at (\tb:\rb);

		% https://ctan.crest.fr/tex-archive/graphics/pgf/base/doc/pgfmanual.pdf
		% §15.9 - Clipping and Fading (Soft Clipping) (p186)
		\begin{scope}[fill=blue!8]
			\fill[clip]
				 (pb) arc[start angle=\tb, end angle=\ta, radius=\ra]
				 -- (O) -- (pb);
		\end{scope}

		% https://ctan.crest.fr/tex-archive/graphics/pgf/base/doc/pgfmanual.pdf
		% §14.7 - The Arch Operation (p159)
		% arc pa,pb
		\draw[blue,thick] (pb) arc[start angle=\tb, end angle=\ta, radius=\ra];

		\draw[color=gray!30, dashed] (\xmin,\ymin) grid (\xmax,\ymax);
		% axes
		\draw[dashed,gray,->] (\xmin,0) -- (\xmax,0) node (xaxis) [gray,right]{$\vec{x}$};
		\draw[dashed,gray,->] (0,\ymin) -- (0,\ymax) node (yaxis) [gray,right]{$\vec{y}$};

		% 8cm = \ra * 2cm (which is the default x length)
		\node[draw,circle, minimum size=\rad cm,inner sep=0,black!30] (c) at (0,0){};
		\draw[] (O) -- (pa) node (pavec) [midway,yshift=10,xshift=-2]{$r$};
		\draw[] (O) -- (pb) node (pbvec) [midway,below,xshift=2]{};

		\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = pbvec--O--pavec};
	\end{tikzpicture}
\end{figure}
\end{definition}
\begin{remark} A circle then, is but a circular sector of angle $2\pi$.
\end{remark}

Unfortunately, if we want to compute the area of a circular sector,
we either need some integral calculus to compute it directly, or indirectly,
via the area of a circle. In addition to the definition of an integral,
to compute the actual integral representing the area of a circle (or
that of a sector), we will need the u-substitution rule, which demands
the fundamental theorem of calculus. \\

A rigorous, extensive treatment of Riemann integration would require
more work than what we aim to achieve here; you may want to refer to
a full real analysis course for more.

% https://home.iitk.ac.in/~psraj/mth101/lecture_notes/lecture15-16.pdf

% https://www.nagwa.com/en/explainers/279131484389/
% https://tutorial.math.lamar.edu/classes/calci/defnofdefiniteintegral.aspx
% https://www.youtube.com/watch?v=qy9ec8Q1Lss&list=PL22w63XsKjqxqaF-Q7MSyeSG1W1_xaQoS&index=53

\begin{definition}[(Riemann) integral]
TODO
\end{definition}

\begin{theorem}[Fundamental theorem of calculus]
TODO
\end{theorem}
\begin{proof}
TODO
\end{proof}

% https://en.wikipedia.org/wiki/Fundamental_theorem_of_calculus#Formal_statements
% https://en.wikipedia.org/wiki/Riemann_integral

% linearity of integration
% -\int_b^a = \int_a^b
% \pi as a radian measure equivalent to 180°

\begin{theorem}[u-substitution/reversed chain-rule (single variable)]
Let $U \subseteq \mathbb{R}$, $(a, b)\in\mathbb{R}^2$. Let
$\varphi : U \rightarrow \mathbb{R}$ and $\nu : [a, b] \rightarrow U$
be respectively $C^0$ and $C^1$ functions. Then,
\[
	\boxed{\int_a^b\varphi(\nu(x))\nu'(x)\,dx = \int_{\nu(a)}^{\nu(b)}\varphi(u)\,du}
\]
\end{theorem}
\begin{proof}
Let's assume here that continuous functions are integrable. Then,
the existence of both integrals is guaranteed by
the restrictions imposed on $\varphi$ and $\nu$. \\

Then, let us note $\Phi$ the anti-derivative of $\varphi$, i.e.
$\Phi' = \varphi$, which by the same assumption as before must exists,
since $\varphi$ is continuous. Let us then apply the chain-rule to
$\Phi \circ \nu$:
\[
	(\Phi \circ \nu)'(x) = \nu'(x)\Phi'(\nu(x)) = \varphi(\nu(x))\nu'(x)
\]
Finally, by integrating both sides and repeatedly applying the fundamental
theorem of calculus twice, we obtain:
\begin{equation*} \begin{aligned}
	\int_a^b\varphi(\nu(x))\nu'(x)\,dx =& \int_a^b(\Phi \circ \nu)'(x)dx \\
	~ =& (\Phi \circ \nu)(b)-(\Phi \circ \nu)(a) \\
	~ =& \Phi(\nu(b)) - \Phi(\nu(a)) \\
	~ =& \int_{\nu(a)}^{\nu(b)}\varphi(u)\,du
\end{aligned} \end{equation*}
\end{proof}

\begin{theorem}[circle area] The area of a circle of radius $r$ is given by:
\[ \boxed{\pi r^2} \]
\end{theorem}
\begin{proof}
The problem of the area of a circle can be reduced via
symmetry to the integration of a positive curve on an interval.
More precisely, let's consider a circle centered at the origin
of radius $r$. To compute its area, suffice to compute the area of
a quadrant of it, say the first quadrant (the blueish one; starting
from this one, the four quadrant are enumerated following an
anti-clockwise/trigonometric direction)

\begin{figure}[H]
	\centering
	\begin{tikzpicture}
		\tikzmath{
			\xmin = -5;
			\xmax = 5;
			\ymin = -5;
			\ymax = 5;
			\ra = 4;
			\rad = 2*\ra; % \r * 2cm, where 2cm is the default x length
			\ta = 90;
			\rb = \ra;
			\rbd = \rad;
			\tb = 0;
		}
		\coordinate (O) at (0, 0);
		\coordinate (pa) at (\ta:\ra);
		\coordinate (pb) at (\tb:\rb);

		% https://ctan.crest.fr/tex-archive/graphics/pgf/base/doc/pgfmanual.pdf
		% §15.9 - Clipping and Fading (Soft Clipping) (p186)
		\begin{scope}[fill=blue!8]
			\fill[clip]
				 (pb) arc[start angle=\tb, end angle=\ta, radius=\ra]
				 -- (O) -- (pb);
		\end{scope}

		% https://ctan.crest.fr/tex-archive/graphics/pgf/base/doc/pgfmanual.pdf
		% §14.7 - The Arch Operation (p159)
		% arc pa,pb
		\draw[blue,thick] (pb) arc[start angle=\tb, end angle=\ta, radius=\ra];

		\draw[color=gray!30, dashed] (\xmin,\ymin) grid (\xmax,\ymax);
		% axes
		\draw[dashed,gray,->] (\xmin,0) -- (\xmax,0) node (xaxis) [gray,right]{$\vec{x}$};
		\draw[dashed,gray,->] (0,\ymin) -- (0,\ymax) node (yaxis) [gray,right]{$\vec{y}$};

		% 8cm = \ra * 2cm (which is the default x length)
		\node[draw,circle, minimum size=\rad cm,inner sep=0,black!30] (c) at (0,0){};
		\draw[] (O) -- (pa) node (pavec) [midway,yshift=10,xshift=-2]{$r$};
		\draw[] (O) -- (pb) node (pbvec) [midway,below,xshift=2]{};
	\end{tikzpicture}
\end{figure}

By symmetry, the area of a circle $A_S$ is four times that of
any quadrant $A_{Q_i}$. Furthermore, the first quadrant's area $A_{Q_1}$
is given by the area under the curve describing a circle
that we saw earlier in \ref{L02E02:rmk:circle-eq}, restricted
to $[0, r]$. More precisely:
\[
	A_S = 4 A_{Q_i} = 4 A_{Q_1} = 4\int_0^r\sqrt{r^2 - x^2}\,dx
\]

This integral can be considered in the form:
\[ \int_{\nu(\theta_0)}^{\nu(\theta_1)}\varphi(x)\,dx \]

Let's perform a first change of variable by setting:
\[ \nu(\theta) = r\sin\theta;\qquad \nu'(\theta) = r\cos\theta \]

It follows that:
\[
	\nu(\theta_0) = 0 \Rightarrow \theta_0 = 0;\qquad
	\nu(\theta_1) = 0 \Rightarrow \theta_1 = \frac\pi2
\]

The integral can now be rewritten:
\begin{equation*} \begin{aligned}
	A_S &\quad=&& 4\int_0^{\pi/2}\phi(\nu(\theta))\nu'(\theta)\,d\theta \\
	~ &\quad=&& 4\int_0^{\pi/2}\sqrt{r^2-(r\sin\theta)^2}r\cos\theta\,d\theta \\
	~ &\quad=&& 4r^2\int_0^{\pi/2}\sqrt{1-\sin^2\theta}\cos\theta\,d\theta\qquad (r > 0) \\
	~ &\quad=&& 4r^2\int_0^{\pi/2}\cos^2\theta\,d\theta\qquad
		(\cos\theta > 0,\,\text{Pythagorean theorem})
\end{aligned} \end{equation*}

However, with (\ref{L02E05:thm:trig-shift}) we have:
\[
	4r^2\int_0^{\pi/2}\cos^2\theta\,d\theta\qquad=\qquad
	4r^2\int_0^{\pi/2}(\sin(\theta+\frac\pi2))^2\,d\theta
\]

We can perform a second change of variable on the rightmost
integral:

\[ \mu(u) = \frac\pi2-u;\qquad \mu'(u) = -1 \]

Then:

\[
	\mu(u_0) = 0 \Rightarrow u_0 = \frac\pi2;\qquad
	\mu(u_1) = \frac\pi2 \Rightarrow u_1 = 0
\]

The integral becomes:
\[
	4r^2\int_0^{\pi/2}(\sin(\theta+\frac\pi2))^2\,d\theta
	\quad=\quad -4r^2\int_{\pi/2}^0\sin(u)^2\,du
	\quad=\quad 4r^2\int_0^{\pi/2}\sin^2\theta\,d\theta
\]

Referring back to our previous integral equality, this means
we have:
\[
	S_A\qquad=\qquad 4r^2\int_0^{\pi/2}\cos^2\theta\,d\theta\qquad=\qquad
	4r^2\int_0^{\pi/2}\sin^2\theta\,d\theta
\]

However, by linearity of integration, and by the Pythagorean theorem,
again, we have
\[
	\int_0^{\pi/2}\cos^2\theta\,d\theta
	+
	\int_0^{\pi/2}\sin^2\theta\,d\theta
	=\int_0^{\pi/2}\underbrace{\cos^2\theta+\sin^2\theta}_{=1}\,d\theta
	=\int_0^{\pi/2}\,d\theta=\frac\pi2
	=2\int_0^{\pi/2}\cos^2\theta\,d\theta
\]

Hence,
\[
	S_A = 2r^2 \underbrace{2\int_0^{\pi/2}\cos^2\theta\,d\theta)}_{=\pi/2} =
	\boxed{\pi r^2}
\]

\end{proof}

\begin{theorem}[circular sector area] The area of a circular
sector, of angle $\theta$, in a circle of radius $r$ is given
by:
\[ \boxed{\frac12r^2\theta} \]
\end{theorem}
\begin{proof} Because the area is evenly distributed on a circle,
this is a simple cross-multiplication\footnote{
\url{https://en.wikipedia.org/wiki/Cross-multiplication}} involving
the area of a circle:
\begin{equation*} \begin{aligned}
	2\pi &&\rightarrow\quad& \pi r^2 \\
	\theta &&\rightarrow\quad& A_\theta= \frac{\theta\pi r^2}{2\pi}
		= \boxed{\frac12r^2\theta}
\end{aligned} \end{equation*}
\end{proof}
\begin{remark} We could also have proved it directly with an integral,
as we did for the circle.
\end{remark}

\begin{theorem}[squeeze theorem] Let $\varphi$, $\psi$, $\phi$ be three
real-valued functions defined on an interval $I\subset\mathbb{R}$, and
$a$ be a point of $I$. If, $(\forall x \in I/\{a\})$ ($x\in I$ but $x\neq a$),
we have:
\[
	\varphi(x) \le \psi(x) \le \phi(x)
\]
With:
\[
	\lim_{x\rightarrow a} \varphi(x) = \lambda = \lim_{x\rightarrow a}\phi(x)
\]
Then:
\[
	\boxed{\lim_{x\rightarrow a}\psi(x) = \lambda}
\]
\end{theorem}
\begin{proof}
Let's translate our limits into their $(\epsilon-\delta)$ form,
considering a single $\epsilon$
\[ \epsdelta{\epsilon}{\delta_1}{a}{x}{\varphi(x)}{\lambda}  \]
\[ \epsdelta{\epsilon}{\delta_2}{a}{x}{\phi(x)}{\lambda}     \]

So, let $\epsilon >0$, and let $\delta=\min(\delta_1,\delta_2)$. For
the same reasons as with previous limits proofs, this $\delta$ implies
both the inequalities involving $\epsilon$, which can be restated, by
definition of the absolute value, as:
\begin{equation*} \begin{aligned}
	-\epsilon < \varphi(x)-\lambda < \epsilon \\
	-\epsilon < \phi(x)-\lambda < \epsilon
\end{aligned} \end{equation*}

But we also have:
\[ \varphi(x) \le \psi(x) \le \phi(x) \]
\[ \Leftrightarrow \varphi(x)-\lambda \le \psi(x)-\lambda \le \phi(x)-\lambda \]

So:
\[ -\epsilon < \varphi(x)-\lambda \le \psi(x)-\lambda \le \phi(x)-\lambda < \epsilon \]
\[ \Leftrightarrow \abs{\psi(x)-\lambda} < \epsilon \]

Which concludes the proof, as we now have an $(\epsilon-\delta)$ statement
on $\psi$, equivalent to a limit.

\end{proof}

\hrr

We now have everything we need to start computing the limits involved
in the differentiation of sine:

\begin{theorem}
\[
	\boxed{\lim_{\epsilon\rightarrow 0} \frac{\sin\epsilon}{\epsilon} = 1}
\]
\end{theorem}
\begin{proof} Consider the three following blueish areas:
\begin{figure}[H]
	\centering
	\begin{minipage}{0.31\textwidth}
		\centering
		\begin{tikzpicture}[scale=.7]
			\tikzmath{
				\xmin = 0;
				\xmax = 5;
				\ymin = 0;
				\ymax = 5;
				\r = \xmax;
				\t = 35;
				\px = \r*cos(\t);
				\py = \r*sin(\t);
			}
			\coordinate (O)  at (0, 0);
			\coordinate (p)  at (\t:\r);
			\coordinate (xo) at (\xmax,0);

			\draw[->] (\xmin-0.5, 0) -- (\xmax+0.5, 0) node[below] {$\vec{x}$};
			\draw[->] (0, \ymin-.5) -- (0, \ymax+.5) node[left] {$\vec{y}$};

			\begin{scope}[fill=blue!8]
				\fill[clip] (\px,0) -- (p) -- (O);
			\end{scope}
			\draw[color=gray!30, dashed]
				(\xmin-1,\ymin-1) grid (\xmax+1,\ymax+1);

			\draw[black!30] (xo) arc[start angle=0, end angle=90, radius=\r];
			\draw[] (p) -- (\px,0) node [below]{$r\cos(\theta)$};
			\draw[] (O) -- (xo);
			\draw[->] (O) -- (p) node (pvec) [midway,above]{$r$};

			\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = xo--O--p};
			\draw[dashed] (p) -- (0,\py) node [below right]{$r\sin(\theta)$};
		\end{tikzpicture}
	\end{minipage}
	\begin{minipage}{0.31\textwidth}
		\centering
		\begin{tikzpicture}[scale=.7]
			\tikzmath{
				\xmin = 0;
				\xmax = 5;
				\ymin = 0;
				\ymax = 5;
				\r = \xmax;
				\t = 35;
				\py = \r*sin(\t);
			}
			\coordinate (O)  at (0, 0);
			\coordinate (p)  at (\t:\r);
			\coordinate (xo) at (\xmax,0);

			\draw[->] (\xmin-0.5, 0) -- (\xmax+0.5, 0) node[below] {$\vec{x}$};
			\draw[->] (0, \ymin-.5) -- (0, \ymax+.5) node[left] {$\vec{y}$};

			\begin{scope}[fill=blue!8]
				\fill[clip]
					 (xo) arc[start angle=0, end angle=\t, radius=\r]
					 -- (p) -- (O);
			\end{scope}
			\draw[color=gray!30, dashed]
				(\xmin-1,\ymin-1) grid (\xmax+1,\ymax+1);

			\draw[black!30] (xo) arc[start angle=0, end angle=90, radius=\r];
			\draw[] (xo) arc[start angle=0, end angle=\t, radius=\r];
			\draw[] (O) -- (xo);
			\draw[->] (O) -- (p) node (pvec) [midway,above]{$r$};

			\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = xo--O--p};
			\draw[dashed] (p) -- (0,\py) node [below right]{$r\sin(\theta)$};
		\end{tikzpicture}
	\end{minipage}
	\begin{minipage}{0.31\textwidth}
		\centering
		\begin{tikzpicture}[scale=.7]
			\tikzmath{
				\xmin = 0;
				\xmax = 5;
				\ymin = 0;
				\ymax = 5;
				\r = \xmax;
				\t = 35;
				\px = \r*cos(\t);
				\qy = \r*tan(\t);
			}
			\coordinate (O)  at (0, 0);
			\coordinate (p)  at (\t:\r);
			\coordinate (xo) at (\xmax,0);
			\coordinate (q)  at (\r,\qy);

			\draw[->] (\xmin-0.5, 0) -- (\xmax+0.5, 0) node[below] {$\vec{x}$};
			\draw[->] (0, \ymin-.5) -- (0, \ymax+.5) node[left] {$\vec{y}$};

			\begin{scope}[fill=blue!8]
				\fill[clip] (q) -- (O) -- (xo);
			\end{scope}
			\draw[color=gray!30, dashed]
				(\xmin-1,\ymin-1) grid (\xmax+1,\ymax+1);

			\draw[black!30] (xo) arc[start angle=0, end angle=90, radius=\r];
			\draw[] (O) -- (q) node []{};
			\draw[] (O) -- (xo) -- (q);
			\draw[->] (O) -- (p) node (pvec) [midway,above]{$r$};

			\draw[dashed] (q) -- (0,\qy) node [below right]{$r\tan(\theta)$};

			\pic [draw,"$\theta$",angle eccentricity=1.5,gray] {angle = xo--O--p};
		\end{tikzpicture}
	\end{minipage}
\end{figure}
The three areas are definitely ordered from smaller to bigger (left to right),
and we can also determine them: the middle one is that of a sector, while the
two side ones are right triangles (so their areas is half of the corresponding
rectangle). We then have the following inequalities:
\begin{equation*} \begin{aligned}
	~ && \frac12r^2\cos\theta\sin\theta &\le& \frac12r^2\theta &\le& \frac12r^2\tan\theta \\
	\Leftrightarrow && \cos\theta\sin\theta &\le& \theta &\le& \frac{\sin\theta}{\cos\theta} \\
	\Leftrightarrow && \cos\theta &\le& \frac{\theta}{\sin\theta} &\le& \frac{1}{\cos\theta} \\
	\Leftrightarrow && \frac1{\cos\theta} &\ge& \frac{\sin\theta}{\theta} &\ge& \cos\theta
\end{aligned} \end{equation*}

But, as $\theta$ goes to zero, the two extremes of this inequalities become:
\begin{equation*} \begin{aligned}
	\lim_{\theta\rightarrow 0}&
		\frac{1}{\cos\theta} &=\quad& 1;\quad&
	\lim_{\theta\rightarrow 0}&
		\cos\theta &=\quad& 1
\end{aligned} \end{equation*}

Hence by the \textit{squeeze theorem}, it follows that we \textit{must} have:
\[
	\boxed{\lim_{\theta\rightarrow 0} \frac{\sin\theta}{\theta} = 1}
\]

\end{proof}

As for the other limit:
\begin{theorem}
\[
	\boxed{\lim_{\epsilon\rightarrow 0} \frac{\cos\epsilon-1}{\epsilon} = 0}
\]
\end{theorem}
\begin{proof} We will rely on the previous limit; this will be a "proof
with a trick" (multiplying by $a/a=1$; in the present context, $a$ will
always be non-zero). Note also at the end that we can
apply the product rules for limits given the existence of both sublimits.
\begin{equation*} \begin{aligned}
	\lim_{\epsilon\rightarrow 0} \frac{\cos\epsilon-1}{\epsilon}
		&=&& \lim_{\epsilon\rightarrow 0}\left(
			\frac{\cos\epsilon-1}{\epsilon}
			\times\frac{\cos\epsilon+1)}{\cos\epsilon+1)}
		\right) \\
	~ &=&& \lim_{\epsilon\rightarrow 0}\left(
			\frac{\cos^2\epsilon-1}{\epsilon(\cos\epsilon+1))}
		\right) \\
	~ &=&& -\lim_{\epsilon\rightarrow 0}\left(
			\frac{\sin^2\epsilon}{\epsilon(\cos\epsilon+1))}
		\right) \\
	~ &=&& -\lim_{\epsilon\rightarrow 0}\left(
			\frac{\sin\epsilon}{\epsilon}\times\frac{\sin\epsilon}{\cos\epsilon+1}
		\right) \\
	~ &=&& -\underbrace{\lim_{\epsilon\rightarrow 0}(
			\frac{\sin\epsilon}{\epsilon})}_{\rightarrow 1}
		\times\underbrace{
			\lim_{\epsilon\rightarrow 0}(\frac{\sin\epsilon}{\cos\epsilon+1})
		}_{\rightarrow 0/2=0} \\
	~ &=&& \boxed{0} \\
\end{aligned} \end{equation*}
\end{proof}
\hrr
We now have everything to conclude: let's recapitulate all the
intermediate steps to compute $\sin'$:
\begin{theorem}[sine derivative]
\[
	(\forall x\in\mathbb{R}),\quad \boxed{\sin'(x) = \cos(x)}
\]
\end{theorem}

\begin{proof}
\begin{equation*} \begin{aligned}
	(\forall x \in\mathbb{R}),\quad\sin'(x) &\triangleq&& \lim_{\epsilon \rightarrow 0}
		\frac{\sin(x+\epsilon)-\sin x}{\epsilon} \\
	~ &=&& \lim_{\epsilon \rightarrow 0}
		\frac{\sin x\cos\epsilon+\cos x\sin\epsilon-\sin x}{\epsilon} \\
	~ &=&& \lim_{\epsilon \rightarrow 0}\left(
		\frac{\sin x(\cos\epsilon-1)}{\epsilon}+\frac{\cos x\sin\epsilon}{\epsilon}
		\right) \\
	~ &=&& \sin x\underbrace{
			\lim_{\epsilon \rightarrow 0}\frac{\cos\epsilon-1}{\epsilon}
		}_{=0}
		+\cos x\underbrace{
			\lim_{\epsilon\rightarrow 0}\frac{\sin\epsilon}{\epsilon}
		}_{=1} \\
	~ &=&& \boxed{\cos x}
\end{aligned} \end{equation*}
\end{proof}
\hr
$\bm{d\cos t/dt}$\,\\
\begin{theorem}[cosine derivative]
\[
	(\forall x\in\mathbb{R}),\quad \boxed{\cos'(x) = -\sin(x)}
\]
\end{theorem}
\begin{proof}
The results follow from the shifts formulas \ref{L02E05:thm:ref-shift}
\begin{equation*} \begin{aligned}
	(\forall x\in\mathbb{R}),\quad \cos'(x) &&=\quad&
		\sin'(x+\frac\pi2) \\
	~ &&=\quad& (\sin\circ(y \mapsto y+\frac\pi2))'(x) \\
	~ &&=\quad& \cos(x+\frac\pi2) \\
	~ &&=\quad& \boxed{-\sin(x)}
\end{aligned} \end{equation*}
\end{proof}

\hr
$\bm{d e^t/dt}$\,\\
This one, as mentioned in the book, is "trivial" when we define the
exponential function to be precisely the function which is equal to
its derivative (and such as $e^0$ = 1). \\

And this is usually the way the exponential function will be first
introduced to students. You may want to have a look at other equivalent
characterization of the function\footnote
{\url{https://en.wikipedia.org/wiki/Characterizations\_of\_the\_exponential\_function}}.
Trying to compute an exponential defined on a development in infinite
series carries a certain aesthetic for instance.

\[ \boxed{\frac{d}{dt}e^t \triangleq e^t} \]

\hr
$\bm{d\ln t/dt}$\,\\
As for the exponential, there can be some variety here depending
on how we \textit{characterize} the $\ln$ function
\footnote{\url{https://en.wikipedia.org/wiki/Natural\_logarithm\#Definitions}}.
Usually, it will be introduced as the \textit{inverse function} of
the exponential:
\begin{definition}[natural logarithm]
The natural logarithm function is defined as the function $\ln$ such that:
\[
	(\forall x\in\mathbb{R}),\quad \boxed{e^{\ln(x)} = x}
\]
\end{definition}
\begin{remark} To rigorously establish this definition, would have
needed to prove that the exponential is invertible.
% TODO?
%	Strictly positive => 1-to-1 => invertible
%	e-x * e^x = e^0 = 1 \forall x so e^x can't be zero \forall x
%		and e^0 = 1 => exp strictly positive
%	suffice to prove that e^x * e^y = e^x+y then
%	https://math.stackexchange.com/a/749179
\end{remark}

\begin{theorem}[natural logarithm derivative]
\[
	(\forall x\in\mathbb{R}),\quad \boxed{\ln'(x) = \frac1x}
\]
\end{theorem}
\begin{proof}
The proof develops from the previous definition of the logarithm
by integrating both side and then applying the chain rule:
\begin{equation*} \begin{aligned}
	~ && (\forall x\in\mathbb{R}),\quad e^{\ln(x)} &&=\quad& x \\
	\Leftrightarrow && \frac{d}{dx}e^{\ln(x)} &&=\quad& \frac{d}{dx}x \\
	\Leftrightarrow && \ln'(x)\underbrace{e^{\ln(x)}}_{=x} &&=\quad& 1 \\
	\Leftrightarrow && \ln'(x) &&=\quad& \boxed{\frac1x}
\end{aligned} \end{equation*}
\end{proof}

\begin{remark} For the sake of completeness, some authors\footnote{
\url{https://www.whitman.edu/mathematics/calculus\_late\_online/section09.02.html}},
will for instance start by defining the logarithm as an integral,
and then define the exponential as the inverse of the logarithm. From which
they can prove that the derivative of the exponential is the exponential.
\end{remark}
\end{document}