Fix 1994 B3

This is a slightly subjective fix. The issue is that `f > 0` does not
mean that `f` is positive everywhere; it means that `f` is non-negative
everywhere and positive at at least one point. I believe this is what is
intended in the informal statement.

The issue is slightly confounded by the fact that if for all `x`,
`deriv f x > f x` and `f x` is non-negative then the derivative is
strictly positive, and thus `f` is strictly monotone, and thus being
non-negative implies being strictly positive everywhere.

So there is no mathematical change to the meaning here but I think this
is a more faithful representation of the question. It should also be
noted that the fact that there is no mathematical change depends upon
not-quite-totally-trivial facts.

I have also taken the opportunity to rewrite question with slightly
improved style.

lean4/src/putnam_1994_b3.lean

@@ -8,9 +8,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