Merge pull request #238 from ocfnash/more_fixes

Fix a few minor Lean misformalisations

lean4/src/putnam_1994_a1.lean

@@ -6,7 +6,7 @@ open Filter Topology
 Suppose that a sequence $a_1,a_2,a_3,\dots$ satisfies $0<a_n \leq a_{2n}+a_{2n+1}$ for all $n \geq 1$. Prove that the series $\sum_{n=1}^\infty a_n$ diverges.
 -/
 theorem putnam_1994_a1
-(a : ℕ → ℝ)
-(ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1))
-: ¬(∃ s : ℝ, Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop (𝓝 s)) :=
-sorry
+    (a : ℕ → ℝ)
+    (ha : ∀ n ≥ 1, 0 < a n ∧ a n ≤ a (2 * n) + a (2 * n + 1)) :
+    Tendsto (fun N : ℕ => ∑ n : Set.Icc 1 N, a n) atTop atTop :=
+  sorry

lean4/src/putnam_1994_b3.lean

@@ -7,9 +7,7 @@ abbrev putnam_1994_b3_solution : Set ℝ := sorry
 /--
 Find the set of all real numbers $k$ with the following property: For any positive, differentiable function $f$ that satisfies $f'(x)>f(x)$ for all $x$, there is some number $N$ such that $f(x)>e^{kx}$ for all $x>N$.
 -/
-theorem putnam_1994_b3
-(k : ℝ)
-(allfexN : Prop)
-(hallfexN : allfexN = ∀ f : ℝ → ℝ, (f > 0 ∧ Differentiable ℝ f ∧ ∀ x : ℝ, deriv f x > f x) → (∃ N : ℝ, ∀ x > N, f x > Real.exp (k * x)))
-: allfexN ↔ k ∈ putnam_1994_b3_solution :=
-sorry
+theorem putnam_1994_b3 :
+    {k | ∀ f (hf : (∀ x, 0 < f x ∧ f x < deriv f x) ∧ Differentiable ℝ f),
+      ∃ N, ∀ x > N, Real.exp (k * x) < f x} = putnam_1994_b3_solution :=
+  sorry

lean4/src/putnam_2010_a5.lean

@@ -1,11 +1,14 @@
 import Mathlib
 
+open scoped Matrix
+
 /--
 Let $G$ be a group, with operation $*$. Suppose that \begin{enumerate} \item[(i)] $G$ is a subset of $\mathbb{R}^3$ (but $*$ need not be related to addition of vectors); \item[(ii)] For each $\mathbf{a},\mathbf{b} \in G$, either $\mathbf{a}\times \mathbf{b} = \mathbf{a}*\mathbf{b}$ or $\mathbf{a}\times \mathbf{b} = 0$ (or both), where $\times$ is the usual cross product in $\mathbb{R}^3$. \end{enumerate} Prove that $\mathbf{a} \times \mathbf{b} = 0$ for all $\mathbf{a}, \mathbf{b} \in G$.
 -/
 theorem putnam_2010_a5
-(G : Set (Fin 3 → ℝ))
-(hGgrp : Group G)
-(hGcross : ∀ a b : G, crossProduct a b = (a * b : Fin 3 → ℝ) ∨ crossProduct (a : Fin 3 → ℝ) b = 0)
-: ∀ a b : G, crossProduct (a : Fin 3 → ℝ) b = 0 :=
-sorry
+    (G : Type*) [Group G]
+    (i : G ↪ (Fin 3 → ℝ))
+    (h : ∀ a b, (i a) ×₃ (i b) = i (a * b) ∨ (i a) ×₃ (i b) = 0)
+    (a b : G) :
+    (i a) ×₃ (i b) = 0 :=
+  sorry

lean4/src/putnam_2020_b5.lean

@@ -7,7 +7,7 @@ For $j \in \{1, 2, 3, 4\}$, let $z_j$ be a complex number with $|z_j| = 1$ and $
 -/
 theorem putnam_2020_b5
 (z : Fin 4 → ℂ)
-(hzle1 : ∀ n, ‖z n‖ < 1)
+(hzle1 : ∀ n, ‖z n‖ = 1)
 (hzne1 : ∀ n, z n ≠ 1)
 : 3 - z 0 - z 1 - z 2 - z 3 + (z 0) * (z 1) * (z 2) * (z 3) ≠ 0:=
 sorry