From 3d0dc2b926d9e8a56a10810f3c3dcefd518afdd4 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Thu, 11 May 2023 13:35:05 -0600 Subject: [PATCH] Continuing working on Apostol 1.11 exercises. --- Bookshelf/Apostol/Chapter_1_07.tex | 17 +- Bookshelf/Apostol/Chapter_1_11.lean | 50 ++---- Bookshelf/Apostol/Chapter_1_11.tex | 241 ++++++++++++++++++++++++++-- Common/Real/Floor.lean | 149 +++++++++++++++++ DocGen4/Output/Index.lean | 6 +- preamble.tex | 2 +- 6 files changed, 393 insertions(+), 72 deletions(-) create mode 100644 Common/Real/Floor.lean diff --git a/Bookshelf/Apostol/Chapter_1_07.tex b/Bookshelf/Apostol/Chapter_1_07.tex index fb539e3..6a02590 100644 --- a/Bookshelf/Apostol/Chapter_1_07.tex +++ b/Bookshelf/Apostol/Chapter_1_07.tex @@ -22,7 +22,7 @@ The properties of area in this set of exercises are to be deduced from the Prove that each of the following sets is measurable and has zero area: -\subsection*{\proceeding{Exercise 1a}}% +\subsection*{\unverified{Exercise 1a}}% \label{sub:exercise-1a} A set consisting of a single point. @@ -38,7 +38,7 @@ A set consisting of a single point. \end{proof} -\subsection*{\proceeding{Exercise 1b}}% +\subsection*{\unverified{Exercise 1b}}% \label{sub:exercise-1b} A set consisting of a finite number of points in a plane. @@ -97,7 +97,7 @@ A set consisting of a finite number of points in a plane. \end{proof} -\subsection*{\proceeding{Exercise 1c}}% +\subsection*{\unverified{Exercise 1c}}% \label{sub:exercise-1c} The union of a finite collection of line segments in a plane. @@ -382,24 +382,19 @@ Prove that the formula is valid for right triangles and parallelograms. Likewise, \begin{equation} \label{sub:exercise-4b-eq2} - I_T = \frac{1}{2}(I_R - H_L + 2). + I_T = \frac{1}{2}(I_R - (H_L - 2)). \end{equation} The following shows the lattice point area formula is in agreement with the expected result: \begin{align*} I_T + \frac{1}{2}B_T - 1 - & = \frac{1}{2}(I_R - H_L + 2) + \frac{1}{2}B_T - 1 + & = \frac{1}{2}(I_R - (H_L - 2)) + \frac{1}{2}B_T - 1 & \eqref{sub:exercise-4b-eq2} \\ - & = \frac{1}{2}\left[ I_R - H_L + 2 + B_T - 2 \right] \\ & = \frac{1}{2}\left[ I_R - H_L + B_T \right] \\ & = \frac{1}{2}\left[ I_R - H_L + \frac{1}{2}B_R - 1 + H_L \right] & \eqref{sub:exercise-4b-eq1} \\ & = \frac{1}{2}\left[ I_R + \frac{1}{2}B_R - 1 \right] \\ - & = \frac{1}{2}\left[ (w - 1)(h - 1) + \frac{1}{2}(2(w + h)) - 1 \right] - & \text{\nameref{sub:exercise-4a}} \\ - & = \frac{1}{2}\left[ (w - 1)(h - 1) + w + h - 1 \right] \\ - & = \frac{1}{2}\left[ wh - w - h + 1 + w + h - 1 \right] \\ - & = \frac{wh}{2}. + & = \frac{1}{2}\left[ wh \right] & \text{\nameref{sub:exercise-4a}}. \end{align*} We do not prove this formula is valid for parallelograms here. diff --git a/Bookshelf/Apostol/Chapter_1_11.lean b/Bookshelf/Apostol/Chapter_1_11.lean index 7abedde..6f0d62e 100644 --- a/Bookshelf/Apostol/Chapter_1_11.lean +++ b/Bookshelf/Apostol/Chapter_1_11.lean @@ -1,12 +1,14 @@ -import Mathlib.Algebra.BigOperators.Basic import Mathlib.Data.Real.Basic -import Mathlib.Data.Finset.Basic import Mathlib.Tactic.LibrarySearch +import Common.Real.Floor + /-! # Apostol.Chapter_1_11 -/ namespace Apostol.Chapter_1_11 +open BigOperators + /-! ## Exercise 4 Prove that the greatest-integer function has the properties indicated. @@ -76,49 +78,14 @@ 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) -namespace Hermite - -/-- -Constructs a partition of `[0, 1)` that looks as follows: -``` -[0, 1/n), [1/n, 2/n), ..., [(n-1)/n, 1) -``` --/ -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 - -/-- -The fractional portion of any real number is always in `[0, 1)`. --/ -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 : ℝ) - : ⌊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 + : ⌊n * x⌋ = Finset.sum (Finset.range n) (fun i => ⌊x + i/n⌋) := + Real.Floor.floor_mul_eq_sum_range_floor_add_index_div n x /-- ### Exercise 4d @@ -157,6 +124,9 @@ 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 +theorem exercise_7b (ha : a > 0) (hb : b > 0) (hp : Nat.coprime a b) + : ∑ n in (Finset.range b).filter (· > 0), ⌊n * ((a : ℕ) : ℝ) / b⌋ = + ((a - 1) * (b - 1)) / 2 := by + sorry end Apostol.Chapter_1_11 diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex index dc8cff4..2823511 100644 --- a/Bookshelf/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -2,6 +2,8 @@ \input{../../preamble} +\externaldocument[C:1:07:]{Chapter_1_07}[Chapter_1_07.pdf] + \newcommand{\lean}[1]{\leanref {./Chapter\_1\_11.html\#Apostol.Chapter\_1\_11.#1} {Apostol.Chapter\_1\_11.#1}} @@ -15,7 +17,7 @@ Prove that the greatest-integer function has the properties indicated: -\subsection*{\proceeding{Exercise 4a}}% +\subsection*{\verified{Exercise 4a}}% \label{sub:exercise-4a} $\floor{x + n} = \floor{x} + n$ for every integer $n$. @@ -24,9 +26,19 @@ $\floor{x + n} = \floor{x} + n$ for every integer $n$. \lean{exercise\_4a} + \divider + + Let $x$ be a real number and $n$ an integer. + Let $m = \floor{x + n}$. + By definition of the floor function, $m$ is the unique integer such that + $m \leq x + n < m + 1$. + Then $m - n \leq x < (m - n) + 1$. + That is, $m - n = \floor{x}$. + Rearranging terms we see that $m = \floor{x} + n$ as expected. + \end{proof} -\subsection*{\proceeding{Exercise 4b}}% +\subsection*{\verified{Exercise 4b}}% \label{sub:exercise-4b} $\floor{-x} = @@ -37,16 +49,45 @@ $\floor{-x} = \begin{proof} - \ % Force space prior to *Proof.* + \ \vspace{6pt} - \begin{enumerate}[(a)] - \item \lean{exercise\_4b\_1} - \item \lean{exercise\_4b\_2} - \end{enumerate} + \lean{exercise\_4b\_1} + + \lean{exercise\_4b\_2} + + \divider + + There are two cases to consider: + + \paragraph{Case 1}% + + Suppose $x$ is an integer. + Then $x = \floor{x}$ and $-x = \floor{-x}$. + It immediately follows that $$\floor{-x} = -x = -\floor{x}.$$ + + \paragraph{Case 2}% + + Suppose $x$ is not an integer. + Let $m = \floor{-x}$. + By definition of the floor function, $m$ is the unique integer such that + $m \leq -x < m + 1$. + Equivalently, $-m - 1 < x \leq -m$. + Since $x$ is not an integer, it follows $-m - 1 \leq x < -m$. + Then, by definition of the floor function, $\floor{x} = -m - 1$. + Solving for $m$ yields $$\floor{-x} = m = -\floor{x} - 1.$$ + + \paragraph{Conclusion}% + + The above two cases are exhaustive. Thus + $$\floor{-x} = + \begin{cases} + -\floor{x} & \text{if } x \text{ is an integer}, \\ + -\floor{x} - 1 & \text{otherwise}. + \end{cases}$$ \end{proof} -\subsection*{\proceeding{Exercise 4c}}% +\subsection*{\verified{Exercise 4c}}% \label{sub:exercise-4c} $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$. @@ -55,6 +96,40 @@ $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$. \lean{exercise\_4c} + \divider + + Rewrite $x$ and $y$ as the sum of their floor and fractional components: + $x = \floor{x} + \{x\}$ and $y = \floor{y} + \{y\}$. + Now + \begin{align} + \floor{x + y} + & = \floor{\floor{x} + \{x\} + \floor{y} + \{y\}} \nonumber \\ + & = \floor{\floor{x} + \floor{y} + \{x\} + \{y\}} \nonumber \\ + & = \floor{x} + \floor{y} + \floor{\{x\} + \{y\}} + & \text{\nameref{sub:exercise-4a}} \label{sub:exercise-4c-eq1} + \end{align} + There are two cases to consider: + + \paragraph{Case 1}% + + Suppose $\{x\} + \{y\} < 1$. + Then $\floor{\{x\} + \{y\}} = 0$. + Substituting this value into \eqref{sub:exercise-4c-eq1} yields + $$\floor{x + y} = \floor{x} + \floor{y}.$$ + + \paragraph{Case 2}% + + Suppose $\{x\} + \{y\} \geq 1$. + Because $\{x\}$ and $\{y\}$ are both less than $1$, $\{x\} + \{y\} < 2$. + Thus $\floor{\{x\} + \{y\}} = 1$. + Substituting this value into \eqref{sub:exercise-4c-eq1} yields + $$\floor{x + y} = \floor{x} + \floor{y} + 1.$$ + + \paragraph{Conclusion}% + + Since the above two cases are exhaustive, it follows + $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$. + \end{proof} \subsection*{\proceeding{Exercise 4d}}% @@ -66,6 +141,11 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$ \lean{exercise\_4d} + \divider + + This is immediately proven by applying Hermite's Identity as shown in + \nameref{sec:exercise-5}. + \end{proof} \subsection*{\proceeding{Exercise 4e}}% @@ -77,6 +157,11 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$ \lean{exercise\_4e} + \divider + + This is immediately proven by applying Hermite's Identity as shown in + \nameref{sec:exercise-5}. + \end{proof} \section*{\proceeding{Exercise 5}}% @@ -116,7 +201,7 @@ State and prove such a generalization. \paragraph{Left-Hand Side}% - Consider the left-hande side of identity \eqref{sec:exercise-5-eq1} + Consider the left-hand 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 @@ -182,13 +267,32 @@ Prove that the number of lattice points in $S$ is equal to the sum \begin{proof} - 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)}.$$ + Let $i = a, \ldots, b$ and define $S_i = \mathbb{N} \cap \ioc{0}{f(i)}$. + By construction, the number of lattice points in $S$ is + \begin{equation} + \label{sec:exercise-6-eq1} + \sum_{n = a}^b \abs{S_n}. + \end{equation} + All that remains is to show $\abs{S_i} = \floor{f(i)}$. + There are two cases to consider: + + \paragraph{Case 1}% + + Suppose $f(i)$ is an integer. + Then the number of integers in $\ioc{0}{f(i)}$ is $f(i) = \floor{f(i)}$. + + \paragraph{Case 2}% + + Suppose $f(i)$ is not an integer. + Then the number of integers in $\ioc{0}{f(i)}$ is the same as that of + $\ioc{0}{\floor{f(i)}}$. + Once again, that number is $\floor{f(i)}$. + + \paragraph{Conclusion}% + + By cases 1 and 2, $\abs{S_i} = \floor{f(i)}$. + Substituting this identity into \eqref{sec:exercise-6-eq1} finishes the + proof. \end{proof} @@ -199,6 +303,9 @@ 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$. +\note{When $b = 1$, the proofs of (a) and (b) are trivial. We continue under the + assumption $b > 1$.} + \subsection*{\unverified{Exercise 7a}}% \label{sub:exercise-7a} @@ -207,7 +314,78 @@ Derive this result by a geometric argument, counting lattice points in a right \begin{proof} - TODO + Let $f \colon [1, b - 1] \rightarrow \mathbb{R}$ be given by $f(x) = ax / b$. + Let $S$ denote the set of points $(x, y)$ satisfying $1 \leq x \leq b - 1$, + $0 < y \leq f(x)$. + By \nameref{sec:exercise-6}, the number of lattice points of $S$ is equal to + the sum + \begin{equation} + \label{sub:exercise-7a-eq1} + \sum_{n=1}^{b-1} \floor{f(n)} = \sum_{n=1}^{b-1} \floor{\frac{na}{b}}. + \end{equation} + Define $T$ to be the triangle of width $w = b$ and height $h = f(b) = a$ + as $$T = \{ (x, y) : 0 < x < b, 0 < y \leq f(x) \}.$$ + By construction, $T$ does not introduce any additional lattice points. + Thus $S$ and $T$ have the same number of lattice points. + Let $H_L$ denote the number of boundary points on $T$'s hypotenuse. + We prove that (i) $H_L = 2$ and (ii) that $T$ has $\frac{(a - 1)(b - 1)}{2}$ + lattice points. + + \paragraph{(i)}% + \label{par:exercise-7a-i} + + Consider the line $L$ overlapping the hypotenuse of $T$. + By construction, $T$'s hypotenuse has endpoints $(0, 0)$ and $(b, a)$. + By hypothesis, $a$ and $b$ are positive, excluding the possibility of $L$ + being vertical. + Define the slope of $L$ as $$m = \frac{a}{b}.$$ + $H_L$ coincides with the number of indices $i = 0, \ldots, b$ such that + $(i, i * m)$ is a lattice point. + But $a$ and $b$ are coprime by hypothesis and $i \leq b$. + Thus $i * m$ is an integer if and only if $i = 0$ or $i = b$. + Thus $H_L = 2$. + + \paragraph{(ii)}% + + Next we count the number of lattice points in $T$. + Let $R$ be the overlapping retangle of width $w$ and height $h$, situated + with bottom-left corner at $(0, 0)$. + Let $I_R$ denote the number of interior lattice points of $R$. + Let $I_T$ and $B_T$ denote the interior and boundary lattice points of $T$ + respectively. + By \nameref{C:1:07:sub:exercise-4b-eq2}, + \begin{align} + I_T + & = \frac{1}{2}(I_R - (H_L - 2)) \nonumber \\ + & = \frac{1}{2}(I_R - (2 - 2)) + & \text{\nameref{par:exercise-7a-i}} \nonumber \\ + & = \frac{1}{2}I_R. & \label{sub:exercise-7a-eq2} + \end{align} + Furthermore, since both the adjacent and opposite side of $T$ are not + included in $T$ and there exist no lattice points on $T$'s hypotenuse + besides the endpoints, it follows + \begin{equation} + \label{sub:exercise-7a-eq3} + B_T = 0. + \end{equation} + Thus the number of lattice points of $T$ equals + \begin{align} + I_T + B_T + & = I_T & \eqref{sub:exercise-7a-eq3} \nonumber \\ + & = \frac{1}{2}I_R & \eqref{sub:exercise-7a-eq2} \nonumber \\ + & = \frac{(b - 1)(a - 1)}{2}. + & \text{\nameref{C:1:07:sub:exercise-4a}} + \label{sub:exercise-7a-eq4} + \end{align} + + \paragraph{Conclusion}% + + By \eqref{sub:exercise-7a-eq1} the number of lattice points of $S$ is equal + to the sum $$\sum_{n=1}^{b-1} \floor{\frac{na}{b}}.$$ + But the number of lattice points of $S$ is the same as that of $T$. + By \eqref{sub:exercise-7a-eq4}, the number of lattice points in $T$ is equal + to $$\frac{(b - 1)(a - 1)}{2}.$$ + Thus $$\sum_{n=1}^{b-1} \floor{\frac{na}{b}} = \frac{(a - 1)(b - 1)}{2}.$$ \end{proof} @@ -223,6 +401,35 @@ Now apply Exercises 4(a) and (b) to the bracket on the right. \lean{exercise\_7b} + \divider + + Let $n = 1, \ldots, b - 1$. + By hypothesis, $a$ and $b$ are coprime. + Furthermore, $n < b$ for all values of $n$. + Thus $an / b$ is not an integer. + By \nameref{sub:exercise-4b}, + \begin{equation} + \label{sub:exercise-7b-eq1} + \floor{-\frac{an}{b}} = -\floor{\frac{an}{b}} - 1. + \end{equation} + Consider the following: + \begin{align*} + \sum_{n=1}^{b-1} \floor{\frac{na}{b}} + & = \sum_{n=1}^{b-1} \floor{\frac{a(b - n)}{b}} \\ + & = \sum_{n=1}^{b-1} \floor{\frac{ab - an}{b}} \\ + & = \sum_{n=1}^{b-1} \floor{-\frac{an}{b} + a} \\ + & = \sum_{n=1}^{b-1} \floor{-\frac{an}{b}} + a. + & \text{\nameref{sub:exercise-4a}} \\ + & = \sum_{n=1}^{b-1} -\floor{\frac{an}{b}} - 1 + a + & \eqref{sub:exercise-7b-eq1} \\ + & = -\sum_{n=1}^{b-1} \floor{\frac{an}{b}} - \sum_{n=1}^{b-1} 1 + + \sum_{n=1}^{b-1} a \\ + & = -\sum_{n=1}^{b-1} \floor{\frac{an}{b}} - (b - 1) + a(b - 1). + \end{align*} + Rearranging the above yields + $$2\sum_{n=1}^{b-1} \floor{\frac{an}{b}} = (a - 1)(b - 1).$$ + Dividing both sides of the above identity concludes the proof. + \end{proof} \section*{\unverified{Exercise 8}}% diff --git a/Common/Real/Floor.lean b/Common/Real/Floor.lean new file mode 100644 index 0000000..f271657 --- /dev/null +++ b/Common/Real/Floor.lean @@ -0,0 +1,149 @@ +import Mathlib.Algebra.BigOperators.Basic +import Mathlib.Data.Real.Basic +import Mathlib.Data.Finset.Basic +import Mathlib.Tactic.LibrarySearch + +/-! # Common.Real.Floor + +A collection of useful definitions and theorems around the floor function. +-/ + +namespace Real.Floor + +/-- +The fractional portion of any real number is always in `[0, 1)`. +-/ +theorem fract_mem_Ico_zero_one (x : ℝ) + : Int.fract x ∈ Set.Ico 0 1 := + ⟨Int.fract_nonneg x, Int.fract_lt_one x⟩ + +/-! ## Hermite's Identity + +Definitions and theorems in support of proving Hermite's identity. +-/ + +namespace Hermite + +/-- +A partition of `[0, 1)` that looks as follows: + +``` +[0, 1/n), [1/n, 2/n), ..., [(n-1)/n, 1) +``` + +This is expected to be used as an indexing function of a union of sets, e.g. +`⋃ i ∈ Finset.range n, partition n i`. +-/ +def partition (n : ℕ) (i : ℕ) : Set ℝ := Set.Ico (↑i / n) ((↑i + 1) / n) + +/-- +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 : ℕ, + j < n ∧ r ∈ Set.Ico (((j : ℕ) : ℝ) / n) ((↑j + 1) / n) := by + sorry + +/-- +The indexed union of the family of sets of a `partition` is a subset of `[0, 1)`. +-/ +theorem partition_subset_Ico_zero_one + : (⋃ i ∈ Finset.range n, partition n i) ⊆ Set.Ico 0 1 := by + simp only [ + Finset.mem_range, + gt_iff_lt, + zero_lt_one, + not_true, + ge_iff_le, + Set.unionᵢ_subset_iff + ] + intro i hi x hx + have hn : (0 : ℝ) < n := calc (0 : ℝ) + _ ≤ i := Nat.cast_nonneg i + _ < n := Nat.cast_lt.mpr hi + apply And.intro + · have h_zero_le_i_div_n : (0 : ℝ) ≤ i / n := by + rw [← mul_le_mul_right hn, zero_mul, div_mul, div_self, div_one] + · exact Nat.cast_nonneg i + · exact ne_iff_lt_or_gt.mpr (Or.inr hn) + calc (0 : ℝ) + _ ≤ i / n := h_zero_le_i_div_n + _ ≤ x := hx.left + · have h_succ_div_n_le_one : (i + 1) / n ≤ (1 : ℝ) := by + rw [div_le_one_iff] + refine Or.inl ?_ + exact ⟨hn, by norm_cast⟩ + calc x + _ < (i + 1) / n := hx.right + _ ≤ 1 := h_succ_div_n_le_one + +/-- +`[0, 1)` is a subset of the indexed union of the family of sets of a `partition`. +-/ +theorem Ico_zero_one_subset_partition + : Set.Ico 0 1 ⊆ (⋃ i ∈ Finset.range n, partition n i) := by + intro x hx + simp only [Finset.mem_range, Set.mem_unionᵢ, exists_prop] + unfold partition + exact fract_mem_partition x hx 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 := + Set.Subset.antisymm_iff.mpr + ⟨partition_subset_Ico_zero_one, Ico_zero_one_subset_partition⟩ + +end Hermite + +open BigOperators + +/-- ### Hermite's Identity + +The following decomposes the floor of a multiplication into a sum of floors. +-/ +theorem floor_mul_eq_sum_range_floor_add_index_div (n : ℕ) (x : ℝ) + : ⌊n * x⌋ = ∑ i in Finset.range n, ⌊x + i / n⌋ := by + let r := Int.fract x + + -- Here we see there exists some `j` such that `r ∈ [j / n, (j + 1) / n]`. + have hx : x = ⌊x⌋ + r := Eq.symm (add_eq_of_eq_sub' rfl) + have ⟨j, ⟨hj, hr⟩⟩ := + Hermite.fract_mem_partition r (fract_mem_Ico_zero_one x) n + + -- With the above definitions established, we now show the left- and + -- right-hand sides of the goal evaluate to the same number. + + have hlhs : ⌊n * x⌋ = n * ⌊x⌋ + j := by + have hn : (0 : ℝ) < n := calc (0 : ℝ) + _ ≤ j := Nat.cast_nonneg j + _ < n := Nat.cast_lt.mpr hj + -- We prove that `nr ∈ [j, j + 1)`. It must then follow `⌊nr⌋ = j`. + have hnr : n * r ∈ Set.Ico ((j : ℕ) : ℝ) (j + 1) := by + apply And.intro + · have := hr.left + rw [← mul_le_mul_right hn, div_mul, div_self, div_one] at this + · rwa [mul_comm] + · exact ne_of_gt hn + · have := hr.right + rw [← mul_lt_mul_right hn, div_mul, div_self, div_one] at this + · rwa [mul_comm] + · exact ne_of_gt hn + have hnr_eq_j : ⌊n * r⌋ = j := by + have := Int.floor_eq_on_Ico' j (n * r) hnr + norm_cast at this + conv => + lhs + rw [hx, mul_add, add_comm] + norm_cast + rw [Int.floor_add_int, hnr_eq_j, add_comm] + + have hrhs : ∑ i in Finset.range n, ⌊x + i / n⌋ = n * ⌊x⌋ + j := by + sorry + + -- Close out goal by showing left- and right-hand side equal a common value. + rw [hlhs, hrhs] + +end Real.Floor \ No newline at end of file diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index c87a68c..5877829 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -37,9 +37,9 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <| status: