From 5fe571c31361ffd01605cc5f7da779f49797d4bb Mon Sep 17 00:00:00 2001 From: Terence Tao Date: Mon, 21 Jul 2025 08:45:25 -0700 Subject: [PATCH] Update appendices --- analysis/Analysis/Appendix_A_1.lean | 2 +- analysis/Analysis/Appendix_A_2.lean | 7 +++---- analysis/Analysis/Appendix_A_3.lean | 3 ++- analysis/Analysis/Appendix_A_4.lean | 2 +- analysis/Analysis/Appendix_A_5.lean | 2 +- analysis/Analysis/Appendix_A_6.lean | 3 +-- analysis/Analysis/Appendix_A_7.lean | 2 +- analysis/Analysis/Appendix_B_1.lean | 23 ++++++++++------------- analysis/Analysis/Appendix_B_2.lean | 2 +- 9 files changed, 21 insertions(+), 25 deletions(-) diff --git a/analysis/Analysis/Appendix_A_1.lean b/analysis/Analysis/Appendix_A_1.lean index c6c03bc..f9bb9c8 100644 --- a/analysis/Analysis/Appendix_A_1.lean +++ b/analysis/Analysis/Appendix_A_1.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.1 +# Analysis I, Appendix A.1: Mathematical Statements An introduction to mathematical statements. Showcases some basic tactics and Lean syntax. diff --git a/analysis/Analysis/Appendix_A_2.lean b/analysis/Analysis/Appendix_A_2.lean index 60b998f..2d5ca10 100644 --- a/analysis/Analysis/Appendix_A_2.lean +++ b/analysis/Analysis/Appendix_A_2.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.2 +# Analysis I, Appendix A.2: Implication An introduction to implications. Showcases some basic tactics and Lean syntax. @@ -134,8 +134,7 @@ example {x:ℝ} (h:x>0) (hsin: Real.sin x = 1) : x ≥ Real.pi / 2 := by linarith linarith have h2 : Real.sin x < Real.sin (Real.pi / 2) := by - apply Real.sin_lt_sin_of_lt_of_le_pi_div_two _ _ h' - . linarith - linarith + -- the <;> tactic applies the next tactic to all currently visible goals. + apply Real.sin_lt_sin_of_lt_of_le_pi_div_two _ _ h' <;> linarith simp at h1 h2 linarith diff --git a/analysis/Analysis/Appendix_A_3.lean b/analysis/Analysis/Appendix_A_3.lean index 9e6b40d..8162191 100644 --- a/analysis/Analysis/Appendix_A_3.lean +++ b/analysis/Analysis/Appendix_A_3.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.3 +# Analysis I, Appendix A.3: The structure of proofs Some examples of proofs @@ -18,6 +18,7 @@ example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := /-- Proposition A.3.2 -/ example {x:ℝ} : x = Real.pi → Real.sin (x/2) + 1 = 2 := by intro h + -- congr() produces an equality (or similar relation) from one or more existing relations, such as `h`, by substituting that relation in every location marked with a `$` sign followed by that relation, for instance `h` would be substituted at every location of `$h`. replace h := congr($h/2) replace h := congr(Real.sin $h) simp at h diff --git a/analysis/Analysis/Appendix_A_4.lean b/analysis/Analysis/Appendix_A_4.lean index 409393b..0258cbb 100644 --- a/analysis/Analysis/Appendix_A_4.lean +++ b/analysis/Analysis/Appendix_A_4.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.4 +# Analysis I, Appendix A.4: Variables and quantifiers Some examples of how variables and quantifiers are used in Lean diff --git a/analysis/Analysis/Appendix_A_5.lean b/analysis/Analysis/Appendix_A_5.lean index 332247e..7a97891 100644 --- a/analysis/Analysis/Appendix_A_5.lean +++ b/analysis/Analysis/Appendix_A_5.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.5 +# Analysis I, Appendix A.5: Nested quantifiers Some examples of nested quantifiers in Lean diff --git a/analysis/Analysis/Appendix_A_6.lean b/analysis/Analysis/Appendix_A_6.lean index 3eaaf76..014bc83 100644 --- a/analysis/Analysis/Appendix_A_6.lean +++ b/analysis/Analysis/Appendix_A_6.lean @@ -3,7 +3,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv /-! -# Analysis I, Appendix A.6 +# Analysis I, Appendix A.6: Some examples of proofs and quantifiers Some examples of proofs and quantifiers in Lean @@ -72,4 +72,3 @@ example : ∃ ε > 0, ∀ x, 0 < x ∧ x < ε → sin x > x / 2 := by convert hcosy using 1 . ring field_simp - diff --git a/analysis/Analysis/Appendix_A_7.lean b/analysis/Analysis/Appendix_A_7.lean index b66b171..30efc0e 100644 --- a/analysis/Analysis/Appendix_A_7.lean +++ b/analysis/Analysis/Appendix_A_7.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix A.7 +# Analysis I, Appendix A.7: Equality Introduction to equality in Lean diff --git a/analysis/Analysis/Appendix_B_1.lean b/analysis/Analysis/Appendix_B_1.lean index 380c5b4..5cc6942 100644 --- a/analysis/Analysis/Appendix_B_1.lean +++ b/analysis/Analysis/Appendix_B_1.lean @@ -1,7 +1,7 @@ import Mathlib.Tactic /-! -# Analysis I, Appendix B.1 +# Analysis I, Appendix B.1: The decimal representation of natural numbers Am implementation of the decimal representation of Mathlib's natural numbers `ℕ`. @@ -155,7 +155,7 @@ theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := by convert Finset.single_le_sum _ (Finset.mem_univ a) . simp [a, head, List.head_eq_getElem] . infer_instance - intro i _; positivity + intros; positivity /-- An operation implicit in the proof of Theorem B.1.5: -/ abbrev PosintDecimal.append (p:PosintDecimal) (d:Digit) : PosintDecimal := @@ -175,20 +175,17 @@ theorem PosintDecimal.append_toNat (p:PosintDecimal) (d:Digit) : congr 2 have : p.head :: (p.digits.tail ++ [d]) = p.digits ++ [d] := by rw [←List.cons_append, head, List.head_cons_tail] - have hlen : p.digits.length - 1 - ↑i < (p.digits ++ [d]).length := by - simp; omega + have hlen : p.digits.length - 1 - ↑i < (p.digits ++ [d]).length := by simp; omega calc _ = (p.digits ++ [d])[p.digits.length - 1 - ↑i] := by congr _ = _ := by apply List.getElem_append_left theorem PosintDecimal.eq_append {p:PosintDecimal} (h: 2 ≤ p.digits.length) : ∃ (q:PosintDecimal) (d:Digit), p = q.append d := by use mk' p.head (p.digits.tail.dropLast) p.head_ne_zero - set a := p.digits.getLast p.nonempty - use a + set a := p.digits.getLast p.nonempty; use a apply congr' simp [mk', List.cons_append] - have := List.head_cons_tail p.digits p.nonempty - rw [←this] + rw [←List.head_cons_tail p.digits p.nonempty] congr 1 convert (List.dropLast_append_getLast _).symm using 2; swap . simp [←List.length_pos_iff]; linarith @@ -214,14 +211,14 @@ theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p . simp [hdl, mk'] intro i hi₁ hi₂ replace hi₁ : i = 0 := by linarith - subst hi₁; simp [mk', Digit.mk, hd] + simp [hi₁, mk', Digit.mk, hd] have : d.toNat ≥ 10 := calc _ ≥ (d.head:ℕ) * 10^(d.digits.length-1) := by set a : Fin d.digits.length := ⟨ d.digits.length - 1, by omega ⟩ convert Finset.single_le_sum _ (Finset.mem_univ a) . simp [a, head, List.head_eq_getElem] . infer_instance - intro i _; positivity + intros; positivity _ ≥ 1 * 10^(2-1) := by gcongr . have := d.head_ne_zero'; omega @@ -256,9 +253,9 @@ theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p @[simp] theorem PosintDecimal.coe_inj (p q:PosintDecimal) : (p:ℕ) = (q:ℕ) ↔ p = q := by - constructor - . intro h; exact (exists_unique _ (q.pos)).unique h rfl - intro h; rw [h] + constructor <;> intro h + . exact (exists_unique _ (q.pos)).unique h rfl + rw [h] inductive IntDecimal where diff --git a/analysis/Analysis/Appendix_B_2.lean b/analysis/Analysis/Appendix_B_2.lean index 2691592..4517fea 100644 --- a/analysis/Analysis/Appendix_B_2.lean +++ b/analysis/Analysis/Appendix_B_2.lean @@ -2,7 +2,7 @@ import Mathlib.Tactic import Analysis.Appendix_B_1 /-! -# Analysis I, Appendix B.2 +# Analysis I, Appendix B.2: The decimal representation of real numbers Am implementation of the decimal representation of Mathlib's real numbers `ℝ`. -- 2.51.2