fixes for 2003 isabelle and coq (except 2003_b5 for coq)

coq/src/putnam_2003_a1.v

@@ -1,8 +1,8 @@
 Require Import Nat List Ensembles Finite_sets Coquelicot.Coquelicot.
-Definition putnam_2003_a1_solution (n: nat) := n.
+Definition putnam_2003_a1_solution : nat -> nat := (fun n : nat => n).
 Theorem putnam_2003_a1
     (n: nat)
     (hn : n > 0)
-    (E: Ensemble (list nat) := fun l => forall (i j: nat), i < length l /\ j < length l /\ i < j -> nth i l 0 <= nth j l 0 /\ fold_left add l 0 = n)
+    (E: Ensemble (list nat) := fun l => fold_left add l 0 = n /\ (forall i : nat, i < length l -> nth i l 0 > 0) /\ (forall (i j: nat), i < length l /\ j < length l /\ i < j -> nth i l 0 <= nth j l 0) /\ last l 0 <= hd 0 l + 1)
     : cardinal (list nat) E (putnam_2003_a1_solution n).
 Proof. Admitted.

coq/src/putnam_2003_a2.v

@@ -6,7 +6,11 @@ Theorem putnam_2003_a2
         | _, nil => nil
         | h1 :: t1, h2 :: t2 => (h1 + h2) :: suml t1 t2
     end)
-    : forall (n: nat) (a b: list R), length a = n /\ length b = n ->
-    (fold_left Rmult a 1) ^ (1 / n) + (fold_left Rmult b 1) ^ (1 / n) <=
+    (n : nat)
+    (a b : list R)
+    (npos : ge n 1)
+    (ablen : length a = n /\ length b = n)
+    (abnneg : forall i : nat, lt i n -> nth i a 0 >= 0 /\ nth i b 0 >= 0)
+    : (fold_left Rmult a 1) ^ (1 / n) + (fold_left Rmult b 1) ^ (1 / n) <=
     (fold_left Rmult (Suml a b) 1) ^ (1 / n).
 Proof. Admitted.

coq/src/putnam_2003_a3.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2003_a3_solution := 2 * sqrt 2 - 1.
 Theorem putnam_2003_a3
     (f : R -> R := fun x => Rabs (sin x + cos x + tan x + 1 / tan x + 1 / cos x  + 1 / sin x))
-    : exists (minx: R), forall (x: R), f minx <= f x -> f minx = putnam_2003_a3_solution.
+    : (exists x : R, f x = putnam_2003_a3_solution) /\ (forall x : R, f x >= putnam_2003_a3_solution).
 Proof. Admitted.

coq/src/putnam_2003_a4.v

@@ -2,7 +2,7 @@ Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_a4
     (a b c A B C: R)
     (ha : a <> 0)
-    (hA :A <> 0)
+    (hA : A <> 0)
     (hp : forall (x: R), Rabs (a * x ^ 2 + b * x + c) <= Rabs (A * x ^ 2 + B * x + C))
     : Rabs (b ^ 2 - 4 * a * c) <= Rabs (B ^ 2 - 4 * A * C).
 Proof. Admitted.

coq/src/putnam_2003_b1.v

@@ -1,7 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2003_b1_solution := True.
+Definition putnam_2003_b1_solution := False.
 Theorem putnam_2003_b1
     (p : (nat -> R) -> R -> nat -> R := fun coeff x n => sum_n (fun i => coeff i * x ^ i) n)
-    : exists (coeffa coeffb coeffc coeffd: nat -> R) (na nb nc nd: nat), forall (x y: R),
-    1 + x * y * (x * y) ^ 2 = (p coeffa x na) * (p coeffc y nc) + (p coeffb x nb) * (p coeffd y nd).
+    : (exists (coeffa coeffb coeffc coeffd: nat -> R) (na nb nc nd: nat), forall (x y: R),
+    1 + x * y + x ^ 2 * y ^ 2 = (p coeffa x na) * (p coeffc y nc) + (p coeffb x nb) * (p coeffd y nd))
+    <-> putnam_2003_b1_solution.
 Proof. Admitted.

coq/src/putnam_2003_b3.v

