\documentclass{article}
\usepackage{fullpage,amsmath}
\usepackage{hyperref}
\usepackage{amssymb}
\usepackage{listings}
\usepackage{mathtools}


%%  Common macros for the course CSC165H1F,
%%  on the St. George Campus at the University of Toronto.
%%
%%  Copyright (c) 2009-2011 Francois Pitt <fpitt@cs.utoronto.ca>
%%
%%  This work may be distributed and/or modified under the conditions of
%%  the LaTeX Project Public License, either version 1.3 of this license
%%  or (at your option) any later version.
%%  The latest version of this license is in
%%      http://www.latex-project.org/lppl.txt
%%  and version 1.3 or later is part of all distributions of LaTeX
%%  version 2003/12/01 or later.
%%
%%  This work has the LPPL maintenance status "author-maintained".
%%
%%  The Current Maintainer of this work is
%%  Francois Pitt <fpitt@cs.utoronto.ca>.
%%
%%  This work consists of the file macros-165.tex.

% Trick so that math symbols are bold when text is.
\let\seiresfb\bfseries\def\bfseries{\boldmath\seiresfb}
\let\seiresdm\mdseries\def\mdseries{\unboldmath\seiresdm}

% Spacing macros with default argument.
\newcommand*{\vstretch}[1][1]{\vspace*{\stretch{#1}}}
\newcommand*{\hstretch}[1][1]{\hspace*{\stretch{#1}}}

% General fonts and characters.
\let\altemph\textsl  % alternate way to emphasize
\let\strong\textbf  % strong emphasis
\let\latinabb\emph  % abbreviations of latin phrases
\let\code\texttt  % code fragments
\let\const\textsf  % constants
\let\term\textbf  % newly-introduced (or defined) words
\let\var\mathrm  % multi-letter variables (or constants)
\let\pred\mathbf  % predicates
\newcommand*{\txtbksl} {\symbol{"5C}}% \
\newcommand*{\txtcaret}{\symbol{"5E}}% ^
\newcommand*{\txtunder}{\symbol{"5F}}% _
\newcommand*{\txtlcurl}{\symbol{"7B}}% {
\newcommand*{\txtrcurl}{\symbol{"7D}}% }
\newcommand*{\txttilde}{\symbol{"7E}}% ~
\newcommand*{\N}{\ensuremath{\mathbb{N}}}  % requires amssymb
\newcommand*{\Z}{\ensuremath{\mathbb{Z}}}  % requires amssymb
\newcommand*{\Q}{\ensuremath{\mathbb{Q}}}  % requires amssymb
\newcommand*{\R}{\ensuremath{\mathbb{R}}}  % requires amssymb
\newcommand*{\bigOh}{\mathcal{O}}
\newcommand*{\onehalf}{\ensuremath{{}^1\!\!/\!_2}}

% Abbreviations of latin phrases.
\newcommand*{\ie}{\latinabb{i.e.}}
\newcommand*{\eg}{\latinabb{e.g.}}
\newcommand*{\etc}{\latinabb{etc}}
\newcommand*{\vs}{\latinabb{vs}}

% General math macros.
\newcommand*{\comp}[1]{\overline{#1}}  % set complement
\newcommand*{\emptystr}{\varepsilon}  % empty string
\newcommand*{\lequiv}{\mathrel{\ \Longleftrightarrow\ }}  % equivalence
\newcommand*{\lxor}{\oplus}  % exclusive or
\newcommand*{\cat}{\cdot}  % string concatenation
\newcommand*{\invisible}[1]{\mathrel{\hphantom{#1}}}
% floors and ceilings, with optional size-changing command,
% e.g., \floor[\Big]{x/2} generates '\Big\lfloor{x/2}\Big\rfloor'
\newcommand*{\floor}[2][]{{#1\lfloor}{#2}{#1\rfloor}}
\newcommand*{\ceil}[2][]{{#1\lceil}{#2}{#1\rceil}}
\newcommand*{\lcm}{\operatorname{lcm}}  % requires amsmath
\newcommand*{\size}{\operatorname{size}}  % requires amsmath

% Redefined symbols from amssymb.
\renewcommand*{\emptyset}{\varnothing}  % rounder than default
\let\bigiff\iff
\renewcommand*{\iff}{\mathrel{\Leftrightarrow}}  % smaller than default
\let\bigimplies\implies
\renewcommand*{\implies}{\mathrel{\Rightarrow}}  % smaller than default
\renewcommand*{\ge}{\geqslant}  % with slanted line under the > sign
\renewcommand*{\le}{\leqslant}  % with slanted line under the < sign

% For algorithms, in Python.
\let\kw\textbf  % keywords
\let\proc\textsc  % function names
\newcommand*{\opgets}[1]{\mathrel{#1=}}
\newcommand*{\eq}{\mathrel{==}}
\newcommand*{\True}{\const{True}}
\newcommand*{\False}{\const{False}}
\newcommand*{\None}{\const{None}}
\newcommand*{\cmod}{\mathbin{\%}}
\newcommand*{\len}{\operatorname{len}}  % requires amsmath

% Like {itemize} but using less vertical space.
\newenvironment*{points}
 {\ifvmode\else\unskip\par\fi\begin{list}{$\bullet$}
   {\setlength{\topsep}{.25ex plus .125ex minus .1825ex}
    \setlength{\itemsep}{\topsep}\setlength{\parsep}{0ex}
    \setlength{\leftmargin}{1.75em}\setlength{\labelsep}{.5em}
    \setlength{\labelwidth}{1.75em}}\ignorespaces}
 {\ifvmode\else\unskip\fi\end{list}\ignorespaces}

% Checkboxes and checklists.
\newcommand*{\cbox}[1]{{\fboxrule.125ex\fboxsep0ex
    \framebox[2.75ex]{\rule[-.75ex]{0ex}{2.75ex}\smash{#1}}}}
\newcommand*{\cmark}{\raisebox{.0625ex}{$\surd$\kern.125ex}}
\newcommand*{\xmark}{\raisebox{-.1875ex}{\kern.0625ex{X}}}
\newcommand*{\checkbox}{{\sf\cbox{}}}
\newcommand*{\checkedbox}{{\sf\cbox{\cmark}}}
\newcommand*{\markedbox}{{\sf\cbox{\xmark}}}
\newenvironment{checklist}{\begin{list}{\checkbox}{}}{\end{list}}
\newcommand*{\checkeditem}{\item[\checkedbox]}
\newcommand*{\markeditem}{\item[\markedbox]}

% Proof-related environments and macros.
\newcommand*{\just}{{\quad\#\ }}  % justification for a proof step
\newenvironment*{pindent}
   {\begin{list}{}
       {\topsep 0pt
        \partopsep 0pt
        \itemsep 0pt
        \parsep 0pt
        \parskip 0pt}\item\relax}
   {\unskip\end{list}\ignorespaces}
% Usage: \begin{assumption}[<pre-text>]{<assumption>}
%          ...body...
%        \end{assumption}{<conclusion>}
% is formatted as
%    <pre-text> assume <assumption>
%        ...body...
%    <conclusion>
% or if <pre-text> is empty,
%    Assume <assumption>
%        ...body...
%    <conclusion>
\newenvironment*{assumption}[2][]
   {\unskip\ifvmode\else\par\fi
    {#1} \ifx\empty#1\empty\expandafter\uppercase\fi{a}ssume {#2}
    \begin{pindent}}
   {\end{pindent}}
% Usage: \begin{pickavalue}[<pre-text>]{<names>}
%          ...body...
%        \end{pickavalue}{<conclusion>}
% is formatted as
%    <pre-text> let <names>
%    ...body...
%    <conclusion>
% or if <pre-text> is empty,
%    Let <names>
%    ...body...
%    <conclusion>
\newenvironment*{pickavalue}[2][]
   {\unskip\ifvmode\else\par\fi
    {#1} \ifx\empty#1\empty\expandafter\uppercase\fi{l}et {#2}
    \par\ignorespaces}
   {\unskip\par\ignorespaces}



\DeclarePairedDelimiter\abs{\lvert}{\rvert}%
\DeclarePairedDelimiter\norm{\lVert}{\rVert}%



\title{CSC165, Summer 2014\\
A Primer on Proving Inequalities}

\renewcommand{\today}{~}
\hypersetup{pdfpagemode=Fullscreen,
  colorlinks=true,
  linkfileprefix={}}
\begin{document}
\maketitle


\section{Introduction}

In this primer, we describe some elementary techniques for proving inequalities. Here are some properties of inequalities (some of those are taken from Section 1.5 of the notes):
For anye $x \in \mathbb{R}, y \in \mathbb{R}, w \in \mathbb{R}, z \in \mathbb{R}$:
\begin{align}
&	(x < y)\land(w \le z)  \implies [x+w < y + z] \\
&	(x< y) \land (z > 0 )  \implies [xz < yz] \\
&	(x< y) \land (z < 0 )  \implies [xz > yz] \\
&	(x < y) \land (y \le z)  \implies [x<z] \\
&	(x \le y) \land (y < z)  \implies [x<z] \\
&	(x \le y) \land (y \le z)  \implies [x\le z] \\
&	|x+y| \le |x| +|y| \\
&	x^2 \ge 0
\end{align}


\section{$(x< y) \land (z > 0 )  \implies [xz < yz]$, $(x< y) \land (z < 0 )  \implies [xz > yz]$}
Basically, multiplying (or dividing) by a positive number preserves the inequality. Multiplying (or dividing) by a negative number ``flips" the inequality.

For example, for real numbers $a$ and $b$,  
	$$a > b \Leftrightarrow -b < -a, $$ 

\noindent since we transform the inequality by multiplying it by $-1$, which is a negative number (both going left-to-right and right-to-left).

For a positive natural number $n$, 
	$$n^2 > 1 \Leftrightarrow n^3 > n,$$

\noindent since we transform the inequality by multiplying it by $n$ (going left-right) or dividing it by $n$ (going right-to-left), and $n$ is a positive number by assumption\footnote{Strictly speaking the assumption that $n$ is positive (i.e., not zero) is not needed there, since it follows from both $n^2 > 1$ and $n^3 > n$.}

Keep in mind that if $z$ is $0$, the inequality is not preserved: $1 < 2$, but it is not the case that $0*1 = 0*2$. It is, however, true that $(x< y) \land (z \ge 0 )  \implies [xz \le yz]$, with $xz=yz$ happening when $z = 0$.

\newpage
\section{$(x < y)\land(w \le z)  \implies [x+w < y + z]$}

First, it's important to have the intuition for why this is true. Imagine you're starting with
$$
	x < y.
$$

\noindent Now if we add the smaller value ($w$) to the left-hand side (LHS), which is smaller to begin with, and the larger (or equal to $w$) value ($z$) to the right-hand side (RHS), then the inequality still holds (i.e.,  $[x+w < y + z]$ is true).


Suppose  that we would like to prove that, for any $n>1$, 
	$$6n^3 > 3n+2.$$

The idea is to use that for any  $n > 1$,  $3n^3 > 3n$ and $2n^3 > 2$.

First, we prove that for any natural $n > 1$ and any positive real $a$,  $a n^3 > a n$:
\vspace{0.1in}
\begin{pindent}
	\begin{assumption}{$n  \in \mathbb{N}, a \in \mathbb{R}^{\ge 0}$}
	\begin{assumption}{$n > 1$}
		Then $n^2 = n*n > n*1 = n > 1$\just{multiplication by a positive number $n$, algebra, assumption that $n>1$}\\
		Then $n^2 > 1$\just{omit intermediate terms in the line above}\\
		Also $a n > a*1 > 0$\just{multiply both sides of an inequality by $3>0$}\\
		Then $a n^3 > an$\just{multiply both sides of an inequality by $3n>0$}
	\end{assumption}{Then $[n>1] \implies an^3 > an$\just{introduce implication}}
	\end{assumption}{Then $\forall n  \in \mathbb{N}, \forall a \in \mathbb{R}^{\ge 0}, [n>1] \implies an^3 > a n$\just{introduce universal twice}}
\end{pindent}
\vspace{0.1in}
	
Note that in order to obtain this proof, we could start with the the thing we're trying to prove, and ``work backwards:" Start at $a n^3 > a n$, and then divide by $a n$ to get $n^2 > 1$. When presenting the proof, we first prove $n^2 > 1$ (which is true since $n>1$), and then get to $3n^3 > 3n$, but we know where to start because we started with what we wanted to prove and then worked backwards.

You can similarly prove that $2n^3 > 2$ for $n> 1$.

Now we can prove that for any $n>1$,  $6n^3 > 3n+2$. We start at what we're trying to prove and work backwards to obtain the proof. But be careful: when working backwards, we need to make sure that the derivation will actually be correct when presenting it going ``forward."

We start at $6n^3 > 3n+2$. This is implied by $n^3 + 3n^3 + 2n^3 > 3n + 2$ (we have just re-expressed the LHS.) This is implied by $n^3 + 2n^3 > 2$ since for $n>1$ since we proved that  $a n^3 > a n$ for positive $a$ (and we can set $a = 3$). (Note that it's not true that for $n>1$, $n^3 + 3n^3 + 2n^3 > 3n + 2 \implies n^3 + 2n^3 > 2$, but it is true that for $n > 1$, $ n^3 + 2n^3 > 2 \implies n^3 + 3n^3 + 2n^3 > 3n + 2$. The direction in which we work is important.)  Now $n^3 + 2n^3 > 2$ is implied by $n^3  > 0$ since we can prove (but haven't proven here that $2n^3 > 2$ for $n > 1$. $n^3 > 0$ is true since $n > 0$, and so $n*n^2 > 0*n^2$ since $n^2> 0$.

We now prove the statement by working backwards.

\vspace{0.1in}
\begin{pindent}
	\begin{assumption}{$n  \in \mathbb{N}$}
	\begin{assumption}{$n > 1$}
		Then $n > 0$\just{$n > 1 > 0$}\\
		Then $n^2*n > n^2 0$\just{$n^2 > 0$}\\
		Then $n^3 > 0$\just{algebra}\\
		Then $n^3 + 3n^3 > 3n$\just{$3n^3>3n$ for $n> 1$ proved above, $n>1$ by assumption, $(x< y) \land (z > 0 )  \implies [xz < yz]$}\\
		Then $n^3 + 3n^3 + 2n^2> 3n + 2$\just{$2n^2>2$ for $n>1$ proved by the reader, $n>1$ by assumption, $(x< y) \land (z > 0 )  \implies [xz < yz]$}\\
		Then $6n^3 > 3n + 2$\just{algebra}
	\end{assumption}{Then $[n>1] \implies 6n^3 > 3n + 2$\just{introduce implication}}
	\end{assumption}{Then $\forall n  \in \mathbb{N}, [n>1] \implies 6n^3 > 3n + 2$\just{introduce universal}}
\end{pindent}
\vspace{0.1in}

\section{$x^2 \ge 0$}

The square of any real number is non-negative. Why is this true? One way to see it is to say that $x^2 = x*x$, so it's either a product of two negative numbers or a product of two non-negative numbers. Either way, it's non-negative.

The property $x^2 \ge 0$ is sometimes useful in itself. Here's another instance where it's useful. To prove that $x^2-2x+2 > 0$, we might say $x^2 -2x+2 = x^2-2x+1+1 = (x-1)^2+1 > 0$, where the last step is justified by starting with $1>0$, and then adding $(x-1)^2$ to the LHS and $0$ to the RHS.


\end{document}