From df1537b71a2260680ab2ab2c2e0927420cecee4c Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 8 May 2023 13:18:12 -0600 Subject: [PATCH] Draft up Exercises 1.11. --- Bookshelf/Real.lean | 1 + Bookshelf/Real/Int.lean | 10 ++ Exercises/Apostol.lean | 3 +- .../{Exercises_1_7.tex => Chapter_1_07.tex} | 0 Exercises/Apostol/Chapter_1_11.lean | 75 ++++++++ Exercises/Apostol/Chapter_1_11.tex | 163 ++++++++++++++++++ .../{Chapter_I_3.lean => Chapter_I_03.lean} | 18 +- .../{Chapter_I_3.tex => Chapter_I_03.tex} | 6 +- preamble.tex | 2 + 9 files changed, 263 insertions(+), 15 deletions(-) create mode 100644 Bookshelf/Real/Int.lean rename Exercises/Apostol/{Exercises_1_7.tex => Chapter_1_07.tex} (100%) create mode 100644 Exercises/Apostol/Chapter_1_11.lean create mode 100644 Exercises/Apostol/Chapter_1_11.tex rename Exercises/Apostol/{Chapter_I_3.lean => Chapter_I_03.lean} (97%) rename Exercises/Apostol/{Chapter_I_3.tex => Chapter_I_03.tex} (96%) diff --git a/Bookshelf/Real.lean b/Bookshelf/Real.lean index b9ab721..fb2bc18 100644 --- a/Bookshelf/Real.lean +++ b/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 diff --git a/Bookshelf/Real/Int.lean b/Bookshelf/Real/Int.lean new file mode 100644 index 0000000..44c19db --- /dev/null +++ b/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 \ No newline at end of file diff --git a/Exercises/Apostol.lean b/Exercises/Apostol.lean index d4fda4b..e8d8fc4 100644 --- a/Exercises/Apostol.lean +++ b/Exercises/Apostol.lean @@ -1 +1,2 @@ -import Exercises.Apostol.Chapter_I_3 +import Exercises.Apostol.Chapter_I_03 +import Exercises.Apostol.Chapter_1_11 \ No newline at end of file diff --git a/Exercises/Apostol/Exercises_1_7.tex b/Exercises/Apostol/Chapter_1_07.tex similarity index 100% rename from Exercises/Apostol/Exercises_1_7.tex rename to Exercises/Apostol/Chapter_1_07.tex diff --git a/Exercises/Apostol/Chapter_1_11.lean b/Exercises/Apostol/Chapter_1_11.lean new file mode 100644 index 0000000..61497d9 --- /dev/null +++ b/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 diff --git a/Exercises/Apostol/Chapter_1_11.tex b/Exercises/Apostol/Chapter_1_11.tex new file mode 100644 index 0000000..cb9564d --- /dev/null +++ b/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} diff --git a/Exercises/Apostol/Chapter_I_3.lean b/Exercises/Apostol/Chapter_I_03.lean similarity index 97% rename from Exercises/Apostol/Chapter_I_3.lean rename to Exercises/Apostol/Chapter_I_03.lean index fc5243c..0718498 100644 --- a/Exercises/Apostol/Chapter_I_3.lean +++ b/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⟩ diff --git a/Exercises/Apostol/Chapter_I_3.tex b/Exercises/Apostol/Chapter_I_03.tex similarity index 96% rename from Exercises/Apostol/Chapter_I_3.tex rename to Exercises/Apostol/Chapter_I_03.tex index 1368235..54f16d2 100644 --- a/Exercises/Apostol/Chapter_I_3.tex +++ b/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} diff --git a/preamble.tex b/preamble.tex index 7f6a239..efad4a2 100644 --- a/preamble.tex +++ b/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}}