Draft up Exercises 1.11.

Bookshelf/Real.lean

@@ -1,6 +1,7 @@
 import Bookshelf.Real.Basic
 import Bookshelf.Real.Function
 import Bookshelf.Real.Geometry
+import Bookshelf.Real.Int
 import Bookshelf.Real.Rational
 import Bookshelf.Real.Sequence
 import Bookshelf.Real.Set

Bookshelf/Real/Int.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Real.Basic
+
+namespace Real
+
+/--
+Check whether a real number is an integer.
+-/
+def isInt (x : ℝ) := x = Int.floor x
+
+end Real

Exercises/Apostol.lean

@@ -1 +1,2 @@
-import Exercises.Apostol.Chapter_I_3
+import Exercises.Apostol.Chapter_I_03
+import Exercises.Apostol.Chapter_1_11

Exercises/Apostol/Chapter_1_11.lean

@@ -0,0 +1,75 @@
+import Bookshelf.Real.Int
+import Mathlib.Data.Real.Basic
+
+/-! # Exercises.Apostol.Exercises_1_11 -/
+
+namespace Exercises.Apostol.Exercises_1_11
+
+/-! ## Exercise 4
+
+Prove that the greatest-integer function has the properties indicated.
+-/
+
+/-- ### Exercise 4a
+
+`⌊x + n⌋ = ⌊x⌋ + n` for every integer `n`.
+-/
+theorem exercise_4a (x : ℝ) (n : ℤ) : ⌊x + n⌋ = ⌊x⌋ + n := by
+  sorry
+
+/-- ### Exercise 4b
+
+`⌊-x⌋ = -⌊x⌋` if `x` is an integer.
+`⌊-x⌋ = -⌊x⌋ - 1` otherwise.
+-/
+theorem exercise_4b (x : ℝ)
+  : (Real.isInt x → ⌊-x⌋ = -⌊x⌋)
+  ∨ (¬Real.isInt x → ⌊-x⌋ = -⌊x⌋ - 1) := by
+  sorry
+
+/-- ### Exercise 4c
+
+`⌊x + y⌋ = ⌊x⌋ + ⌊y⌋` or `⌊x⌋ + ⌊y⌋ + 1`.
+-/
+theorem exercise_4c (x y : ℝ)
+  : ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ ∨ ⌊x + y⌋ = ⌊x⌋ + ⌊y⌋ + 1 := by
+  sorry
+
+/-- ### Exercise 4d
+
+`⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋`
+-/
+theorem exercise_4d (x : ℝ)
+  : ⌊2 * x⌋ = ⌊x⌋ + ⌊x + 1/2⌋ := by
+  sorry
+
+/-- ### Exercise 4e
+
+`⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋`
+-/
+theorem exercise_4e (x : ℝ)
+  : ⌊3 * x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋ := by
+  sorry
+
+/-- ### Exercise 5
+
+The formulas in Exercises 4(d) and 4(e) suggest a generalization for `⌊nx⌋`.
+State and prove such a generalization.
+-/
+theorem exercise_5 (n : ℕ) (x : ℝ)
+  : ⌊n * x⌋ = 10 := by
+  sorry
+
+/-- ### Exercise 7b
+
+If `a` and `b` are positive integers with no common factor, we have the formula
+`Σ_{n=1}^{b-1} ⌊na / b⌋ = ((a - 1)(b - 1)) / 2`. When `b = 1`, the sum on the
+left is understood to be `0`.
+
+Derive the result analytically as follows: By changing the index of summation,
+note that `Σ_{n=1}^{b-1} ⌊na / b⌋ = Σ_{n=1}^{b-1} ⌊a(b - n) / b⌋`. Now apply
+Exercises 4(a) and (b) to the bracket on the right.
+-/
+theorem exercise_7b : True := sorry
+
+end Exercises.Apostol.Exercises_1_11

Exercises/Apostol/Chapter_1_11.tex

