From bec3093d026e6123aa2f97a5d7f29a13e44e8a6d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 11 Apr 2023 06:46:59 -0600 Subject: [PATCH] Apostol I 3. Better organize concepts in `common` and continue adding more to parts of I 3 proofs. --- common/Common.lean | 4 +- .../Real/Sequence.lean} | 89 +++++++++ common/Common/Data/Real/Sequence.tex | 35 ++++ common/Common/Data/Real/Set.lean | 12 ++ common/Common/Sequence/Arithmetic.tex | 21 --- common/Common/Sequence/Geometric.lean | 92 ---------- common/Common/Sequence/Geometric.tex | 21 --- .../Apostol/Chapter_I_3.lean | 169 +++++++++++++++++- one-variable-calculus/Apostol/Chapter_I_3.tex | 45 ++++- 9 files changed, 346 insertions(+), 142 deletions(-) rename common/Common/{Sequence/Arithmetic.lean => Data/Real/Sequence.lean} (61%) create mode 100644 common/Common/Data/Real/Sequence.tex create mode 100644 common/Common/Data/Real/Set.lean delete mode 100644 common/Common/Sequence/Arithmetic.tex delete mode 100644 common/Common/Sequence/Geometric.lean delete mode 100644 common/Common/Sequence/Geometric.tex diff --git a/common/Common.lean b/common/Common.lean index e9ccfee..9058953 100644 --- a/common/Common.lean +++ b/common/Common.lean @@ -1,3 +1,3 @@ -import Common.Sequence.Arithmetic -import Common.Sequence.Geometric +import Common.Data.Real.Set +import Common.Data.Real.Sequence import Common.Tuple diff --git a/common/Common/Sequence/Arithmetic.lean b/common/Common/Data/Real/Sequence.lean similarity index 61% rename from common/Common/Sequence/Arithmetic.lean rename to common/Common/Data/Real/Sequence.lean index c72c9d8..6500bea 100644 --- a/common/Common/Sequence/Arithmetic.lean +++ b/common/Common/Data/Real/Sequence.lean @@ -115,3 +115,92 @@ theorem sum_recursive_closed (seq : Arithmetic) (n : Nat) _ = seq.sum_closed (n + 1) := rfl end Arithmetic + +/-- +A `0th`-indexed geometric sequence. +-/ +structure Geometric where + a₀ : Real + r : Real + +namespace Geometric + +/-- +Returns the value of the `n`th term of a geometric sequence. + +This function calculates the value of this term directly. Keep in mind the +sequence is `0`th-indexed. +-/ +def termClosed (seq : Geometric) (n : Nat) : Real := + seq.a₀ * seq.r ^ n + +/-- +Returns the value of the `n`th term of a geometric sequence. + +This function calculates the value of this term recursively. Keep in mind the +sequence is `0`th-indexed. +-/ +def termRecursive : Geometric → Nat → Real + | seq, 0 => seq.a₀ + | seq, (n + 1) => seq.r * (seq.termRecursive n) + +/-- +The recursive and closed term definitions of a geometric sequence agree with +one another. +-/ +theorem term_recursive_closed (seq : Geometric) (n : Nat) + : seq.termRecursive n = seq.termClosed n := by + induction n with + | zero => unfold termClosed termRecursive; norm_num + | succ n ih => calc + seq.termRecursive (n + 1) + _ = seq.r * (seq.termRecursive n) := rfl + _ = seq.r * (seq.termClosed n) := by rw [ih] + _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl + _ = seq.a₀ * seq.r ^ (n + 1) := by ring + _ = seq.termClosed (n + 1) := rfl + +/-- +The summation of the first `n + 1` terms of a geometric sequence. + +This function calculates the sum directly. +-/ +noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat) + : seq.r ≠ 1 → Real := + fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) + +/-- +The summation of the first `n + 1` terms of a geometric sequence. + +This function calculates the sum recursively. +-/ +def sum_recursive : Geometric → Nat → Real + | seq, 0 => seq.a₀ + | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n + +/-- +The recursive and closed definitions of the sum of a geometric sequence agree +with one another. +-/ +theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1) + : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by + have h : 1 - seq.r ≠ 0 := by + intro h + rw [sub_eq_iff_eq_add, zero_add] at h + exact False.elim (p (Eq.symm h)) + induction n with + | zero => + unfold sum_recursive sum_closed_ratio_neq_one + simp + rw [mul_div_assoc, div_self h, mul_one] + | succ n ih => + calc + sum_recursive seq (n + 1) + _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl + _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih] + _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl + _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h] + _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf + _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl + +end Geometric diff --git a/common/Common/Data/Real/Sequence.tex b/common/Common/Data/Real/Sequence.tex new file mode 100644 index 0000000..fa769b3 --- /dev/null +++ b/common/Common/Data/Real/Sequence.tex @@ -0,0 +1,35 @@ +\documentclass{article} + +\input{../../../preamble} + +\begin{document} + +\begin{theorem}[Sum of Arithmetic Series] + + Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. + Then for some $n \in \mathbb{N}$, + $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ + +\end{theorem} + +\begin{proof} + + \href{Sequence.lean}{Common.Data.Real.Sequence.Arithmetic.sum_recursive_closed} + +\end{proof} + +\begin{theorem}[Sum of Geometric Series] + + Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. + Then for some $n \in \mathbb{N}$, + $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ + +\end{theorem} + +\begin{proof} + + \href{Sequence.lean}{Common.Data.Real.Sequence.Geometric.sum_recursive_closed} + +\end{proof} + +\end{document} diff --git a/common/Common/Data/Real/Set.lean b/common/Common/Data/Real/Set.lean new file mode 100644 index 0000000..614fefd --- /dev/null +++ b/common/Common/Data/Real/Set.lean @@ -0,0 +1,12 @@ +import Mathlib.Data.Real.Basic + +namespace Real + +/-- +The Minkowski sum of two sets `s` and `t` is the set +`s + t = { a + b : a ∈ s, b ∈ t }`. +-/ +def minkowski_sum (s t : Set ℝ) := + { x | ∃ a ∈ s, ∃ b ∈ t, x = a + b } + +end Real diff --git a/common/Common/Sequence/Arithmetic.tex b/common/Common/Sequence/Arithmetic.tex deleted file mode 100644 index 70953bd..0000000 --- a/common/Common/Sequence/Arithmetic.tex +++ /dev/null @@ -1,21 +0,0 @@ -\documentclass{article} - -\input{../../preamble} - -\begin{document} - -\begin{theorem}[Sum of Arithmetic Series] - - Let $(a_i)_{i \geq 0}$ be an arithmetic sequence with common difference $d$. - Then for some $n \in \mathbb{N}$, - $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ - -\end{theorem} - -\begin{proof} - - \href{Arithmetic.lean}{Common.Sequence.Arithmetic.sum_recursive_closed} - -\end{proof} - -\end{document} diff --git a/common/Common/Sequence/Geometric.lean b/common/Common/Sequence/Geometric.lean deleted file mode 100644 index 50276cb..0000000 --- a/common/Common/Sequence/Geometric.lean +++ /dev/null @@ -1,92 +0,0 @@ -import Mathlib.Data.Real.Basic -import Mathlib.Tactic.NormNum -import Mathlib.Tactic.Ring - -/-- -A `0th`-indexed geometric sequence. --/ -structure Geometric where - a₀ : Real - r : Real - -namespace Geometric - -/-- -Returns the value of the `n`th term of a geometric sequence. - -This function calculates the value of this term directly. Keep in mind the -sequence is `0`th-indexed. --/ -def termClosed (seq : Geometric) (n : Nat) : Real := - seq.a₀ * seq.r ^ n - -/-- -Returns the value of the `n`th term of a geometric sequence. - -This function calculates the value of this term recursively. Keep in mind the -sequence is `0`th-indexed. --/ -def termRecursive : Geometric → Nat → Real - | seq, 0 => seq.a₀ - | seq, (n + 1) => seq.r * (seq.termRecursive n) - -/-- -The recursive and closed term definitions of a geometric sequence agree with -one another. --/ -theorem term_recursive_closed (seq : Geometric) (n : Nat) - : seq.termRecursive n = seq.termClosed n := by - induction n with - | zero => unfold termClosed termRecursive; norm_num - | succ n ih => calc - seq.termRecursive (n + 1) - _ = seq.r * (seq.termRecursive n) := rfl - _ = seq.r * (seq.termClosed n) := by rw [ih] - _ = seq.r * (seq.a₀ * seq.r ^ n) := rfl - _ = seq.a₀ * seq.r ^ (n + 1) := by ring - _ = seq.termClosed (n + 1) := rfl - -/-- -The summation of the first `n + 1` terms of a geometric sequence. - -This function calculates the sum directly. --/ -noncomputable def sum_closed_ratio_neq_one (seq : Geometric) (n : Nat) - : seq.r ≠ 1 → Real := - fun _ => (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) - -/-- -The summation of the first `n + 1` terms of a geometric sequence. - -This function calculates the sum recursively. --/ -def sum_recursive : Geometric → Nat → Real - | seq, 0 => seq.a₀ - | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n - -/-- -The recursive and closed definitions of the sum of a geometric sequence agree -with one another. --/ -theorem sum_recursive_closed (seq : Geometric) (n : Nat) (p : seq.r ≠ 1) - : sum_recursive seq n = sum_closed_ratio_neq_one seq n p := by - have h : 1 - seq.r ≠ 0 := by - intro h - rw [sub_eq_iff_eq_add, zero_add] at h - exact False.elim (p (Eq.symm h)) - induction n with - | zero => - unfold sum_recursive sum_closed_ratio_neq_one - simp - rw [mul_div_assoc, div_self h, mul_one] - | succ n ih => - calc - sum_recursive seq (n + 1) - _ = seq.termClosed (n + 1) + seq.sum_recursive n := rfl - _ = seq.termClosed (n + 1) + sum_closed_ratio_neq_one seq n p := by rw [ih] - _ = seq.a₀ * seq.r ^ (n + 1) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := rfl - _ = seq.a₀ * seq.r ^ (n + 1) * (1 - seq.r) / (1 - seq.r) + (seq.a₀ * (1 - seq.r ^ (n + 1))) / (1 - seq.r) := by rw [mul_div_cancel _ h] - _ = (seq.a₀ * (1 - seq.r ^ (n + 1 + 1))) / (1 - seq.r) := by ring_nf - _ = sum_closed_ratio_neq_one seq (n + 1) p := rfl - -end Geometric diff --git a/common/Common/Sequence/Geometric.tex b/common/Common/Sequence/Geometric.tex deleted file mode 100644 index d0ac39b..0000000 --- a/common/Common/Sequence/Geometric.tex +++ /dev/null @@ -1,21 +0,0 @@ -\documentclass{article} - -\input{../../preamble} - -\begin{document} - -\begin{theorem}[Sum of Geometric Series] - - Let $(a_i)_{i \geq 0}$ be a geometric sequence with common ratio $r \neq 1$. - Then for some $n \in \mathbb{N}$, - $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ - -\end{theorem} - -\begin{proof} - - \href{Geometric.lean}{Common.Sequence.Geometric.sum_recursive_closed} - -\end{proof} - -\end{document} diff --git a/one-variable-calculus/Apostol/Chapter_I_3.lean b/one-variable-calculus/Apostol/Chapter_I_3.lean index f836284..8122961 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3.lean +++ b/one-variable-calculus/Apostol/Chapter_I_3.lean @@ -1,4 +1,6 @@ +import Common.Data.Real.Set import Mathlib.Data.Real.Basic +import Mathlib.Data.Set.Basic import Mathlib.Data.Set.Pointwise.Basic import Mathlib.Tactic.LibrarySearch @@ -7,6 +9,10 @@ import Mathlib.Tactic.LibrarySearch namespace Real +-- ======================================== +-- The least-upper-bound axiom (completeness axiom) +-- ======================================== + /-- A property holds for the negation of elements in set `S` if and only if it also holds for the elements of the negation of `S`. @@ -139,6 +145,10 @@ lemma leq_nat_abs_ceil_self (x : ℝ) : x ≤ Int.natAbs ⌈x⌉ := by _ ≤ 0 := le_of_lt (lt_of_not_le h) _ ≤ ↑(Int.natAbs ⌈x⌉) := GE.ge.le h' +-- ======================================== +-- The Archimedean property of the real-number system +-- ======================================== + /-- Theorem I.29 @@ -200,14 +210,75 @@ theorem forall_pnat_leq_self_leq_frac_imp_eq {x y a : ℝ} _ ≤ a + y / ↑↑n := (h n).right simp at this +-- ======================================== +-- Fundamental properties of the supremum and infimum +-- ======================================== + +/-- +Every member of a set `S` is less than or equal to some value `ub` if and only +if `ub` is an upper bound of `S`. +-/ +lemma mem_upper_bounds_iff_forall_le {S : Set ℝ} + : ub ∈ upperBounds S ↔ (∀ x, x ∈ S → x ≤ ub) := by + apply Iff.intro + · intro h _ hx + exact (h hx) + · exact id + +/-- +If a set `S` has a least upper bound, it follows every member of `S` is less +than or equal to that value. +-/ +lemma forall_lub_imp_forall_le {S : Set ℝ} + : IsLUB S ub → (∀ x, x ∈ S → x ≤ ub) := by + intro h + rw [← mem_upper_bounds_iff_forall_le] + exact h.left + /-- Theorem I.32a Let `h` be a given positive number and let `S` be a set of real numbers. If `S` has a supremum, then for some `x` in `S` we have `x > sup S - h`. -/ -theorem arb_close_to_sup (S : Set ℝ) (s h : ℝ) (hp : h > 0) - : IsLUB S s → ∃ x : S, x > s - h := sorry +theorem sup_imp_exists_gt_sup_sub_delta (S : Set ℝ) (s h : ℝ) (hp : h > 0) + : IsLUB S s → ∃ x ∈ S, x > s - h := by + intro hb + -- Suppose all members of our set was less than `s - h`. Then `s` couldn't be + -- the *least* upper bound. + by_contra nb + suffices s - h ∈ upperBounds S by + have h' : h < h := calc h + _ ≤ 0 := (le_sub_self_iff s).mp (hb.right this) + _ < h := hp + simp at h' + rw [not_exists] at nb + have nb' : ∀ x ∈ S, x ≤ s - h := by + intro x hx + exact le_of_not_gt (not_and.mp (nb x) hx) + rw [← mem_upper_bounds_iff_forall_le] at nb' + exact nb' + +/-- +Every member of a set `S` is greater than or equal to some value `lb` if and +only if `lb` is a lower bound of `S`. +-/ +lemma mem_lower_bounds_iff_forall_ge {S : Set ℝ} + : lb ∈ lowerBounds S ↔ (∀ x ∈ S, x ≥ lb) := by + apply Iff.intro + · intro h _ hx + exact (h hx) + · exact id + +/-- +If a set `S` has a greatest lower bound, it follows every member of `S` is +greater than or equal to that value. +-/ +lemma forall_glb_imp_forall_ge {S : Set ℝ} + : IsGLB S lb → (∀ x ∈ S, x ≥ lb) := by + intro h + rw [← mem_lower_bounds_iff_forall_ge] + exact h.left /-- Theorem I.32b @@ -215,7 +286,97 @@ Theorem I.32b Let `h` be a given positive number and let `S` be a set of real numbers. If `S` has an infimum, then for some `x` in `S` we have `x < inf S + h`. -/ -theorem arb_close_to_inf (S : Set ℝ) (s h : ℝ) (hp : h > 0) - : IsGLB S s → ∃ x : S, x < s + h := sorry +theorem inf_imp_exists_lt_inf_add_delta (S : Set ℝ) (s h : ℝ) (hp : h > 0) + : IsGLB S s → ∃ x ∈ S, x < s + h := by + intro hb + -- Suppose all members of our set was greater than `s + h`. Then `s` couldn't + -- be the *greatest* lower bound. + by_contra nb + suffices s + h ∈ lowerBounds S by + have h' : h < h := calc h + _ ≤ 0 := (add_le_iff_nonpos_right s).mp (hb.right this) + _ < h := hp + simp at h' + rw [not_exists] at nb + have nb' : ∀ x ∈ S, x ≥ s + h := by + intro x hx + exact le_of_not_gt (not_and.mp (nb x) hx) + rw [← mem_lower_bounds_iff_forall_ge] at nb' + exact nb' + +/-- +Theorem I.33a (Additive Property) + +Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set +`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has a supremum, then `C` +has a supremum, and `sup C = sup A + sup B`. +-/ +theorem sup_minkowski_sum_eq_sup_add_sup (A B : Set ℝ) (a b : ℝ) + (hA : A.Nonempty) (hB : B.Nonempty) + (ha : IsLUB A a) (hb : IsLUB B b) + : IsLUB (Real.minkowski_sum A B) (a + b) := by + let C := Real.minkowski_sum A B + -- First we show `a + b` is an upper bound of `C`. + have hub : a + b ∈ upperBounds C := by + rw [mem_upper_bounds_iff_forall_le] + intro x hx + have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx + have hs₁ : a' ≤ a := (forall_lub_imp_forall_le ha) a' ha' + have hs₂ : b' ≤ b := (forall_lub_imp_forall_le hb) b' hb' + exact calc x + _ = a' + b' := hxab + _ ≤ a + b := add_le_add hs₁ hs₂ + -- Now we show `a + b` is the *least* upper bound of `C`. If it wasn't, then + -- either `¬IsLUB A a` or `¬IsLUB B b`, a contradiction. + by_contra nub + have h : ¬IsLUB A a ∨ ¬IsLUB B b := by + sorry + cases h with + | inl na => exact absurd ha na + | inr nb => exact absurd hb nb + +/-- +Theorem I.33b (Additive Property) + +Given nonempty subsets `A` and `B` of `ℝ`, let `C` denote the set +`C = {a + b : a ∈ A, b ∈ B}`. If each of `A` and `B` has an infimum, then `C` +has an infimum, and `inf C = inf A + inf B`. +-/ +theorem inf_minkowski_sum_eq_inf_add_inf (A B : Set ℝ) + (hA : A.Nonempty) (hB : B.Nonempty) + (ha : IsGLB A a) (hb : IsGLB B b) + : IsGLB (Real.minkowski_sum A B) (a + b) := by + let C := Real.minkowski_sum A B + -- First we show `a + b` is a lower bound of `C`. + have hub : a + b ∈ lowerBounds C := by + rw [mem_lower_bounds_iff_forall_ge] + intro x hx + have ⟨a', ⟨ha', ⟨b', ⟨hb', hxab⟩⟩⟩⟩: ∃ a ∈ A, ∃ b ∈ B, x = a + b := hx + have hs₁ : a' ≥ a := (forall_glb_imp_forall_ge ha) a' ha' + have hs₂ : b' ≥ b := (forall_glb_imp_forall_ge hb) b' hb' + exact calc x + _ = a' + b' := hxab + _ ≥ a + b := add_le_add hs₁ hs₂ + -- Now we show `a + b` is the *greatest* lower bound of `C`. If it wasn't, + -- then either `¬IsGLB A a` or `¬IsGLB B b`, a contradiction. + by_contra nub + have h : ¬IsGLB A a ∨ ¬IsGLB B b := by + sorry + cases h with + | inl na => exact absurd ha na + | inr nb => exact absurd hb nb + +/-- +Theorem I.34 + +Given two nonempty subsets `S` and `T` of `ℝ` such that `s ≤ t` for every `s` in +`S` and every `t` in `T`. Then `S` has a supremum, and `T` has an infimum, and +they satisfy the inequality `sup S ≤ inf T`. +-/ +theorem forall_mem_le_forall_mem_imp_sup_le_inf (S T : Set ℝ) + (hS : S.Nonempty) (hT : T.Nonempty) + (p : ∀ s ∈ S, ∀ t ∈ T, s ≤ t) + : ∃ (s : ℝ), IsLUB S s ∧ ∃ (t : ℝ), IsGLB T t ∧ s ≤ t := by + sorry end Real diff --git a/one-variable-calculus/Apostol/Chapter_I_3.tex b/one-variable-calculus/Apostol/Chapter_I_3.tex index 1591b8d..912144a 100644 --- a/one-variable-calculus/Apostol/Chapter_I_3.tex +++ b/one-variable-calculus/Apostol/Chapter_I_3.tex @@ -74,10 +74,51 @@ \ % Force space prior to *Proof.* \begin{enumerate}[(a)] - \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_sup} - \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.arb_close_to_inf} + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_imp_exists_gt_sup_sub_delta} + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_imp_exists_lt_inf_add_delta} \end{enumerate} \end{proof} +\begin{xtheorem}{I.33}[Additive Property] + + Given nonempty subsets $A$ and $B$ of $\mathbb{R}$, let $C$ denote the set + $$C = \{a + b : a \in A, b \in B\}.$$ + + \begin{enumerate}[(a)] + \item If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and + $$\sup{C} = \sup{A} + \sup{B}.$$ + \item If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and + $$\inf{C} = \inf{A} + \inf{B}.$$ + \end{enumerate} + +\end{xtheorem} + +\begin{proof} + + \ % Force space prior to *Proof.* + + \begin{enumerate}[(a)] + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.sup_minkowski_sum_eq_sup_add_sup} + \item \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.inf_minkowski_sum_eq_inf_add_inf} + \end{enumerate} + +\end{proof} + +\begin{xtheorem}{I.34} + + Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that + $$s \leq t$$ + for every $s$ in $S$ and every $t$ in $T$. Then $S$ has a supremum, and $T$ + has an infimum, and they satisfy the inequality + $$\sup{S} \leq \inf{T}.$$ + +\end{xtheorem} + +\begin{proof} + + \href{Chapter_I_3.lean}{Apostol.Chapter_I_3.Real.forall_mem_le_forall_mem_imp_sup_le_inf} + +\end{proof} + \end{document}