From 30bda83706a29a610a60eab5048dae6f30ec1c2d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 8 Apr 2023 15:09:11 -0600 Subject: [PATCH] Demonstrate how Lean/LaTeX will co-exist for now. --- .gitignore | 25 ++++++++-- common/Common/Sequence/Arithmetic.lean | 65 ++++++++++++++++++-------- common/Common/Sequence/Arithmetic.tex | 22 +++++++++ common/Common/Sequence/Geometric.lean | 65 ++++++++++++++++++-------- common/Common/Sequence/Geometric.tex | 22 +++++++++ common/Common/Tuple.lean | 3 +- 6 files changed, 159 insertions(+), 43 deletions(-) create mode 100644 common/Common/Sequence/Arithmetic.tex create mode 100644 common/Common/Sequence/Geometric.tex diff --git a/.gitignore b/.gitignore index 6e543ec..39d8ebd 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,22 @@ # Lean -**/build -**/lake-packages/* -**/_target -**/leanpkg.path +*/build +*/lake-packages +*/_target +*/leanpkg.path + +# TeX +*.aux +*.cb +*.cb2 +*.fdb_latexmk +*.fls +*.fmt +*.fot +*.lof +*.log +*.lot +*.out +*.pdf +*.synctex.gz +*.toc +.*.lb diff --git a/common/Common/Sequence/Arithmetic.lean b/common/Common/Sequence/Arithmetic.lean index cb6df03..fdb73a1 100644 --- a/common/Common/Sequence/Arithmetic.lean +++ b/common/Common/Sequence/Arithmetic.lean @@ -1,33 +1,41 @@ +import Mathlib.Data.Real.Basic import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring -/--[1] -A 0th-indexed arithmetic sequence. +/-- +A `0`th-indexed arithmetic sequence. -/ structure Arithmetic where - a₀ : Int - Δ : Int + a₀ : Real + Δ : Real namespace Arithmetic -/--[1] +/-- Returns the value of the `n`th term of an arithmetic sequence. --/ -def termClosed (seq : Arithmetic) (n : Nat) : Int := seq.a₀ + seq.Δ * n -/--[1] -Returns the value of the `n`th term of an arithmetic sequence. +This function calculates the value of this term directly. Keep in mind the +sequence is `0`th-indexed. -/ -def termRecursive : Arithmetic → Nat → Int +def termClosed (seq : Arithmetic) (n : Nat) : Real := + seq.a₀ + seq.Δ * n + +/-- +Returns the value of the `n`th term of an arithmetic sequence. + +This function calculates the value of this term recursively. Keep in mind the +sequence is `0`th-indexed. +-/ +def termRecursive : Arithmetic → Nat → Real | seq, 0 => seq.a₀ | seq, (n + 1) => seq.Δ + seq.termRecursive n -/--[1] -The recursive definition and closed definitions of an arithmetic sequence are -equivalent. +/-- +The recursive and closed term definitions of an arithmetic sequence agree with +one another. -/ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) - : seq.termRecursive n = seq.termClosed n := by + : seq.termRecursive n = seq.termClosed n := by induction n with | zero => unfold termRecursive termClosed; norm_num | succ n ih => calc @@ -35,14 +43,33 @@ theorem term_recursive_closed (seq : Arithmetic) (n : Nat) = seq.Δ + seq.termRecursive n := rfl _ = seq.Δ + seq.termClosed n := by rw [ih] _ = seq.Δ + (seq.a₀ + seq.Δ * n) := rfl - _ = seq.a₀ + seq.Δ * (n + 1) := by ring + _ = seq.a₀ + seq.Δ * (↑n + 1) := by ring + _ = seq.a₀ + seq.Δ * ↑(n + 1) := by simp _ = termClosed seq (n + 1) := rfl -/--[1] -Summation of the first `n` terms of an arithmetic sequence. +/-- +The summation of the first `n + 1` terms of an arithmetic sequence. + +This function calculates the sum directly. -/ -def sum : Arithmetic → Nat → Int +noncomputable def sum_closed (seq : Arithmetic) (n : Nat) : Real := + ((n + 1) * (seq.a₀ + seq.termClosed n)) / 2 + +/-- +The summation of the first `n + 1` terms of an arithmetic sequence. + +This function calculates the sum recursively. +-/ +def sum_recursive : Arithmetic → Nat → Real | _, 0 => 0 - | seq, (n + 1) => seq.termClosed n + seq.sum n + | seq, (n + 1) => seq.termClosed (n + 1) + seq.sum_recursive n + +/-- +The recursive and closed definitions of the sum of an arithmetic sequence agree +with one another. +-/ +theorem sum_recursive_closed (seq : Arithmetic) (n : Nat) + : sum_recursive seq n = sum_closed seq n := + sorry end Arithmetic diff --git a/common/Common/Sequence/Arithmetic.tex b/common/Common/Sequence/Arithmetic.tex new file mode 100644 index 0000000..fe790dc --- /dev/null +++ b/common/Common/Sequence/Arithmetic.tex @@ -0,0 +1,22 @@ +\documentclass{article} +\usepackage{amsfonts, amsthm} + +\newtheorem{theorem}{Theorem} + +\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} + +Common.Sequence.Arithmetic.sum\_recursive\_closed + +\end{proof} + +\end{document} diff --git a/common/Common/Sequence/Geometric.lean b/common/Common/Sequence/Geometric.lean index e5079a9..d810360 100644 --- a/common/Common/Sequence/Geometric.lean +++ b/common/Common/Sequence/Geometric.lean @@ -1,33 +1,41 @@ +import Mathlib.Data.Real.Basic import Mathlib.Tactic.NormNum import Mathlib.Tactic.Ring -/--[1] -A 0th-indexed geometric sequence. +/-- +A `0th`-indexed geometric sequence. -/ structure Geometric where - a₀ : Int - r : Int + a₀ : Real + r : Real namespace Geometric -/--[1] -The value of the `n`th term of an geometric sequence. --/ -def termClosed (seq : Geometric) (n : Nat) : Int := seq.a₀ * seq.r ^ n +/-- +Returns the value of the `n`th term of a geometric sequence. -/--[1] -The value of the `n`th term of an geometric sequence. +This function calculates the value of this term directly. Keep in mind the +sequence is `0`th-indexed. -/ -def termRecursive : Geometric → Nat → Int +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) -/--[1] -The recursive definition and closed definitions of a geometric sequence are -equivalent. +/-- +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 + : seq.termRecursive n = seq.termClosed n := by induction n with | zero => unfold termClosed termRecursive; norm_num | succ n ih => calc @@ -38,11 +46,30 @@ theorem term_recursive_closed (seq : Geometric) (n : Nat) _ = seq.a₀ * seq.r ^ (n + 1) := by ring _ = seq.termClosed (n + 1) := rfl -/--[1] -Summation of the first `n` terms of a geometric sequence. +/-- +The summation of the first `n + 1` terms of a geometric sequence. + +This function calculates the sum directly. -/ -def sum : Geometric → Nat → Int +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 | _, 0 => 0 - | seq, (n + 1) => seq.termClosed n + seq.sum n + | seq, (n + 1) => seq.termClosed n + seq.sum_recursive n + +/-- +The recursive and closed definitions of the sum of an arithmetic 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 := + sorry end Geometric diff --git a/common/Common/Sequence/Geometric.tex b/common/Common/Sequence/Geometric.tex new file mode 100644 index 0000000..b4e5c12 --- /dev/null +++ b/common/Common/Sequence/Geometric.tex @@ -0,0 +1,22 @@ +\documentclass{article} +\usepackage{amsfonts, amsthm} + +\newtheorem{theorem}{Theorem} + +\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} + +Common.Sequence.Geometric.sum\_recursive\_closed. + +\end{proof} + +\end{document} diff --git a/common/Common/Tuple.lean b/common/Common/Tuple.lean index 5040a18..a68456e 100644 --- a/common/Common/Tuple.lean +++ b/common/Common/Tuple.lean @@ -69,7 +69,8 @@ theorem eq_iff_snoc {t₁ t₂ : Tuple α n} /-- Implements decidable equality for `Tuple α m`, provided `a` has decidable equality. -/ -protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) : Decidable (Eq t₁ t₂) := +protected def hasDecEq [DecidableEq α] (t₁ t₂ : Tuple α n) + : Decidable (Eq t₁ t₂) := match t₁, t₂ with | t[], t[] => isTrue eq_nil | snoc as a, snoc bs b =>