@@ -0,0 +1,163 @@
+\documentclass{article}
+\usepackage{amsmath}
+\usepackage[shortlabels]{enumitem}
+
+\input{../../preamble}
+
+\newcommand{\link}[1]{\lean{../..}
+  {Exercises/Apostol/Exercises\_1\_11}
+  {Exercises.Apostol.Exercises\_1\_11.#1}
+  {Exercises\_1\_11.#1}
+}
+
+\begin{document}
+
+\section{Exercise 4}%
+\label{sec:exercise-4}
+
+Prove that the greatest-integer function has the properties indicated:
+
+\subsection{Exercise 4a}%
+\label{sub:exercise-4a}
+
+$\floor{x + n} = \floor{x} + n$ for every integer $n$.
+
+\begin{proof}
+
+  \link{exercise\_4a}
+
+\end{proof}
+
+\subsection{Exercise 4b}%
+\label{sub:exercise-4b}
+
+$\floor{-x} =
+  \begin{cases}
+    -\floor{x} & \text{if } x \text{ is an integer}, \\
+    -\floor{x} - 1 & \text{otherwise}.
+  \end{cases}$
+
+\begin{proof}
+
+  \link{exercise\_4b}
+
+\end{proof}
+
+\subsection{Exercise 4c}%
+\label{sub:exercise-4c}
+
+$\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$.
+
+\begin{proof}
+
+  \link{exercise\_4c}
+
+\end{proof}
+
+\subsection{Exercise 4d}%
+\label{sub:exercise-4d}
+
+$\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$
+
+\begin{proof}
+
+  \link{exercise\_4d}
+
+\end{proof}
+
+\subsection{Exercise 4e}%
+\label{sub:exercise-4e}
+
+$\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$
+
+\begin{proof}
+
+  \link{exercise\_4e}
+
+\end{proof}
+
+\section{Exercise 5}%
+\label{sec:exercise-5}
+
+The formulas in Exercises 4(d) and 4(e) suggest a generalization for
+  $\floor{nx}$.
+State and prove such a generalization.
+
+\begin{proof}
+
+  \link{exercise\_5}
+
+\end{proof}
+
+\section{Exercise 6}%
+\label{sec:exercise-6}
+
+Recall that a lattice point $(x, y)$ in the plane is one whose coordinates are
+  integers.
+Let $f$ be a nonnegative function whose domain is the interval $[a, b]$, where
+  $a$ and $b$ are integers, $a < b$.
+Let $S$ denote the set of points $(x, y)$ satisfying $a \leq x \leq b$,
+  $0 < y \leq f(x)$.
+Prove that the number of lattice points in $S$ is equal to the sum
+  $$\sum_{n=a}^b \floor{f(n)}.$$
+
+\begin{proof}
+
+  TODO
+
+\end{proof}
+
+\section{Exercise 7}%
+\label{sec:exercise-7}
+
+If $a$ and $b$ are positive integers with no common factor, we have the formula
+  $$\sum_{n=1}^{b-1} \floor{\frac{na}{b}} = \frac{(a - 1)(b - 1)}{2}.$$
+When $b = 1$, the sum on the left is understood to be $0$.
+
+\subsection{Exercise 7a}%
+\label{sub:exercise-7a}
+
+Derive this result by a geometric argument, counting lattice points in a right
+  triangle.
+
+\begin{proof}
+
+  TODO
+
+\end{proof}
+
+\subsection{Exercise 7b}%
+\label{sub:exercise-7b}
+
+Derive the result analytically as follows:
+By changing the index of summation, note that
+  $\sum_{n=1}^{b-1} \floor{na / b} = \sum_{n=1}^{b-1} \floor{a(b - n) / b}$.
+Now apply Exercises 4(a) and (b) to the bracket on the right.
+
+\begin{proof}
+
+  TODO
+
+\end{proof}
+
+\section{Exercise 8}%
+\label{sec:exercise-8}
+
+Let $S$ be a set of points on the real line.
+The \textit{characteristic function} of $S$ is, by definition, the function
+  $\chi_S$ such that $\chi_S(x) = 1$ for every $x$ in $S$, and $\chi_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]$.
+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\chi_{I_k}(x).$$
+This property is described by saying that every step function is a linear
+  combination of characteristic functions of intervals.
+
+\begin{proof}
+
+  TODO
+
+\end{proof}
+
+\end{document}

Exercises/Apostol/Chapter_I_03.lean

@@ -10,8 +10,6 @@ namespace Exercises.Apostol.Chapter_I_3
 #check Archimedean
 #check Real.exists_isLUB
 
-namespace Real
-
 /-! ## The least-upper-bound axiom (completeness axiom) -/
 
 /--
@@ -464,7 +462,7 @@ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ)
     intro x hx
     exact p s hs x hx
   have ⟨S_lub, hS_lub⟩ := Real.exists_isLUB S hS ⟨t, ps⟩
