Fix 2015 B6

Mathlib's `tsum` (with notation `∑'`) gives the wrong answer for
conditionally-convergent sums (unless they happen to sum to zero) and so
is not the right tool in this question.

This is an unfortunate footgun and gap in Mathlib.

The fix is to make a basic limit statement about the sequence of partial
sums.

lean4/src/putnam_2015_b6.lean

@@ -1,12 +1,13 @@
 import Mathlib
 open BigOperators
 
-open Function
+open Filter Topology
 
 noncomputable abbrev putnam_2015_b6_solution : ℝ := sorry
 -- Real.pi ^ 2 / 16
 theorem putnam_2015_b6
-(A : ℕ → ℕ)
-(hA : ∀ k > 0, A k = {j : ℕ | Odd j ∧ j ∣ k ∧ j < Real.sqrt (2 * k)}.encard)
-: ∑' k : Set.Ici 1, (-1 : ℝ) ^ ((k : ℝ) - 1) * (A k / (k : ℝ)) = putnam_2015_b6_solution :=
-sorry
+    (A : ℕ → ℕ)
+    (hA : ∀ k > 0, A k = {j : ℕ | Odd j ∧ j ∣ k ∧ j < Real.sqrt (2 * k)}.encard) :
+    Tendsto (fun K : ℕ ↦ ∑ k in Finset.Icc 1 K, (-1 : ℝ) ^ ((k : ℝ) - 1) * (A k / (k : ℝ)))
+      atTop (𝓝 putnam_2015_b6_solution) :=
+  sorry