diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex index 349aa41..f4bb7b6 100644 --- a/Bookshelf/Apostol.tex +++ b/Bookshelf/Apostol.tex @@ -20,6 +20,37 @@ \chapter{Glossary}% \label{chap:glossary} +\section{\defined{Characteristic Function}}% +\label{sec:def-characteristic-function} + +Let $S$ be a set of points on the real line. +The \textbf{characteristic function} of $S$ is the function $\mathcal{X}_S$ such + that $\mathcal{X}_S(x) = 1$ for every $x$ in $S$, and $\mathcal{X}_S(x) = 0$ + for those $x$ not in $S$. + +\begin{definition} + + \lean{Common/Set/Basic}{Set.characteristic} + +\end{definition} + +\section{\defined{Infimum}}% +\label{sec:def-infimum} + +A number $B$ is called an \textbf{infimum} of a nonempty set $S$ if $B$ has + the following two properties: + \begin{enumerate}[(a)] + \item $B$ is a lower bound for $S$. + \item No number greater than $B$ is a lower bound for $S$. + \end{enumerate} +Such a number $B$ is also known as the \textbf{greatest lower bound}. + +\begin{definition} + + \lean{Mathlib/Order/Bounds/Basic}{IsGLB} + +\end{definition} + \section{\defined{Partition}}% \label{sec:def-partition} @@ -42,16 +73,26 @@ A collection of points satisfying \eqref{sec:partition-eq1} is called a \end{definition} +\section{\partial{Refinement}}% +\label{sec:def-refinement} + +Let $P$ be a \nameref{sec:def-partition} of closed interval $[a, b]$. +A \textbf{refinement} $P'$ of $P$ is a partition formed by adjoining more + subdivision points to those already in $P$. + +$P'$ is said to be \textbf{finer than} $P$. The union of two partitions $P_1$ + and $P_2$ is called the \textbf{common refinement} of $P_1$ and $P_2$. + \section{\defined{Step Function}}% \label{sec:def-step-function} -A function $s$, whose domain is a closed interval $[a, b]$, is called a step - function if there is a \nameref{sec:def-partition} - $P = \{x_0, x_1, \ldots, x_n\}$ of $[a b]$ such that $s$ is constant on each +A function $s$, whose domain is a closed interval $[a, b]$, is called a + \textbf{step function} if there is a \nameref{sec:def-partition} + $P = \{x_0, x_1, \ldots, x_n\}$ of $[a, b]$ such that $s$ is constant on each open subinterval of $P$. That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$ such that $$s(x) = s_k \quad\text{if}\quad x_{k-1} < x < x_k.$$ -Step functions are sometimes called piecewise constant functions. + Step functions are sometimes called \textbf{piecewise constant functions}. \vspace{8pt} \noindent @@ -64,9 +105,38 @@ Step functions are sometimes called piecewise constant functions. \end{definition} +\section{\defined{Supremum}}% +\label{sec:def-supremum} + +A number $B$ is called a \textbf{supremum} of a nonempty set $S$ if $B$ has + the following two properties: + \begin{enumerate}[(a)] + \item $B$ is an upper bound for $S$. + \item No number less than $B$ is an upper bound for $S$. + \end{enumerate} +Such a number $B$ is also known as the \textbf{least upper bound}. + +\begin{definition} + + \lean{Mathlib/Order/Bounds/Basic}{IsLUB} + +\end{definition} + \chapter{A Set of Axioms for the Real-Number System}% \label{chap:set-axioms-real-number-system} +\section{\defined{Completeness Axiom}}% +\label{sec:completeness-axiom} + +Every nonempty set $S$ of real numbers which is bounded above has a supremum; + that is, there is a real number $B$ such that $B = \sup{S}$. + +\begin{axiom} + + \lean{Mathlib/Data/Real/Basic}{Real.exists\_isLUB} + +\end{axiom} + \section{\verified{Lemma 1}}% \label{sec:lemma-1} @@ -80,8 +150,8 @@ Nonempty set $S$ has supremum $L$ if and only if set $-S$ has infimum $-L$. \divider Suppose $L = \sup{S}$ and fix $x \in S$. - By definition of the supremum, $x \leq L$ and $L$ is the smallest value - satisfying this inequality. + By definition of the \nameref{sec:def-supremum}, $x \leq L$ and $L$ is the + smallest value satisfying this inequality. Negating both sides of the inequality yields $-x \geq -L$. Furthermore, $-L$ must be the largest value satisfying this inequality. Therefore $-L = \inf{-S}$. @@ -103,7 +173,8 @@ Every nonempty set $S$ that is bounded below has a greatest lower bound; that Let $S$ be a nonempty set bounded below by $x$. Then $-S$ is nonempty and bounded above by $x$. - By the completeness axiom, there exists a supremum $L$ of $-S$. + By the \nameref{sec:completeness-axiom}, there exists a + \nameref{sec:def-supremum} $L$ of $-S$. By \nameref{sec:lemma-1}, $L$ is a supremum of $-S$ if and only if $-L$ is an infimum of $S$. @@ -130,8 +201,8 @@ For every real $x$ there exists a positive integer $n$ such that $n > x$. \end{proof} -\section{\verified{Theorem I.30}}% -\label{sec:theorem-i.30} +\section{\verified{Archimedean Property of the Reals}}% +\label{sec:archimedean-property-reals} If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive integer $n$ such that $nx > y$. @@ -182,8 +253,8 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities Suppose $x > a$. Then there exists some $c > 0$ such that $a + c = x$. - By \nameref{sec:theorem-i.30}, there exists an integer $n > 0$ such that - $nc > y$. + By \nameref{sec:archimedean-property-reals}, there exists an integer $n > 0$ + such that $nc > y$. Rearranging terms, we see $y / n < c$. Therefore $a + y / n < a + c = x$. But by hypothesis, $x \leq a + y / n$. @@ -220,8 +291,8 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities Suppose $x < a$. Then there exists some $c > 0$ such that $x = a - c$. - By \nameref{sec:theorem-i.30}, there exists an integer $n > 0$ such that - $nc > y$. + By \nameref{sec:archimedean-property-reals}, there exists an integer $n > 0$ + such that $nc > y$. Rearranging terms, we see that $y / n < c$. Therefore $a - y / n > a - c = x$. But by hypothesis, $x \geq a - y / n$. @@ -257,7 +328,8 @@ If $S$ has a supremum, then for some $x$ in $S$ we have $x > \sup{S} - h$. \divider - By definition of a supremum, $\sup{S}$ is the least upper bound of $S$. + By definition of a \nameref{sec:def-supremum}, $\sup{S}$ is the least upper + bound of $S$. For the sake of contradiction, suppose for all $x \in S$, $x \leq \sup{S} - h$. This immediately implies $\sup{S} - h$ is an upper bound of $S$. @@ -280,7 +352,8 @@ If $S$ has an infimum, then for some $x$ in $S$ we have $x < \inf{S} + h$. \divider - By definition of an infimum, $\inf{S}$ is the greatest lower bound of $S$. + By definition of an \nameref{sec:def-infimum}, $\inf{S}$ is the greatest lower + bound of $S$. For the sake of contradiction, suppose for all $x \in S$, $x \geq \inf{S} + h$. This immediately implies $\inf{S} + h$ is a lower bound of $S$. @@ -321,7 +394,7 @@ If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and Let $x \in C$. By definition of $C$, there exist elements $a' \in A$ and $b' \in B$ such that $x = a' + b'$. - By definition of a supremum, $a' \leq \sup{A}$. + By definition of a \nameref{sec:def-supremum}, $a' \leq \sup{A}$. Likewise, $b' \leq \sup{B}$. Therefore $a' + b' \leq \sup{A} + \sup{B}$. Since $x = a' + b'$ was arbitrarily chosen, it follows $\sup{A} + \sup{B}$ @@ -390,7 +463,7 @@ If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and Let $x \in C$. By definition of $C$, there exist elements $a' \in A$ and $b' \in B$ such that $x = a' + b'$. - By definition of an infimum, $a' \geq \inf{A}$. + By definition of an \nameref{sec:def-infimum}, $a' \geq \inf{A}$. Likewise, $b' \geq \inf{B}$. Therefore $a' + b' \geq \inf{A} + \inf{B}$. Since $x = a' + b'$ was arbitrarily chosen, it follows $\inf{A} + \inf{B}$ @@ -577,7 +650,7 @@ A set consisting of a single point. \begin{proof} Let $S$ be a set consisting of a single point. - By definition of a Point, $S$ is a rectangle in which all vertices coincide. + By definition of a point, $S$ is a rectangle in which all vertices coincide. By \nameref{sec:choice-scale}, $S$ is measurable with area its width times its height. The width and height of $S$ is trivially zero. @@ -658,7 +731,7 @@ The union of a finite collection of line segments in a plane. \paragraph{Base Case}% Consider a set $S$ consisting of a single line segment in a plane. - By definition of a Line Segment, $S$ is a rectangle in which one side has + By definition of a line segment, $S$ is a rectangle in which one side has dimension $0$. By \nameref{sec:choice-scale}, $S$ is measurable with area its width $w$ times its height $h$. @@ -1271,8 +1344,7 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$ \divider - This is immediately proven by applying Hermite's Identity as shown in - \nameref{sec:exercise-1.11.5}. + This is immediately proven by applying \nameref{sec:hermites-identity}. \end{proof} @@ -1288,20 +1360,17 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$ \divider - This is immediately proven by applying Hermite's Identity as shown in - \nameref{sec:exercise-1.11.5}. + This is immediately proven by applying \nameref{sec:hermites-identity}. \end{proof} -\section{\partial{Exercise 1.11.5}}% -\label{sec:exercise-1.11.5} +\section{\partial{Hermite's Identity}}% +\label{sec:hermites-identity} The formulas in Exercises 4(d) and 4(e) suggest a generalization for $\floor{nx}$. State and prove such a generalization. -\note{The stated generalization is known as "Hermite's Identity."} - \begin{proof} \lean{Bookshelf/Apostol/Chapter\_1\_11} @@ -1568,11 +1637,10 @@ Now apply Exercises 4(a) and (b) to the bracket on the right. \label{sec:exercise-1.11.8} Let $S$ be a set of points on the real line. -The \textit{characteristic function} of $S$ is, by definition, the function - $\mathcal{X}_S$ such that $\mathcal{X}_S(x) = 1$ for every $x$ in $S$, and - $\mathcal{X}_S(x) = 0$ for those $x$ not in $S$. -Let $f$ be a step function which takes the constant value $c_k$ on the $k$th - open subinterval $I_k$ of some partition of an interval $[a, b]$. +Let $\mathcal{X}_S$ denote the \nameref{sec:def-characteristic-function} of $S$. +Let $f$ be a \nameref{sec:def-step-function} which takes the constant value + $c_k$ on the $k$th open subinterval $I_k$ of some partition of an interval + $[a, b]$. Prove that for each $x$ in the union $I_1 \cup I_2 \cup \cdots \cup I_n$ we have $$f(x) = \sum_{k=1}^n c_k\mathcal{X}_{I_k}(x).$$ This property is described by saying that every step function is a linear @@ -1583,7 +1651,7 @@ This property is described by saying that every step function is a linear Let $x \in I_1 \cup I_2 \cup \cdots \cup I_n$ and $N = \{1, \ldots, n\}$. Let $k \in N$ such that $x \in I_k$. Consider an arbitrary $j \in N - \{k\}$. - By definition of a partition, $I_j \cap I_k = \emptyset$. + By definition of a nameref{sec:def-partition}, $I_j \cap I_k = \emptyset$. That is, $I_j$ and $I_k$ are disjoint for all $j \in N - \{k\}$. Therefore, by definition of the characteristic function, $\mathcal{X}_{I_k}(x) = 1$ and $\mathcal{X}_{I_j}(x) = 0$ for all