\input{latex-macros/handout-preamble.tex}
\inhandout{
\decideaboutsolutions
\usesimpleproblems
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Problem starts here
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{problem}
\PTAGfilename{CP0303_F18_functions.tex}
\PTAGhistory{S09_cp5m}
%\PTAGkeywords{}
%
The Elementary 18.01 Functions ($\EF$'s) are the set of functions of
one real variable defined recursively as follows:

\textbf{Base cases:}
\begin{itemize}
\item The identity function, $\ide(x) \eqdef x$ is an $\EF$,
\item any constant function is an $\EF$,
\item the sine function is an $\EF$,
\end{itemize}

\textbf{Constructor cases:}

If $f,g$ are $\EF$'s, then so are
\begin{enumerate}
\item $f + g$, $fg$, $e^g$ (the constant $e$),\label{+-}
\item the inverse function $f^{-1}$,\label{inversefunc}
\item the composition $f \compose g$.\label{cmp}
\end{enumerate}

\bparts

\ppart\label{1over} Prove that the function $1/x$ is an $\EF$.

\textbf{Warning:} Don't confuse $1/x = x^{-1}$ with the inverse,
$\ide^{-1}$ of the identity function $\ide(x)$.  The inverse
$\ide^{-1}$ is equal to $\ide$.

\solution{$\log x$ is the inverse of $e^x$ so $\log x \in \EF$.  Therefore
  so is $c\cdot \log x$ for any constant $c$, and hence $e^{c \log x} =
  x^c \in \EF$.  Now let $c = -1$ to get $x^{-1} = 1/x \in
  \EF$.\footnote{There's a little problem here: since $\log x$ is not
    real-valued for $x \leq 0$, the function $f(x) \eqdef 1/x$ constructed
    in this way is only defined for $x >0$.  To get an $\EF$ equal to
    $1/x$ defined for all $x \neq 0$, use $\paren{x/\abs{x}}\cdot
    f(\abs{x})$, where $\abs{x} = \sqrt{x^2}$.}}

\ppart Prove by Structural Induction on this definition that the
Elementary 18.01 Functions are \emph{closed under taking derivatives}.
That is, show that if $f(x)$ is an $\EF$, then so is $f^{\prime} \eqdef
df/dx$.  (Just work out 2 or 3 of the most interesting constructor cases;
you may skip the less interesting ones.)

\solution{
\begin{proof}
By Structural Induction on def of $f \in \EF$.  The induction hypothesis
is the above statement to be shown.

\item[Base Cases:] We want to show that the derivatives of all the
  base case functions are in $\EF$.

  This is easy: for example, $d\, \ide(x)/dx = 1$ is a constant function,
  and so is in $\EF$. Similarly, $d\, \sin(x)/dx = \cos(x)$ which is
  also in $\EF$ since $\cos(x) = \sin(x+\pi/2) \in \EF$ by rules for
  constant functions, the identity function, sum, and composition with
  sine.

This proves that the induction hypothesis holds in the Base cases.

\item[Constructor Cases:] ($f^{-1}$).  Assume $f, df/dx \in \EF$ to prove
  $d\, f^{-1}(x)/dx \in \EF$.
Letting $y = f(x)$, so $x=f^{-1}(y)$, we know from Leibniz's rule in
calculus that
\begin{equation}\label{Leib}
df^{-1}(y)/dy = dx/dy = \frac{1}{dy/dx}.
\end{equation}
For example,
\[
d \sin^{-1}(y)/dy = 1/(d \sin(x)/dx) = 1/\cos(x) = 1/\cos(\sin^{-1}(y)).
\]
Stated as in ~(\ref{Leib}), this rule is easy to remember, but can easily
be misleading because of the variable switching between $x$ and $y$.  It's
more clearly stated using variable-free notation:
\begin{equation}\label{Leib2}
(f^{-1})' = (1/f') \compose f^{-1}.
\end{equation}
Now, since $f' \in \EF$ (by assumption), so is $1/f'$ (by
part~\eqref{1over}) and $f^{-1}$ (by constructor rule~\ref{inversefunc}.),
and therefore so is their composition (by rule~\ref{cmp}).  Hence the
righthand side of equation~(\ref{Leib2}) defines a function in $\EF$.

\item[Constructor Case:] ($f \compose g$).  Assume $f, g, df/dx, dg/dx \in \EF$
to prove $d(f \compose g)(x)/dx \in \EF$.

The Chain Rule states that
\[
\frac{d(f(g(x)))}{dx} = \frac{d f(g)}{dg}\cdot\frac{dg}{dx}.
\]
Stated more clearly in variable-free notation, this is
\[
(f \compose g)' = (f' \compose g) \cdot g'.
\]
The righthand side of this equation defines a function in $\EF$ by
constructor rules~\ref{cmp}.\ and~\ref{+-}.

The other Constructor cases are similar, so we conclude that the induction
hypothesis holds in all Constructor cases.

This completes the proof by structural induction that the statement holds
for all $f \in \EF$.
\end{proof}
}
\eparts
\end{problem}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Problem ends here
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{latex-macros/handout-postamble.tex}