From 61078b5e0a98909f619d50bb8e3ce79244ce98a8 Mon Sep 17 00:00:00 2001
From: Jasper Lee <leejasper851@gmail.com>
Date: Sat, 3 Aug 2024 17:12:12 -0400
Subject: [PATCH] did putnam 1999 fixes for isabelle and coq

---
 coq/src/putnam_1999_a2.v    | 3 ++-
 coq/src/putnam_1999_a3.v    | 4 ++--
 coq/src/putnam_1999_a4.v    | 4 ++--
 coq/src/putnam_1999_a5.v    | 4 ++--
 coq/src/putnam_1999_a6.v    | 8 ++++----
 coq/src/putnam_1999_b2.v    | 6 +++---
 coq/src/putnam_1999_b4.v    | 5 ++++-
 coq/src/putnam_1999_b6.v    | 4 +++-
 isabelle/putnam_1999_a2.thy | 2 +-
 isabelle/putnam_1999_a4.thy | 2 +-
 isabelle/putnam_1999_a6.thy | 2 +-
 isabelle/putnam_1999_b4.thy | 2 +-
 isabelle/putnam_1999_b6.thy | 2 +-
 13 files changed, 27 insertions(+), 21 deletions(-)

diff --git a/coq/src/putnam_1999_a2.v b/coq/src/putnam_1999_a2.v
index 8b6a3eb1..46adb04f 100644
--- a/coq/src/putnam_1999_a2.v
+++ b/coq/src/putnam_1999_a2.v
@@ -3,5 +3,6 @@ Open Scope ring_scope.
 Theorem putnam_1999_a2
     (R: numDomainType)
     (p : {poly R})
-    : forall x, p.[x] > 0 = true -> exists (k : nat) (f : nat -> {poly R}), p = \sum_(i < k) (f i)*(f i). 
+    (hpos : forall x, (p.[x] >= 0) = true)
+    : exists (k : nat) (f : nat -> {poly R}), p = \sum_(i < k) ((f i)*(f i)).
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_a3.v b/coq/src/putnam_1999_a3.v
index e88e9082..daa763fe 100644
--- a/coq/src/putnam_1999_a3.v
+++ b/coq/src/putnam_1999_a3.v
@@ -2,6 +2,6 @@ Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a3
     (f : R -> R := fun x => 1/(1- 2 * x - x^2))
     (a : nat -> R)
-    (hf : exists epsilon : R, epsilon > 0 /\ (forall x : R, 0 < Rabs (x) < epsilon -> filterlim (fun n : nat => sum_n (fun i => a i * x^i) n) eventually (locally (f x))))
-    : forall n : nat, ge n 0 -> (exists m : nat, (a n)^2 + (a (S n))^2 = a m).
+    (hf : exists epsilon : R, epsilon > 0 /\ (forall x : R, 0 <= Rabs (x) < epsilon -> filterlim (fun n : nat => sum_n (fun i => a i * x^i) n) eventually (locally (f x))))
+    : forall n : nat, exists m : nat, (a n)^2 + (a (S n))^2 = a m.
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_a4.v b/coq/src/putnam_1999_a4.v
index 2955bbfe..da30c606 100644
--- a/coq/src/putnam_1999_a4.v
+++ b/coq/src/putnam_1999_a4.v
@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_1999_a4_solution := 9/32.
+Definition putnam_1999_a4_solution : R := 9/32.
 Theorem putnam_1999_a4: 
-    Series (fun m => Series (fun n => (INR m ^ 2 * INR n) / (3 ^ m *(INR n * 3 ^ m + INR m * 3 ^ n)))) = putnam_1999_a4_solution.
+    Series (fun m => Series (fun n => (INR (m + 1) ^ 2 * INR (n + 1)) / (3 ^ (m + 1) * (INR (n + 1) * 3 ^ (m + 1) + INR (m + 1) * 3 ^ (n + 1))))) = putnam_1999_a4_solution.
 Proof. Admitted.
