From 958aaea2c451eda62de72339236ee6459df24550 Mon Sep 17 00:00:00 2001
From: Oliver Nash <ddojsioc@google.com>
Date: Tue, 22 Oct 2024 17:16:47 +0000
Subject: [PATCH] Fix 1994 A1

The statement should be that the sum diverges, rather than that it has
no finite limit (even though these are easily equivalent given the
latent positivity hypotheses).
---
 lean4/src/putnam_1994_a1.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/lean4/src/putnam_1994_a1.lean b/lean4/src/putnam_1994_a1.lean
index 99884791..7a7f0a8c 100644
--- a/lean4/src/putnam_1994_a1.lean
+++ b/lean4/src/putnam_1994_a1.lean
@@ -7,7 +7,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