From cac78666db77a60697da51f65e4889c561867af0 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Mon, 10 Apr 2023 06:56:47 -0600 Subject: [PATCH] I_3_10 Apostol. Also introduced notion of "preamble" to share amongst tex docs. --- common/Common/Sequence/Arithmetic.tex | 11 +----- common/Common/Sequence/Geometric.tex | 11 +----- common/preamble.tex | 12 ++++++ .../Enderton/Chapter0.tex | 11 +----- .../Apostol/Chapter_I_3_10.lean | 38 +++++++++++++++++-- .../Apostol/Chapter_I_3_10.tex | 35 ++++++++++------- 6 files changed, 74 insertions(+), 44 deletions(-) create mode 100644 common/preamble.tex diff --git a/common/Common/Sequence/Arithmetic.tex b/common/Common/Sequence/Arithmetic.tex index 1f8d833..015ead2 100644 --- a/common/Common/Sequence/Arithmetic.tex +++ b/common/Common/Sequence/Arithmetic.tex @@ -1,13 +1,6 @@ \documentclass{article} -\usepackage{amsfonts, amsthm} -\usepackage{hyperref} -\newtheorem{theorem}{Theorem} -\newtheorem{custominner}{Theorem} -\newenvironment{custom}[1]{% - \renewcommand\thecustominner{#1}% - \custominner -}{\endcustominner} +\input{../../preamble} \begin{document} @@ -21,7 +14,7 @@ $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ \begin{proof} -\href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum\_recursive\_closed} +\href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum_recursive_closed} \end{proof} diff --git a/common/Common/Sequence/Geometric.tex b/common/Common/Sequence/Geometric.tex index bfba35a..68182fb 100644 --- a/common/Common/Sequence/Geometric.tex +++ b/common/Common/Sequence/Geometric.tex @@ -1,13 +1,6 @@ \documentclass{article} -\usepackage{amsfonts, amsthm} -\usepackage{hyperref} -\newtheorem{theorem}{Theorem} -\newtheorem{custominner}{Theorem} -\newenvironment{custom}[1]{% - \renewcommand\thecustominner{#1}% - \custominner -}{\endcustominner} +\input{../../preamble} \begin{document} @@ -21,7 +14,7 @@ $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ \begin{proof} -\href{Geometric.lean}{Common.Sequence.Geometric.sum\_recursive\_closed} +\href{Geometric.lean}{Common.Sequence.Geometric.sum_recursive_closed} \end{proof} diff --git a/common/preamble.tex b/common/preamble.tex new file mode 100644 index 0000000..1354b8a --- /dev/null +++ b/common/preamble.tex @@ -0,0 +1,12 @@ +\usepackage{amsfonts, amsthm} +\usepackage{hyperref} +\usepackage{underscore} + +\newtheorem{theorem}{Theorem} +\newtheorem{xtheoreminner}{Theorem} +\newenvironment{xtheorem}[1]{% + \renewcommand\thextheoreminner{#1}% + \xtheoreminner +}{\endxtheoreminner} + +\hypersetup{colorlinks=true, urlcolor=blue} diff --git a/mathematical-introduction-logic/Enderton/Chapter0.tex b/mathematical-introduction-logic/Enderton/Chapter0.tex index 95133b9..b27461a 100644 --- a/mathematical-introduction-logic/Enderton/Chapter0.tex +++ b/mathematical-introduction-logic/Enderton/Chapter0.tex @@ -1,13 +1,6 @@ \documentclass{article} -\usepackage{amsfonts, amsthm} -\usepackage{hyperref} -\newtheorem{theorem}{Theorem} -\newtheorem{custominner}{Theorem} -\newenvironment{custom}[1]{% - \renewcommand\thecustominner{#1}% - \custominner -}{\endcustominner} +\input{../../common/preamble} \begin{document} @@ -20,7 +13,7 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. \begin{proof} -\href{Chapter0.lean}{Enderton.Chapter0.lemma\_0a} +\href{Chapter0.lean}{Enderton.Chapter0.lemma_0a} \end{proof} diff --git a/one-variable-calculus/Apostol/Chapter_I_3_10.lean b/one-variable-calculus/Apostol/Chapter_I_3_10.lean index 37a40f0..0591910 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3_10.lean +++ b/one-variable-calculus/Apostol/Chapter_I_3_10.lean @@ -27,7 +27,7 @@ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by _ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h' /-- -Theorem 1.29 +Theorem I.29 For every real `x` there exists a positive integer `n` such that `n > x`. -/ @@ -40,14 +40,14 @@ theorem exists_pnat_geq_self (x : ℝ) : ∃ n : ℕ+, ↑n > x := by exact ⟨x', h⟩ /-- -Theorem 1.30 +Theorem I.30 If `x > 0` and if `y` is an arbitrary real number, there exists a positive integer `n` such that `nx > y`. This is known as the *Archimedean Property of the Reals*. -/ -theorem pos_imp_exists_pnat_mul_self_geq {x y : ℝ} +theorem exists_pnat_mul_self_geq_of_pos {x y : ℝ} : x > 0 → ∃ n : ℕ+, n * x > y := by intro hx let ⟨n, p⟩ := exists_pnat_geq_self (y / x) @@ -55,4 +55,36 @@ theorem pos_imp_exists_pnat_mul_self_geq {x y : ℝ} rw [div_mul, div_self (show x ≠ 0 from LT.lt.ne' hx), div_one] at p' exact ⟨n, p'⟩ +/-- +Theorem I.31 + +If three real numbers `a`, `x`, and `y` satisfy the inequalities +`a ≤ x ≤ a + y / n` for every integer `n ≥ 1`, then `x = a`. +-/ +theorem forall_pnat_leq_self_leq_frac_iff_eq {x y a : ℝ} + : (∀ n : ℕ+, a ≤ x ∧ x ≤ a + (y / n)) → x = a := by + intro h + match @trichotomous ℝ LT.lt _ x a with + | -- x = a + Or.inr (Or.inl r) => exact r + | -- x < a + Or.inl r => + have z : a < a := lt_of_le_of_lt (h 1).left r + simp at z + | -- x > a + Or.inr (Or.inr r) => + let ⟨c, hc⟩ := exists_pos_add_of_lt' r + let ⟨n, hn⟩ := @exists_pnat_mul_self_geq_of_pos c y hc.left + have hn := mul_lt_mul_of_pos_left hn $ + have hp : 0 < (↑↑n : ℝ) := by simp + show 0 < ((↑↑n)⁻¹ : ℝ) from inv_pos.mpr hp + rw [inv_mul_eq_div, ←mul_assoc, mul_comm (n⁻¹ : ℝ), ←one_div, mul_one_div] at hn + simp at hn + have hn := add_lt_add_left hn a + have := calc a + y / ↑↑n + _ < a + c := hn + _ = x := hc.right + _ ≤ a + y / ↑↑n := (h n).right + simp at this + end Real diff --git a/one-variable-calculus/Apostol/Chapter_I_3_10.tex b/one-variable-calculus/Apostol/Chapter_I_3_10.tex index 7e4c684..3bdeecf 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3_10.tex +++ b/one-variable-calculus/Apostol/Chapter_I_3_10.tex @@ -1,37 +1,44 @@ \documentclass{article} -\usepackage{amsfonts, amsthm} -\usepackage{hyperref} -\newtheorem{theorem}{Theorem} -\newtheorem{custominner}{Theorem} -\newenvironment{custom}[1]{% - \renewcommand\thecustominner{#1}% - \custominner -}{\endcustominner} +\input{../../common/preamble} \begin{document} -\begin{custom}{1.29} +\begin{xtheorem}{1.29} For every real $x$ there exists a positive integer $n$ such that $n > x$. -\end{custom} +\end{xtheorem} \begin{proof} -\href{Chapter_I_3_10.lean}{Apostol.Chapter\_I\_3\_10.Real.exists\_pnat\_geq\_self} +\href{Chapter_I_3_10.lean}{Apostol.Chapter_I_3_10.Real.exists_pnat_geq_self} \end{proof} -\begin{custom}{1.30}[Archimedean Property of the Reals] +\begin{xtheorem}{1.30}[Archimedean Property of the Reals] If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive integer $n$ such that $nx > y$. -\end{custom} +\end{xtheorem} \begin{proof} -\href{Chapter_I_3_10.lean}{Apostol.Chapter\_I\_3\_10.Real.pos\_imp\_exists\_pnat\_mul\_self\_geq} +\href{Chapter_I_3_10.lean}{Apostol.Chapter_I_3_10.Real.exists_pnat_mul_self_geq_of_pos} + +\end{proof} + +\begin{xtheorem}{1.31} + +If three real numbers $a$, $x$, and $y$ satisfy the inequalities +$$a \leq x \leq a + \frac{y}{n}$$ +for every integer $n \geq 1$, then $x = a$. + +\end{xtheorem} + +\begin{proof} + +\href{Chapter_I_3_10.lean}{Apostol.Chapter_I_3_10.Real.forall_pnat_leq_self_leq_frac_iff_eq} \end{proof}