\ No newline at end of file
diff --git a/coq/src/putnam_1999_a5.v b/coq/src/putnam_1999_a5.v
index 92bd6d28..40119840 100644
--- a/coq/src/putnam_1999_a5.v
+++ b/coq/src/putnam_1999_a5.v
@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a5
-    (p : (nat -> R) -> R -> R := fun a x => sum_n (fun i => a i * x ^ i) 2000)
-    : forall (a: nat -> R), exists (c: R), Rabs (p a 0) <= c * RInt (fun  x => Rabs (p a x)) (-1) 1.
+    (p : (nat -> R) -> R -> R := fun a x => sum_n (fun i => a i * x ^ i) 1999)
+    : exists (c: R), forall (a: nat -> R), Rabs (p a 0) <= c * RInt (fun x => Rabs (p a x)) (-1) 1.
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_a6.v b/coq/src/putnam_1999_a6.v
index 0417a0b6..34d8d211 100644
--- a/coq/src/putnam_1999_a6.v
+++ b/coq/src/putnam_1999_a6.v
@@ -1,11 +1,11 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_1999_a6
-    (A := fix a (n: nat) :=
+    (A : nat -> R := fix a (n: nat) :=
         match n with 
         | O => 1
         | S O => 2
         | S (S O) => 24
-        | S (S ((S n'') as n') as n) => (6 * a n ^ 2 * a n'' - 8 * a n * a n' ^ 2) / (a n' * a n'')
-    end) 
-    : forall (n: nat), exists (k: nat), A n = INR (n * k).
+        | S (S ((S n'') as n') as n) => (6 * (a n) ^ 2 * a n'' - 8 * a n * (a n') ^ 2) / (a n' * a n'')
+    end)
+    : forall (n: nat), exists (k: Z), A n = INR (n + 1) * IZR k.
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_b2.v b/coq/src/putnam_1999_b2.v
index 54dbad60..25b7d49b 100644
--- a/coq/src/putnam_1999_b2.v
+++ b/coq/src/putnam_1999_b2.v
@@ -4,7 +4,7 @@ Theorem putnam_1999_b2
     (n: nat)
     (p : R -> R := fun x => sum_n (fun i => a1 i * x ^ i) n)
     (q : R -> R := fun x => sum_n (fun i => a2 i * x ^ i) 2)
-    : forall (x: R), p x = q x * (Derive_n (fun x => p x) 2) x /\
-    exists (r1 r2: R), r1 <> r2 /\ p r1 = 0 /\ p r2 = 0 ->
-    exists (roots: list R), length roots = n /\ NoDup roots /\ forall (r: R), In r roots -> p r = 0.
+    (hP : forall (x: R), p x = q x * (Derive_n p 2) x)
+    : (exists (r1 r2: R), r1 <> r2 /\ p r1 = 0 /\ p r2 = 0) ->
+    (exists (roots: list R), length roots = n /\ NoDup roots /\ (forall (r: R), In r roots -> p r = 0)).
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_b4.v b/coq/src/putnam_1999_b4.v
index 33838c26..c4acbe6d 100644
--- a/coq/src/putnam_1999_b4.v
+++ b/coq/src/putnam_1999_b4.v
@@ -2,5 +2,8 @@ Require Import Reals Coquelicot.Derive.
 Open Scope R_scope.
 Theorem putnam_1999_b4
     (f: R -> R)
-    : continuity (Derive_n f 3) -> forall (x: R), f x > 0 /\ (Derive_n f 1) x > 0 /\ (Derive_n f 2) x > 0 /\ (Derive_n f 3) x > 0 -> forall (x: R), (Derive_n f 3) x <= f x -> forall (x: R), (Derive_n f 1) x < 2 * f x.
+    (f_cont : (forall n : nat, (le 1 n /\ le n 3) -> (forall x : R, ex_derive_n f n x)) /\ continuity (Derive_n f 3))
+    (f_pos : forall (x: R), f x > 0 /\ (Derive_n f 1) x > 0 /\ (Derive_n f 2) x > 0 /\ (Derive_n f 3) x > 0)
+    (hf : forall (x: R), (Derive_n f 3) x <= f x)
+    : forall (x: R), (Derive_n f 1) x < 2 * f x.
 Proof. Admitted.
diff --git a/coq/src/putnam_1999_b6.v b/coq/src/putnam_1999_b6.v
index 6436b151..2594eb78 100644
--- a/coq/src/putnam_1999_b6.v
+++ b/coq/src/putnam_1999_b6.v
@@ -1,5 +1,7 @@
 Require Import Reals List Znumtheory.
 Theorem putnam_1999_b6
     (A : list Z)
-    : forall (x: Z), In x A -> x > 1 -> forall (n: Z), exists (s: Z), In s A -> Zis_gcd s n 1 \/ Zis_gcd s n s -> exists (s: Z) (t: Z) (p: Z), In s A /\ In t A /\ prime p -> Zis_gcd s t p.
+    (Age1 : forall (x: Z), In x A -> x > 1)
+    (hgcd : forall (n: Z), exists (s: Z), In s A /\ (Zis_gcd s n 1 \/ Zis_gcd s n s))
+    : exists (s: Z) (t: Z) (p: Z), In s A /\ In t A /\ Zis_gcd s t p /\ prime p.
 Proof. Admitted.
diff --git a/isabelle/putnam_1999_a2.thy b/isabelle/putnam_1999_a2.thy
index 7efdffb4..0d99b703 100644
--- a/isabelle/putnam_1999_a2.thy
+++ b/isabelle/putnam_1999_a2.thy
@@ -5,7 +5,7 @@ begin
 theorem putnam_1999_a2:
   fixes p :: "real poly"
   assumes hpos : "\<forall>x. poly p x \<ge> 0"
-  shows "\<exists>S :: real poly set . \<forall>x. finite S \<and> poly p x = (\<Sum>s \<in> S. (poly s x)^2)"
+  shows "\<exists>S :: real poly set . finite S \<and> (\<forall>x. poly p x = (\<Sum>s \<in> S. (poly s x)^2))"
   sorry
 
 end
diff --git a/isabelle/putnam_1999_a4.thy b/isabelle/putnam_1999_a4.thy
index e7378f0b..7a2a6b03 100644
--- a/isabelle/putnam_1999_a4.thy
+++ b/isabelle/putnam_1999_a4.thy
@@ -5,7 +5,7 @@ begin
 definition putnam_1999_a4_solution :: real where "putnam_1999_a4_solution \<equiv> undefined"
 (* 9 / 32 *)
 theorem putnam_1999_a4:
-  shows "(\<Sum> m :: nat. \<Sum> n :: nat. (m + 1) ^ 2 * (n + 1) / (3 ^ (m + 1) * ((n + 1) * 3 ^ (m + 1) + (m + 1) * 3 ^ (n + 1)))) = putnam_1999_a4_solution"
+  shows "(\<Sum> m :: nat. \<Sum> n :: nat. ((m + 1) ^ 2 * (n + 1)) / (3 ^ (m + 1) * ((n + 1) * 3 ^ (m + 1) + (m + 1) * 3 ^ (n + 1)))) = putnam_1999_a4_solution"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1999_a6.thy b/isabelle/putnam_1999_a6.thy
index 945ff847..c1056ca1 100644
--- a/isabelle/putnam_1999_a6.thy
+++ b/isabelle/putnam_1999_a6.thy
@@ -8,7 +8,7 @@ theorem putnam_1999_a6:
   and ha2: "a 2 = 2"
   and ha3: "a 3 = 24"
   and hange4: "\<forall> n :: nat. n \<ge> 4 \<longrightarrow> a n = (6 * (a (n - 1)) ^ 2 * (a (n - 3)) - 8 * (a (n - 1)) * (a (n - 2)) ^ 2) / (a (n - 2) * a (n - 3))"
-  shows "\<forall> n. n \<ge> 1 \<longrightarrow> (\<exists> k :: int. a n = k * n)"
+  shows "\<forall> n :: nat. n \<ge> 1 \<longrightarrow> (\<exists> k :: int. a n = k * n)"
   sorry
 
 end
\ No newline at end of file
diff --git a/isabelle/putnam_1999_b4.thy b/isabelle/putnam_1999_b4.thy
index dd7cec9c..4def02cb 100644
--- a/isabelle/putnam_1999_b4.thy
+++ b/isabelle/putnam_1999_b4.thy
@@ -4,7 +4,7 @@ begin
 
 theorem putnam_1999_b4:
   fixes f :: "real\<Rightarrow>real"
-  assumes f_cont : "continuous_on UNIV ((deriv^^3) f)"
+  assumes f_cont : "\<forall>n::nat\<in>{0..2}. ((deriv^^n) f) C1_differentiable_on UNIV"
     and f_pos : "\<forall>x. f x > 0"
     and f'_pos : "\<forall>x. deriv f x > 0"
     and f''_pos : "\<forall>x. (deriv^^2) f x > 0"
diff --git a/isabelle/putnam_1999_b6.thy b/isabelle/putnam_1999_b6.thy
index f02ca810..44175401 100644
--- a/isabelle/putnam_1999_b6.thy
+++ b/isabelle/putnam_1999_b6.thy
@@ -7,7 +7,7 @@ theorem putnam_1999_b6:
   assumes S_fin: "finite S"
     and Sge1: "\<forall>s \<in> S. s > 1"
     and hgcd: "\<forall>n::int. \<exists>s \<in> S. (gcd s n) = 1 \<or> (gcd s n) = s"
-  shows "\<exists> s \<in> S. \<exists> t \<in> S. prime(gcd s t)"
+  shows "\<exists> s \<in> S. \<exists> t \<in> S. prime (gcd s t)"
   sorry
 
 end