2002 isabelle and coq fixes

coq/src/putnam_2002_a1.v

@@ -1,8 +1,10 @@
 Require Import Reals Factorial Coquelicot.Coquelicot.
 Definition putnam_2002_a1_solution (k n: nat) := Rpower (-1 * INR k) (INR n) * INR (fact n).
 Theorem putnam_2002_a1
+    (k : nat)
     (p : (nat -> R) -> R -> nat -> R := fun a x n => sum_n (fun i => a i * x ^ i) n)
-    : forall (N k: nat), gt k 0 -> exists (a: nat -> R) (n: nat), forall (x: R), 
-    (Derive_n (fun x => 1 / (x ^ k - 1)) N) x = (p a x n) / (x ^ k - 1) ^ (n + 1) ->
-    p a x 1%nat = putnam_2002_a1_solution k n.
+    (kpos : gt k 0)
+    : forall (N: nat), forall (a: nat -> R) (n: nat),
+    (forall (x: R), (Derive_n (fun x => 1 / (x ^ k - 1)) N) x = (p a x n) / (x ^ k - 1) ^ (n + 1)) ->
+    p a 1 n = putnam_2002_a1_solution k n.
 Proof. Admitted.

coq/src/putnam_2002_b3.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Open Scope R.
 Theorem putnam_2002_b3 
-    : forall (n: nat), ge n 1 -> let n := INR n in 1 / (2 * n * exp 1) < 1 / (exp 1) - Rpower (1 - 1 / n) n < 1 / (n * (exp 1)).
+    : forall (n: nat), gt n 1 -> let n := INR n in 1 / (2 * n * exp 1) < 1 / (exp 1) - Rpower (1 - 1 / n) n < 1 / (n * (exp 1)).
 Proof. Admitted.

isabelle/putnam_2002_a2.thy

@@ -1,6 +1,7 @@
 theory putnam_2002_a2 imports Complex_Main
 "HOL-Analysis.Finite_Cartesian_Product"
 "HOL-Analysis.Linear_Algebra"
+"HOL-Analysis.Elementary_Metric_Spaces"
 begin
 
 theorem putnam_2002_a2:

isabelle/putnam_2002_a3.thy

@@ -3,7 +3,7 @@ begin
 
 theorem putnam_2002_a3:
   fixes n Tn :: "int"
-  defines "Tn \<equiv> card {S :: int set. S \<subseteq> {1..16} \<and> S \<noteq> {} \<and> (\<exists> k :: int. k = (real 1)/(card S) * (\<Sum> s \<in> S. s))}"
+  defines "Tn \<equiv> card {S :: int set. S \<subseteq> {1..n} \<and> S \<noteq> {} \<and> (\<exists> k :: int. k = (real 1)/(card S) * (\<Sum> s \<in> S. s))}"
   assumes hn : "n \<ge> 2"
   shows "even (Tn - n)"
   sorry

isabelle/putnam_2002_b5.thy

@@ -5,8 +5,7 @@ begin
 fun digits :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where
   "digits b n = (if b < 2 then (replicate n 1) else (if n < b then [n] else [n mod b] @ digits b (n div b)))"
 theorem putnam_2002_b5:
-  shows "\<exists> n :: nat. card {b :: nat. length (digits b n) = 3 \<and> digits b n = rev (digits b n)} \<ge> 2002"
+  shows "\<exists> n :: nat. card {b :: nat. b \<ge> 1 \<and> length (digits b n) = 3 \<and> digits b n = rev (digits b n)} \<ge> 2002"
   sorry
 
 end
-

lean4/src/putnam_2002_b5.lean

@@ -4,5 +4,5 @@ open BigOperators
 open Nat Set Topology Filter
 
 theorem putnam_2002_b5
-: ∃ n : ℕ, {b : ℕ | (Nat.digits b n).length = 3 ∧ List.Palindrome (Nat.digits b n)}.ncard ≥ 2002 :=
+: ∃ n : ℕ, {b : ℕ | b ≥ 1 ∧ (Nat.digits b n).length = 3 ∧ List.Palindrome (Nat.digits b n)}.ncard ≥ 2002 :=
 sorry