Update Thu Sep 5 09:09:02 EDT 2024

Author: hrmacbeth

Math2001/Homework/hw1.lean

@@ -0,0 +1,33 @@
+/- Copyright (c) Heather Macbeth, 2023.  All rights reserved. -/
+import Mathlib.Data.Real.Basic
+import Library.Basic
+import AutograderLib
+
+math2001_init
+
+/-! # Homework 1
+
+Don't forget to compare with the text version,
+https://github.com/hrmacbeth/math2001/wiki/Homework-1,
+for clearer statements and any special instructions. -/
+
+
+@[autograded 5]
+theorem problem1 {p q : ℤ} (h1 : p + 4 * q = 1) (h2 : q - 1 = 2) : p = -11 := by
+  sorry
+
+@[autograded 5]
+theorem problem2 {a b : ℝ} (h1 : a + 2 * b = 4) (h2 : a - b = 1) : a = 2 := by
+  sorry
+
+@[autograded 5]
+theorem problem3 {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 := by
+  sorry
+
+@[autograded 5]
+theorem problem4 {x : ℚ} : x ^ 2 - 2 * x ≥ -1 := by
+  sorry
+
+@[autograded 5]
+theorem problem5 (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
+  sorry