-  have ⟨T_glb, hT_glb⟩ := Real.exists_isGLB T hT ⟨s, pt⟩
+  have ⟨T_glb, hT_glb⟩ := exists_isGLB T hT ⟨s, pt⟩
   refine ⟨S_lub, ⟨hS_lub, ⟨T_glb, ⟨hT_glb, ?_⟩⟩⟩⟩
   -- Assume `T_glb < S_lub`. Then `∃ c, T_glb + c < S_lub` which in turn implies
   -- existence of some `x ∈ S` such that `T_glb < S_lub - c / 2 < x < S_lub`.
@@ -489,8 +487,6 @@ theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ)
     _ < x := hx.right
   simp at this
 
-end Real
-
 /-! ## Exercises -/
 
 /-- #### Exercise 1
@@ -498,7 +494,7 @@ end Real
 If `x` and `y` are arbitrary real numbers with `x < y`, prove that there is at
 least one real `z` satisfying `x < z < y`.
 -/
-theorem exercise1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
+theorem exercise_1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
   have ⟨z, hz⟩ := exists_pos_add_of_lt' h
   refine ⟨x + z / 2, ⟨?_, ?_⟩⟩
   · have hz' : z / 2 > 0 := by
@@ -515,15 +511,15 @@ theorem exercise1 (x y : ℝ) (h : x < y) : ∃ z, x < z ∧ z < y := by
 If `x` is an arbitrary real number, prove that there are integers `m` and `n`
 such that `m < x < n`.
 -/
-theorem exercise2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
+theorem exercise_2 (x : ℝ) : ∃ m n : ℝ, m < x ∧ x < n := by
   refine ⟨x - 1, ⟨x + 1, ⟨?_, ?_⟩⟩⟩ <;> norm_num
 
 /-- #### Exercise 3
 
 If `x > 0`, prove that there is a positive integer `n` such that `1 / n < x`.
 -/
-theorem exercise3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
-  have ⟨n, hn⟩ := @Real.exists_pnat_mul_self_geq_of_pos x 1 h
+theorem exercise_3 (x : ℝ) (h : x > 0) : ∃ n : ℕ+, 1 / n < x := by
+  have ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos x 1 h
   refine ⟨n, ?_⟩
   have hr := mul_lt_mul_of_pos_right hn (show 0 < 1 / ↑↑n by norm_num)
   conv at hr => arg 2; rw [mul_comm, ← mul_assoc]; simp
@@ -536,7 +532,7 @@ which satisfies the inequalities `n ≤ x < n + 1`. This `n` is called the
 greatest integer in `x` and is denoted by `⌊x⌋`. For example, `⌊5⌋ = 5`,
 `⌊5 / 2⌋ = 2`, `⌊-8/3⌋ = -3`.
 -/
-theorem exercise4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
+theorem exercise_4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
   let n := Int.floor x
   refine ⟨n, ⟨?_, ?_⟩⟩
   · exact ⟨Int.floor_le x, Int.lt_floor_add_one x⟩
@@ -549,7 +545,7 @@ theorem exercise4 (x : ℝ) : ∃! n : ℤ, n ≤ x ∧ x < n + 1 := by
 If `x` is an arbitrary real number, prove that there is exactly one integer `n`
 which satisfies `x ≤ n < x + 1`.
 -/
-theorem exercise5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
+theorem exercise_5 (x : ℝ) : ∃! n : ℤ, x ≤ n ∧ n < x + 1 := by
   let n := Int.ceil x
   refine ⟨n, ⟨?_, ?_⟩⟩
   · exact ⟨Int.le_ceil x, Int.ceil_lt_add_one x⟩

Exercises/Apostol/Chapter_I_03.tex

@@ -4,9 +4,9 @@
 \input{../../preamble}
 
 \newcommand{\link}[1]{\lean{../..}
-  {Exercises/Apostol/Chapter\_I\_3}
-  {Exercises.Apostol.Chapter\_I\_3.Real.#1}
-  {Chapter\_I\_3.Real.#1}
+  {Bookshelf/Apostol/Chapter\_I\_3}
+  {Apostol.Chapter\_I\_3.#1}
+  {Chapter\_I\_3.#1}
 }
 
 \begin{document}

preamble.tex

@@ -10,6 +10,8 @@
 
 \hypersetup{colorlinks=true, urlcolor=blue}
 
+\newcommand{\ceil}[1]{\left\lceil#1\right\rceil}
+\newcommand{\floor}[1]{\left\lfloor#1\right\rfloor}
 % The first argument refers to a relative path upward from a current file to
 % the root of the workspace (i.e. where this `preamble.tex` file is located).
 \newcommand{\lean}[4]{\href{#1/#2.html\##3}{#4}}