diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean index cc1af60..7abedde 100644 --- a/Bookshelf/Apostol/Chapter_1_11.lean +++ b/Bookshelf/Apostol/Chapter_1_11.lean @@ -1,4 +1,7 @@ +import Mathlib.Algebra.BigOperators.Basic import Mathlib.Data.Real.Basic +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic.LibrarySearch /-! # Apostol.Chapter_1_11 -/ @@ -73,31 +76,77 @@ theorem exercise_4c (x y : ℝ) rw [← sub_lt_iff_lt_add', ← sub_sub, add_sub_cancel, add_sub_cancel] exact add_lt_add (Int.fract_lt_one x) (Int.fract_lt_one y) -/-- ### Exercise 4d +namespace Hermite -`⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋` +/-- +Constructs a partition of `[0, 1)` that looks as follows: +``` +[0, 1/n), [1/n, 2/n), ..., [(n-1)/n, 1) +``` -/ -theorem exercise_4d (x : ℝ) - : ⌊2 * x⌋ = ⌊x⌋ + ⌊x + 1/2⌋ := by +def partition (n : ℕ) (i : ℕ) : Set ℝ := Set.Ico (i / n) ((i + 1) / n) + +/-- +The indexed union of the family of sets of a `partition` is equal to `[0, 1)`. +-/ +theorem partition_eq_Ico_zero_one + : (⋃ i ∈ Finset.range n, partition n i) = Set.Ico 0 1 := by sorry -/-- ### Exercise 4e - -`⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋` +/-- +The fractional portion of any real number is always in `[0, 1)`. -/ -theorem exercise_4e (x : ℝ) - : ⌊3 * x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋ := by +theorem fract_mem_Ico_zero_one (x : ℝ) + : Int.fract x ∈ Set.Ico 0 1 := ⟨Int.fract_nonneg x, Int.fract_lt_one x⟩ + +/-- +The fractional portion of any real number always exists in some member of the +indexed family of sets formed by any `partition`. +-/ +theorem fract_mem_partition (r : ℝ) (hr : r ∈ Set.Ico 0 1) + : ∀ n : ℕ, ∃ j : ℕ, r ∈ Set.Ico ↑(j / n) ↑((j + 1) / n) := by sorry +end Hermite + /-- ### 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 : ℝ) - : True := by + : ⌊n * x⌋ = Finset.sum (Finset.range n) (fun i => ⌊x + i/n⌋) := by + let r := Int.fract x + have hx : x = ⌊x⌋ + r := Eq.symm (add_eq_of_eq_sub' rfl) sorry +/-- ### Exercise 4d + +`⌊2x⌋ = ⌊x⌋ + ⌊x + 1/2⌋` +-/ +theorem exercise_4d (x : ℝ) + : ⌊2 * x⌋ = ⌊x⌋ + ⌊x + 1/2⌋ := by + suffices ⌊x⌋ + ⌊x + 1/2⌋ = Finset.sum (Finset.range 2) (fun i => ⌊x + i/2⌋) by + rw [this] + exact exercise_5 2 x + unfold Finset.sum + simp + rw [add_comm] + +/-- ### Exercise 4e + +`⌊3x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋` +-/ +theorem exercise_4e (x : ℝ) + : ⌊3 * x⌋ = ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋ := by + suffices ⌊x⌋ + ⌊x + 1/3⌋ + ⌊x + 2/3⌋ = Finset.sum (Finset.range 3) (fun i => ⌊x + i/3⌋) by + rw [this] + exact exercise_5 3 x + unfold Finset.sum + simp + conv => rhs; rw [← add_rotate']; arg 2; rw [add_comm] + rw [← add_assoc] + /-- ### Exercise 7b If `a` and `b` are positive integers with no common factor, we have the formula diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex index 88c66a5..593ee86 100644 --- a/Bookshelf/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -1,6 +1,7 @@ \documentclass{article} \usepackage{amsmath} \usepackage[shortlabels]{enumitem} +\usepackage{soul, xcolor} \input{../../preamble} @@ -88,10 +89,94 @@ The formulas in Exercises 4(d) and 4(e) suggest a generalization for $\floor{nx}$. State and prove such a generalization. +\vspace{6pt} +\noindent +\hl{Note}: The stated generalization is known as "Hermite's Identity." + \begin{proof} \link{exercise\_5} + \vspace{6pt} + \hrule + \vspace{6pt} + + We prove that for all natural numbers $n$ and real numbers $x$, the following + identity holds: + \begin{equation} + \label{sec:exercise-5-eq1} + \tag{5.1} + \floor{nx} = \sum_{i=0}^{n-1} \floor{x + \frac{i}{n}} + \end{equation} + By definition of the floor function, $x = \floor{x} + r$ for some + $r \in \ico{0}{1}$. + Define $S$ as the partition of non-overlapping subintervals + $$\ico{0}{\frac{1}{n}}, \ico{\frac{1}{n}}{\frac{2}{n}}, \ldots, + \ico{\frac{n-1}{n}}{1}.$$ + By construction, $\cup\; S = \ico{0}{1}$. + Therefore there exists some $j \in \mathbb{N}$ such that + \begin{equation} + \label{sec:exercise-5-eq2} + \tag{5.2} + r \in \ico{\frac{j}{n}}{\frac{j+1}{n}}. + \end{equation} + With these definitions established, we now show the left- and right-hand sides + of \eqref{sec:exercise-5-eq1} evaluate to the same number. + + \paragraph{Left-Hand Side}% + + Consider the left-hande side of identity \eqref{sec:exercise-5-eq1} + By \eqref{sec:exercise-5-eq2}, $nr \in \ico{j}{j + 1}$. + Therefore $\floor{nr} = j$. + Thus + \begin{align*} + \floor{nx} + & = \floor{n(\floor{x} + r)} \nonumber \\ + & = \floor{n\floor{x} + nr} \nonumber \\ + & = \floor{n\floor{x}} + \floor{nr}. \nonumber + & \eqref{sub:exercise-4a} \\ + & = \floor{n\floor{x}} + j \nonumber \\ + & = n\floor{x} + j. \label{sec:exercise-5-eq3} \tag{5.3} + \end{align*} + + \paragraph{Right-Hand Side}% + + Now consider the right-hand side of identity \eqref{sec:exercise-5-eq1}. + We note each summand, by construction, is the floor of $x$ added to a + nonnegative number less than one. + Therefore each summand contributes either $\floor{x}$ or $\floor{x} + 1$ to + the total. + Letting $z$ denote the number of summands that contribute $\floor{x} + 1$, + we have + \begin{equation} + \label{sec:exercise-5-eq4} + \tag{5.4} + \sum_{i=0}^{n-1} \floor{x + \frac{i}{n}} = n\floor{x} + z. + \end{equation} + The value of $z$ corresponds to the number of indices $i$ that satisfy + $$\frac{i}{n} \geq 1 - r.$$ + By \eqref{sec:exercise-5-eq2}, it follows + \begin{align*} + 1 - r + & \in \ioc{1 - \frac{j+1}{n}}{1-\frac{j}{n}} \\ + & = \ioc{\frac{n - j - 1}{n}}{\frac{n - j}{n}}. + \end{align*} + Thus we can determine the value of $z$ by instead counting the number of + indices $i$ that satisfy $$\frac{i}{n} \geq \frac{n - j}{n}.$$ + Rearranging terms, we see that $i \geq n - j$ holds for + $z = (n - 1) - (n - j) + 1 = j$ of the $n$ summands. + Substituting the value of $z$ into \eqref{sec:exercise-5-eq4} yields + \begin{equation} + \label{sec:exercise-5-eq5} + \tag{5.5} + \sum_{i=0}^{n-1} \floor{x + \frac{i}{n}} = n\floor{x} + j. + \end{equation} + + \paragraph{Conclusion}% + + Since \eqref{sec:exercise-5-eq3} and \eqref{sec:exercise-5-eq5} agree with + one another, it follows identity \eqref{sec:exercise-5-eq1} holds. + \end{proof} \section{Exercise 6}% @@ -108,7 +193,13 @@ Prove that the number of lattice points in $S$ is equal to the sum \begin{proof} - TODO + Define $S_i = \mathbb{Z} \cap \ioc{0}{f(i)}$ for all $i \in \mathbb{Z}$. + By definition, the set of lattice points of $S$ is given by + $$L = \{ (i, j) : i = a, \ldots, b \land j \in S_i \}.$$ + By construction, it follows $$\sum_{j \in S_i} 1 = \floor{f(i)}.$$ + Therefore $$\abs{L} + = \sum_{i=a}^b \sum_{j \in S_i} 1 + = \sum_{i=1}^b \floor{f(i)}.$$ \end{proof} diff --git a/preamble.tex b/preamble.tex index efad4a2..855a02f 100644 --- a/preamble.tex +++ b/preamble.tex @@ -10,8 +10,13 @@ \hypersetup{colorlinks=true, urlcolor=blue} +\newcommand{\abs}[1]{\left|#1\right|} \newcommand{\ceil}[1]{\left\lceil#1\right\rceil} \newcommand{\floor}[1]{\left\lfloor#1\right\rfloor} +\newcommand{\icc}[2]{\left[#1, #2\right]} +\newcommand{\ico}[2]{\left[#1, #2\right)} +\newcommand{\ioc}[2]{\left(#1, #2\right]} +\newcommand{\ioo}[2]{\left(#1, #2\right)} % 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}}