@@ -2,13 +2,15 @@ Require Import Nat List Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_b3
     (lcmn := fix lcm_n (args : list nat) : nat :=
         match args with
-        | nil => 0%nat
+        | nil => 1%nat
         | h :: args' => div (h * (lcm_n args')) (gcd h (lcm_n args'))
     end)
     (prodn := fix prod_n (m: nat -> R) (n : nat) : R :=
         match n with
         | O => m 0%nat
-        | S n' => m n' * prod_n m n'
+        | S n' => m n * prod_n m n'
     end)
-    : forall (n: nat), gt n 0 -> INR (fact n) = prodn (fun i => INR (lcmn (seq 0 (div n (i + 1))))) n.
+    (n : nat)
+    (npos : gt n 0)
+    : INR (fact n) = prodn (fun i => INR (lcmn (seq 1 (div n (i + 1))))) (sub n 1).
 Proof. Admitted.

coq/src/putnam_2003_b4.v

@@ -1,13 +1,13 @@
 Require Import Reals ZArith Coquelicot.Coquelicot.
 Theorem putnam_2003_b4
     (a b c d e: Z)
+    (r1 r2 r3 r4: R)
     (ha : ~ Z.eq a 0)
     : let a := IZR a in 
     let b := IZR b in 
     let c := IZR c in 
     let d := IZR d in 
     let e := IZR e in 
-    exists (r1 r2 r3 r4: R), forall (z: R), 
-    a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + e = a * (z - r1) * (z - r2) * (z - r3) * (z - r4) ->
-    (exists (p q: Z), r1 + r2 = IZR p / IZR q) /\ r1 + r2 <> r3 + r4 -> exists (p q: Z), r1 * r2 = IZR p / IZR q.
+    (forall (z: R), a * z ^ 4 + b * z ^ 3 + c * z ^ 2 + d * z + e = a * (z - r1) * (z - r2) * (z - r3) * (z - r4)) ->
+    ((exists (p q: Z), r1 + r2 = IZR p / IZR q) /\ r1 + r2 <> r3 + r4) -> (exists (p q: Z), r1 * r2 = IZR p / IZR q).
 Proof. Admitted.

coq/src/putnam_2003_b6.v

@@ -1,5 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2003_b6
-    : forall (f: R -> R) (x: R), 0 <= x <= 1 -> continuity_pt f x ->
-    RInt (fun x => RInt (fun y => Rabs (f x + f y)) 0 1) 0 1 >= RInt (fun x => Rabs (f x)) 0 1.
+    (f : R -> R)
+    (hf : continuity f)
+    : RInt (fun x => RInt (fun y => Rabs (f x + f y)) 0 1) 0 1 >= RInt (fun x => Rabs (f x)) 0 1.
 Proof. Admitted.

isabelle/putnam_2003_a2.thy

@@ -4,7 +4,8 @@ begin
 (* Note: Boosted domain to infinite set *)
 theorem putnam_2003_a2:
   fixes n::nat and a b::"nat\<Rightarrow>real"
-  assumes abnneg : "\<forall>i \<in> {0..<n}. a i \<ge> 0 \<and> b i \<ge> 0"
+  assumes npos: "n \<ge> 1"
+  and abnneg: "\<forall>i \<in> {0..<n}. a i \<ge> 0 \<and> b i \<ge> 0"
   shows "((\<Prod>i=0..<n. a i) powr (1/n)) + ((\<Prod>i=0..<n. b i) powr (1/n)) \<le> ((\<Prod>i=0..<n. (a i + b i)) powr (1/n))"
   sorry
 

isabelle/putnam_2003_b6.thy

@@ -1,13 +1,12 @@
 theory putnam_2003_b6 imports Complex_Main
-"HOL-Analysis.Lebesgue_Measure"
-"HOL-Analysis.Set_Integral"
+"HOL-Analysis.Interval_Integral"
 begin
 
 theorem putnam_2003_b6:
   fixes f :: "real \<Rightarrow> real"
   assumes hf : "continuous_on UNIV f"
   shows "set_lebesgue_integral lebesgue {(x, y). 0 \<le> x \<and> x \<le> 1 \<and> 0 \<le> y \<and> y \<le> 1} (\<lambda> t :: real \<times> real. \<bar>f (fst t) + f (snd t)\<bar>)
-        \<ge> interval_lebesgue_integral lebesgue 0 1 f"
+        \<ge> interval_lebesgue_integral lebesgue 0 1 (\<lambda>x::real. \<bar>f x\<bar>)"
   sorry
 
 end