My solutions to Tao's Analysis I, formalized in Lean
danabra.mov
1import Mathlib.Tactic
2
3/-!
4# Analysis I, Appendix A.3: The structure of proofs
5
6Some examples of proofs
7
8-/
9
10/-- Proposition A.3.1 -/
11example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := by
12 intro h
13 replace h := hAC h
14 replace h := hCD h
15 replace h := hDB h
16 exact h
17
18/-- Proposition A.3.2 -/
19example {x:ℝ} : x = Real.pi → Real.sin (x/2) + 1 = 2 := by
20 intro h
21 -- 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`.
22 replace h := congr($h/2)
23 replace h := congr(Real.sin $h)
24 simp at h
25 replace h := congr($h + 1)
26 convert h
27 norm_num
28
29
30/-- Proposition A.3.1, alternate proof -/
31example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := by
32 intro h
33 suffices hD : D
34 . exact hDB hD
35 suffices hC : C
36 . exact hCD hC
37 exact hAC h
38
39/-- Proposition A.3.2, alternate proof -/
40example {x:ℝ} : x = Real.pi → Real.sin (x/2) + 1 = 2 := by
41 intro h
42 suffices h1 : Real.sin (x/2) = 1
43 . simp [h1]
44 norm_num
45 suffices h2 : x/2 = Real.pi/2
46 . simp [h2]
47 simp [h]
48
49/-- Proposition A.3.3 -/
50example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := by
51 apply summable_of_ratio_test_tendsto_lt_one h' _ _
52 . simp [Filter.eventually_atTop]
53 use 1
54 intro b hb
55 simp [show b ≠ 0 by linarith, show r ≠ 0 by linarith]
56 suffices hconv: Filter.atTop.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) (nhds r)
57 . apply hconv.congr'
58 simp [Filter.EventuallyEq, Filter.eventually_atTop]
59 use 1
60 intro b hb
61 have : b > 0 := by linarith
62 have hb1 : (b+1:ℝ) > 0 := by linarith
63 simp [abs_of_pos h, abs_of_pos hb1]
64 field_simp
65 ring_nf
66 suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) (nhds 1)
67 . convert hconv.const_mul r
68 simp
69 suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) (nhds 1)
70 . apply hconv.congr'
71 simp [Filter.EventuallyEq, Filter.eventually_atTop]
72 use 1
73 intro b hb
74 have : (b:ℝ) > 0 := by norm_cast
75 field_simp
76 suffices hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) (nhds 0)
77 . convert hconv.const_add 1
78 simp
79 exact tendsto_one_div_atTop_nhds_zero_nat
80
81/-- Proposition A.3.1, third proof -/
82example {A B C D: Prop} (hAC: A → C) (hCD: C → D) (hDB: D → B): A → B := by
83 intro h
84 suffices hD : D
85 . exact hDB hD
86 have hC : C := hAC h
87 exact hCD hC
88
89/-- Proposition A.3.4 -/
90example {A B C D E F G H I:Prop} (hAE: A → E) (hEB: E ∧ B → F) (hADG : A → G → D) (hHI: H ∨ I) (hFHC : F ∧ H → C) (hAHG : A ∧ H → G) (hIG: I → G) (hIGC: G → C) : A ∧ B → C ∧ D := by
91 rintro ⟨ hA, hB ⟩
92 have hE : E := hAE hA
93 have hF : F := hEB ⟨hE, hB⟩
94 suffices hCG : C ∧ G
95 . obtain ⟨ hC, hG ⟩ := hCG
96 have hD : D := hADG hA hG
97 exact ⟨hC, hD⟩
98 rcases hHI with hH | hI
99 . have hC := hFHC ⟨ hF, hH⟩
100 have hG := hAHG ⟨hA, hH⟩
101 exact ⟨hC, hG⟩
102 have hG := hIG hI
103 have hC := hIGC hG
104 exact ⟨hC, hG⟩
105
106/-- Proposition A.3.5 -/
107example {A B C D:Prop} (hBC: B → C) (hAD: A → D) (hCD: D → ¬ C) : A → ¬ B := by
108 intro hA
109 by_contra hB
110 have hC : C := hBC hB
111 have hD : D := hAD hA
112 have hC' : ¬ C := hCD hD
113 contradiction