Merge pull request #176 from trishullab/john

Coq revisions 2006-2011

coq/src/putnam_2006_a5.v

@@ -1,11 +1,16 @@
 Require Import Nat Reals Coquelicot.Coquelicot.
-Definition putnam_2006_a5_solution (n: nat) := if eqb (n mod 4) (1%nat) then (INR n) else (-1 * INR n).
+Definition putnam_2006_a5_solution (n: nat) := if eqb (n mod 4) (1%nat) then (Z.of_nat n) else (-1 * Z.of_nat n)%Z.
 Theorem putnam_2006_a5
     (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'
+        | O => 1
+        | S n' => m (S n') * prod_n m n'
     end)
-    : forall (n: nat) (th: R), odd n = true /\ ~ exists (p q: Z), th / PI = IZR (p / q) /\
-    let a (k: nat) := tan (th + INR k * PI / INR n) in sum_n a n / prodn a n = putnam_2006_a5_solution n.
+    (n : nat)
+    (th : R)
+    (a : nat -> R)
+    (nodd : odd n = true)
+    (thetairr : ~ exists (p q: Z), th / PI = IZR (p / q))
+    (ha : forall k, a k = tan (th + (INR k * PI) / INR n))
+    : sum_n_m a 1 n / prodn a n = IZR (putnam_2006_a5_solution n).
 Proof. Admitted.

coq/src/putnam_2006_b2.v

@@ -5,6 +5,6 @@ Theorem putnam_2006_b2
     (X : list R)
     (hXcard : length X = n)
     : exists (presS: R -> Prop) (m: Z) (S: list R), 
-    (neq (length S) 0) /\ (forall (x: R), In x S <-> (In x X /\ presS x)) /\
+    (neq (length S) 0) /\ NoDup S /\ (forall (x: R), In x S <-> (In x X /\ presS x)) /\
     (Rabs (IZR m + (fold_left Rplus S 0)) <= 1 / INR (n + 1)).
 Proof. Admitted.

coq/src/putnam_2006_b5.v

@@ -5,7 +5,7 @@ Theorem putnam_2006_b5
     (I : (R -> R) -> R := fun f => RInt (fun x => x ^ 2 * f x) 0 1)
     (J : (R -> R) -> R := fun f => RInt (fun x => x * (f x) ^ 2) 0 1)
     (m: R)
-    (hm : exists (f: R -> R) (x: R), 0 <= x <= 1 /\ continuity_pt f x /\ m = I f - J f)
-    (hmub : forall (f: R -> R) (x: R), 0 <= x <= 1 /\ continuity_pt f x /\ m >= I f - J f)
+    (hm : exists (f: R -> R), (forall (x: R), 0 <= x <= 1 -> continuity_pt f x) /\ m = I f - J f)
+    (hmub : forall (f: R -> R), (forall (x: R), 0 <= x <= 1 -> continuity_pt f x) -> m >= I f - J f)
     : m = putnam_2006_b5_solution.
 Proof. Admitted.

coq/src/putnam_2006_b6.v

@@ -8,7 +8,7 @@ Theorem putnam_2006_b6
     (A := fix a (n: nat) : R :=
         match n with
         | O => a0
-        | S n' => a n' + 1 / (a n') ^ (1 / k)
+        | S n' => a n' + Rpower (1 / (a n')) (1 / INR k)
     end)
     : Lim_seq (fun n => (A n) ^ (k + 1) / INR n ^ k) = putnam_2006_b6_solution k.
 Proof. Admitted.

coq/src/putnam_2007_a4.v

@@ -1,9 +1,9 @@
 Require Import Reals Zpower Coquelicot.Coquelicot.
-Definition putnam_2007_a4_solution (f: R -> R) := exists (c d: Z), Z.ge d 0 /\ Z.ge c (1 - d) /\ f = (fun n => (IZR (Zpower 10 c) * IZR (Zpower (9 * floor n + 1) d) - 1) / 9).
+Definition putnam_2007_a4_solution (f: R -> R) := exists (c d: Z), Z.ge d 0 /\ Z.ge c (1 - d) /\ f = (fun n => (Rpower 10 (IZR c) * Rpower (9 * n + 1) (IZR d) - 1) / 9).
 Theorem putnam_2007_a4
     (repunit : R -> Prop := fun n => n = IZR (floor n) /\ n > 0 /\ exists (m: nat), n = sum_n (fun i => 10 ^ i) m)
     (c: nat -> R)
     (n: nat)
-    (f : R -> R := fun x => sum_n (fun i => c i * x ^ i) (n + 1))
-    : repunit (INR n) -> repunit (f (INR n)) <-> putnam_2007_a4_solution f.
+    (f : R -> R := fun x => sum_n (fun i => c i * x ^ i) n)
+    : (forall (n: nat), repunit (INR n) -> repunit (f (INR n))) <-> putnam_2007_a4_solution f.
 Proof. Admitted.

coq/src/putnam_2007_b1.v

@@ -3,7 +3,8 @@ Theorem putnam_2007_b1
     (c: nat -> nat)
     (n: nat)
     (hn : gt n 0)
-    (f : nat -> R := fun x => sum_n (fun i => INR (mul (c i) (x ^ i))) (n + 1))
+    (k: nat)
+    (f : nat -> R := fun x => sum_n (fun i => INR (mul (c i) (x ^ i))) (k + 1))
     : forall (x: nat), gt (c x) 0 ->
     Z.to_nat (floor (f n)) %| Z.to_nat (floor (f (Z.to_nat (floor (f n + 1))))) = true <-> n = 1%nat.
 Proof. Admitted.

coq/src/putnam_2007_b2.v

@@ -1,8 +1,9 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2007_b2
     (f: R -> R)
-    (hf : forall (x: R), 0 <= x <= 1 /\ continuity_pt f x /\ ex_derive f x /\ RInt f 0 1 = 0)
+    (hf : (forall (x: R), 0 <= x <= 1 -> ex_derive f x /\ continuity_pt (Derive f) x) /\ RInt f 0 1 = 0)
     (max_f_prime_abs: R)
-    : (forall (x: R), 0 <= x <= 1 -> max_f_prime_abs >= Rabs (Derive f x)) /\ (exists (x: R), 0 <= x <= 1 -> max_f_prime_abs = Rabs (Derive f x)) /\
-    forall (a: R), 0 < a < 1 -> Rabs (RInt f 0 a) = max_f_prime_abs / 8. 
+    (heqmax: exists (x: R), 0 <= x <= 1 -> max_f_prime_abs = Rabs (Derive f x))
+    (hmaxub: forall (x: R), 0 <= x <= 1 -> max_f_prime_abs >= Rabs (Derive f x))
+    : forall (a: R), 0 < a < 1 -> Rabs (RInt f 0 a) <= max_f_prime_abs / 8.
 Proof. Admitted.

coq/src/putnam_2007_b3.v

@@ -1,10 +1,10 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2007_b3_solution := let a := (1 + sqrt 5) / 2 in 2 ^ 2006 / sqrt 5 * (a ^ 3997 - Rpower a (-3997)).
+Definition putnam_2007_b3_solution := let a := (1 + sqrt 5) / 2 in (2 ^ 2006 / sqrt 5) * (a ^ 3997 - Rpower a (-3997)).
 Theorem putnam_2007_b3
     (X := fix x (n: nat) :=
         match n with
         | O => 1
-        | S n' => 3 * x n' + IZR (floor (x n' * sqrt (INR n)))
+        | S n' => 3 * x n' + IZR (floor (x n' * sqrt 5))
     end)
     : X 2007%nat = putnam_2007_b3_solution.
 Proof. Admitted.

coq/src/putnam_2008_a1.v

@@ -1,7 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2008_a1
     (f : R -> R -> R)
-    (x y z: R)
-    (hf : f x y + f y z + f z x = 0)
+    (hf : forall (x y z: R), f x y + f y z + f z x = 0)
     : exists (g: R -> R), forall (x y: R), f x y = g x - g y.
 Proof. Admitted.

coq/src/putnam_2008_a4.v

@@ -3,5 +3,5 @@ Definition putnam_2008_a4_solution := False.
 Theorem putnam_2008_a4
     (f : R -> R)
     (hf : forall (x : R), f x = (if (Rle_dec x (exp 1)) then x else x * f (ln x)))
-    : ex_lim_seq (fun nInc => sum_n (fun n => 1 / f (INR n)) nInc) <-> putnam_2008_a4_solution.
+    : ex_lim_seq (fun nInc => sum_n_m (fun n => 1 / f (INR n)) 1 nInc) <-> putnam_2008_a4_solution.
 Proof. Admitted.

coq/src/putnam_2008_b4.v

@@ -1,10 +1,10 @@
-Require Import Nat Reals Coquelicot.Coquelicot.
+Require Import Nat ZArith Reals Coquelicot.Coquelicot.
 Theorem putnam_2008_b4
     (p: nat)
     (hp : Znumtheory.prime (Z.of_nat p))
     (c: nat -> Z)
     (n: nat)
-    (h : nat -> nat := fun x => Z.to_nat (floor (sum_n (fun i => IZR (c i) * INR (x ^ i)) (n + 1))))
-    : (forall (i j: nat), i <> j /\ and (le 0 i) (le i (p ^ 2 - 1)) /\ and (le 0 j) (le j (p ^ 2 - 1)) -> (h i) mod (p ^ 2) <> h j mod p ^ 2) ->
-    (forall (i j: nat), i <> j /\ and (le 0 i) (le i (p ^ 3 - 1)) /\ and (le 0 j) (le j (p ^ 3 - 1)) -> h i mod p ^ 2 <> h j mod p ^ 3).
+    (h : nat -> Z := fun x => floor (sum_n (fun i => IZR (c i) * INR (x ^ i)) n))
+    (hh : forall (i j: nat), i <> j /\ and (le 0 i) (le i (p ^ 2 - 1)) /\ and (le 0 j) (le j (p ^ 2 - 1)) -> Z.modulo (h i) (Z.of_nat (p ^ 2)) <> Z.modulo (h j) (Z.of_nat (p ^ 2)))
+    : (forall (i j: nat), i <> j /\ and (le 0 i) (le i (p ^ 3 - 1)) /\ and (le 0 j) (le j (p ^ 3 - 1)) -> Z.modulo (h i) (Z.of_nat (p ^ 3)) <> Z.modulo (h j) (Z.of_nat (p ^ 3))).
 Proof. Admitted.

coq/src/putnam_2008_b5.v

@@ -1,8 +1,8 @@
-Require Import Reals Coquelicot.Coquelicot. From mathcomp Require Import div.
+Require Import Reals QArith Coquelicot.Coquelicot. From mathcomp Require Import div.
 Open Scope R.
-Definition putnam_2008_b5_solution (f : R -> R) := exists n : Z, f = (fun x => x + IZR n) /\ f = (fun x => -x + IZR n).
+Definition putnam_2008_b5_solution (f : R -> R) := exists n : Z, f = (fun x => x + IZR n) \/ f = (fun x => -x + IZR n).
 Theorem putnam_2008_b5
     (f: R -> R)
-    (hf : continuity f)
-    : forall (x: R), ex_derive f x -> forall (q: R), exists (n1 n2 d: nat), q = INR (n1 / d) /\ f q = INR (n2 / d) /\ coprime n1 d = true /\ coprime n2 d = true <-> putnam_2008_b5_solution f.
+    (hf : (forall x: R, ex_derive f x) /\ continuity (Derive f))
+    : (forall (q: Q), exists (n1 n2 d: nat), Q2R q = INR n1 / INR d /\ f (Q2R q) = INR n2 / INR d /\ coprime n1 d = true /\ coprime n2 d = true) <-> putnam_2008_b5_solution f.
 Proof. Admitted.

coq/src/putnam_2008_b6.v

@@ -5,5 +5,5 @@ Theorem putnam_2008_b6
     (hk : k > 0)
     (klimited : {perm 'I_n} -> Prop := fun sigma => forall (i: 'I_n), Rle (Rabs (INR (nat_of_ord (sigma i)) - INR i)) (INR k))
     (E : Ensemble {perm 'I_n} := fun p =>  klimited p)
-    : exists (sz: nat), cardinal {perm 'I_n} E sz /\ Nat.odd sz <-> n mod (2 * k + 1) = 0 \/ n mod (2 * k + 1) = 1.
+    : (exists (sz: nat), cardinal {perm 'I_n} E sz /\ Nat.odd sz) <-> n mod (2 * k + 1) = 0 \/ n mod (2 * k + 1) = 1.
 Proof. Admitted.

coq/src/putnam_2009_a1.v

@@ -3,8 +3,8 @@ Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
 Open Scope R.
 Definition putnam_2009_a1_solution := True.
 Theorem putnam_2009_a1
-    (f: Tpoint -> R)
-    : ((forall (A B C D: Tpoint), Square A B C D -> 
+    : (forall f: Tpoint -> R, 
+    (forall (A B C D: Tpoint), Square A B C D -> 
     f A + f B + f C + f D = 0) ->
     forall (P : Tpoint), f P = 0) <->
     putnam_2009_a1_solution.

coq/src/putnam_2009_a2.v

@@ -1,13 +1,12 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2009_a2_solution : (R -> R) := fun x => Rpower 2 (-1 / 12) * (sin (6 * x + PI / 4) / (cos (6 * x + PI / 4)) ^ 2) ^ (1 / 6).
+Definition putnam_2009_a2_solution : (R -> R) := fun x => Rpower 2 (-1 / 12) * Rpower (sin (6 * x + PI / 4) / (cos (6 * x + PI / 4)) ^ 2) (1 / 6).
 Theorem putnam_2009_a2
     (f g h: R -> R) 
     (a b: R)
-    (hab : a < b)
-    : forall (x: R), a < x < b -> 
-    (ex_derive f x /\ ex_derive g x /\ ex_derive h x /\
-    Derive f x = 2 * f (f (g (h x))) + 1 / g (h x) /\ f 0 = 1 /\
-    Derive g x = 2 * f (g (g (h x))) + 4 / f (h x) /\ g 0 = 1 /\
-    Derive h x = 3 * f (g (h (h x))) + 1 / f (g x) /\ h 0 = 1) ->
-    f = putnam_2009_a2_solution.
+    (hab : a < 0 < b)
+    (hdiff : forall (x: R), a < x < b -> ex_derive f x /\ ex_derive g x /\ ex_derive h x)
+    (hf : forall (x: R), a < x < b -> Derive f x = 2 * (f x)^2 * (g x) * (h x) + 1 / ((g x) * (h x)) /\ f 0 = 1)
+    (hg : forall (x: R), a < x < b -> Derive g x = (f x) * (g x)^2 * (h x) + 4 / ((f x) * (h x)) /\ g 0 = 1)
+    (hh : forall (x: R), a < x < b -> Derive h x = 3 * (f x) * (g x) * (h x)^2 + 1 / ((f x) * (g x)) /\ h 0 = 1)
+    : exists (c d: R), c < 0 < d /\ (forall (x: R), c < x < d -> f x = putnam_2009_a2_solution x).
 Proof. Admitted.

coq/src/putnam_2009_a4.v

@@ -1,7 +1,5 @@
 Require Import Ensembles QArith.
 Definition putnam_2009_a4_solution := False.
 Theorem putnam_2009_a4
-    (E: Ensemble Q)
-    (hE : E 0 /\ forall (q: Q), (E q -> E (q + 1) /\ E (q - 1)) /\ (E q /\ q <> 0 /\ q <> 1 -> E (1 / (q * (q - 1)))))
-    : forall (q: Q), E q <-> putnam_2009_a4_solution.
+    : (forall (E: Ensemble Q), (E 0 /\ forall (q: Q), (E q -> E (q + 1) /\ E (q - 1)) /\ (E q /\ q <> 0 /\ q <> 1 -> E (1 / (q * (q - 1))))) -> forall (q: Q), E q) <-> putnam_2009_a4_solution.
 Proof. Admitted.

coq/src/putnam_2009_b5.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2009_b5
     (f: R -> R) 
-    (hf : R -> Prop := fun x => (1 < x /\ ex_derive f x /\ Derive f x = (x ^ 2 - (f x) ^ 2) / (x ^ 2  * ((f x) ^ 2 + 1))))
-    : filterlim (fun n : nat => f (INR n)) eventually (Rbar_locally p_infty).
+    (hf : forall (x: R), 1 < x -> (ex_derive f x /\ Derive f x = (x ^ 2 - (f x) ^ 2) / (x ^ 2 * ((f x) ^ 2 + 1))))
+    : is_lim f p_infty p_infty.
 Proof. Admitted.

coq/src/putnam_2009_b6.v

@@ -1,6 +1,6 @@
 Require Import List ZArith Coquelicot.Coquelicot.
 Open Scope Z.
 Theorem putnam_2009_b6
-    : forall (n: Z), n > 0 -> exists (a: list Z), length a = 2009%nat /\ nth 0 a 0 = 0 /\ nth 2008 a 0 = n /\
-    forall (i: nat), and (le 1 i) (lt i 2009) -> exists (j: nat), and (le 0 j) (lt j i) /\ ((exists (k: Z), k > 0 /\ nth i a 0 = nth j a 0 + 2 ^ k) \/ exists (b c: Z), b > 0 /\ c > 0 /\ nth i a 0 = b mod c). 
+    : forall (n: Z), n > 0 -> exists (a: list Z), length a = 2010%nat /\ nth 0 a 0 = 0 /\ nth 2009 a 0 = n /\
+    forall (i: nat), and (le 1 i) (le i 2009) -> (exists (j: nat), lt j i /\ (exists (k: Z), k >= 0 /\ nth i a 0 = nth j a 0 + 2 ^ k)) \/ exists (b c: nat), lt b i /\ lt c i /\ nth b a 0 > 0 /\ nth c a 0 > 0 /\ nth i a 0 = (nth b a 0) mod (nth c a 0).
 Proof. Admitted.

coq/src/putnam_2010_a2.v

@@ -2,5 +2,5 @@ Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2010_a2_solution (f: R -> R) := exists (c d: R), f = (fun x => c * x + d).
 Theorem putnam_2010_a2
     (f: R -> R)
-    : forall (x: R) (n: nat), Derive f x = (f (x + (INR n)) - f x) / (INR n) <-> putnam_2010_a2_solution f.
+    : (forall (x: R) (n: nat), gt n 0 -> ex_derive f x /\ Derive f x = (f (x + (INR n)) - f x) / (INR n)) <-> putnam_2010_a2_solution f.
 Proof. Admitted.

coq/src/putnam_2010_a6.v

@@ -1,7 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2010_a6
     (f: R -> R)
-    (x y: R)
-    (hf : x >= 0 /\ x < y -> f x > f y /\ continuity_pt f x /\ Lim_seq (fun n => f (INR n)) = 0)
-    : ~ ex_lim_seq (fun nInc => RInt (fun x => (f x - f (x + 1)) / f x) 0 (INR nInc)).
+    (hf : (forall (x: R), x >= 0 -> (forall (y: R), x < y -> f x > f y) /\ continuity_pt f x) /\ is_lim f p_infty 0)
+    : ~ ex_finite_lim (fun nInc => RInt (fun x => (f x - f (x + 1)) / f x) 0 nInc) p_infty.
 Proof. Admitted.

coq/src/putnam_2010_b1.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2010_b1_solution := False.
 Theorem putnam_2010_b1
-    : exists (a: nat -> R), forall (m: nat), gt m 0 -> Series (fun i => (a i) ^ m) = (INR m) <-> putnam_2010_b1_solution.
+    : (exists (a: nat -> R), forall (m: nat), gt m 0 -> Series (fun i => (a i) ^ m) = (INR m)) <-> putnam_2010_b1_solution. 
 Proof. Admitted.

coq/src/putnam_2010_b2.v

@@ -1,16 +1,16 @@
-Require Import Reals Rgeom ZArith GeoCoq.Main.Tarski_dev.Ch16_coordinates_with_functions.
-Context `{T2D:Tarski_2D} `{TE:@Tarski_euclidean Tn TnEQD}.
+Require Import Reals Rgeom ZArith.
 Open Scope R.
 Definition putnam_2010_b2_solution := 3.
 Theorem putnam_2010_b2
-    (pt_to_R : Tpoint -> (R * R))
-    (int_val : Tpoint -> Prop := fun P => exists (x y : Z), pt_to_R P = (IZR x, IZR y))
-    (dist : Tpoint -> Tpoint -> R := fun A B => let (a, b) := pt_to_R A in let (c, d) := pt_to_R B in dist_euc a b c d)
-    (p : Tpoint -> Tpoint -> Tpoint -> Prop :=
-        fun A B C => ~ Col A B C /\ int_val A /\ int_val B /\ int_val C /\
-        exists (z: Z), dist A B = IZR z /\ dist A C = IZR z /\ dist B C = IZR z)
-    (m : Z)
-    (hm : exists (A B C: Tpoint), p A B C)
-    (hmlb : forall (A B C: Tpoint), p A B C -> dist A B >= IZR m)
-    : IZR m = putnam_2010_b2_solution.
+    (dist : (R * R) -> (R * R) -> R := fun A B => let (a, b) := A in let (c, d) := B in dist_euc a b c d)
+    (int_val : (R * R) -> Prop := fun P => exists (x y : Z), P = (IZR x, IZR y))
+    (noncollinear: (R * R) -> (R * R) -> (R * R) -> Prop := fun A B C => let (a, b) := A in let (c, d) := B in let (e, f) := C in
+        ~exists (s t : R), (s * (c - a) + t * (e - a), s * (d - b) + t * (f - b)) = (0, 0))
+    (p : (R * R) -> (R * R) -> (R * R) -> Prop :=
+        fun A B C => noncollinear A B C /\ int_val A /\ int_val B /\ int_val C /\
+        (exists (x : Z), dist A B = IZR x) /\ (exists (y : Z), dist A C = IZR y) /\ (exists (z : Z), dist B C = IZR z))
+    (m : R)
+    (hm : exists (A B C: R * R), p A B C /\ dist A B = m)
+    (hmlb : forall (A B C: R * R), p A B C -> dist A B >= m)
+    : m = putnam_2010_b2_solution.
 Proof. Admitted.

coq/src/putnam_2010_b4.v

@@ -1,8 +1,8 @@
 Require Import Reals Coquelicot.Coquelicot.
-Definition putnam_2010_b4_solution (c1 c2: nat -> R) (n m: nat) := exists (a b c d: R), b * c - a  * d = 1 /\ n = 1%nat /\ m = 1%nat /\ c1 = (fun x => match x with | O => b | S O => a | _ => 0 end) /\ c2 = (fun x => match x with | O => d | S O => c | _ => 0 end).
+Definition P : (nat -> R) -> nat -> R -> R := fun c n x => sum_n (fun i => c i * x ^ i) n.
+Definition putnam_2010_b4_solution (c1 c2: nat -> R) (n m: nat) := exists (a b c d: R), b * c - a * d = 1 /\ P c1 n = (fun x => a * x + b) /\ P c2 m = (fun x => c * x + d).
 Theorem putnam_2010_b4
-    (P : (nat -> R) -> nat -> R -> R := fun c n x => sum_n (fun i => c i * x ^ i) (n + 1))
     (c1 c2: nat -> R)
     (n m: nat)
-    : forall (x: R), (P c1 n x) * (P c2 m (x + 1)) - (P c1 n (x + 1)) * (P c2 m x) = 1 <-> putnam_2010_b4_solution c1 c2 n m.
+    : (forall (x: R), (P c1 n x) * (P c2 m (x + 1)) - (P c1 n (x + 1)) * (P c2 m x) = 1) <-> putnam_2010_b4_solution c1 c2 n m.
 Proof. Admitted.

coq/src/putnam_2010_b5.v

@@ -1,5 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2010_b5_solution := False.
 Theorem putnam_2010_b5
-    : exists (f: R -> R), forall (x y: R), x < y -> f x < f y /\ Derive f x = f (f x) <-> putnam_2010_b5_solution.
+    : (exists (f: R -> R), forall (x y: R), (x < y -> f x < f y) /\ ex_derive f x /\ Derive f x = f (f x)) <-> putnam_2010_b5_solution.
 Proof. Admitted.

coq/src/putnam_2011_a2.v

@@ -4,14 +4,15 @@ Theorem putnam_2011_a2
     (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)
     (a: nat -> R)
+    (ha1 : a 0%nat = 1)
     (B := fix b (n: nat) :=
         match n with
         | O => 1
         | S n' => b n' * a n - 2
     end)
-    (M: nat)
-    : (forall (n: nat), a n > 0 /\ B n > 0 /\ -1 * INR M <= B n <= INR M) -> Series (fun n => prodn a n) = putnam_2011_a2_solution.
+    (M: R)
+    : (forall (n: nat), a n > 0 /\ B n > 0 /\ -1 * M <= B n <= M) -> Series (fun n => 1 / prodn a n) = putnam_2011_a2_solution.
 Proof. Admitted.

coq/src/putnam_2011_a3.v

@@ -1,7 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
+(* Note: There may be multiple possible correct answers. *)
 Definition putnam_2011_a3_solution := (-1, 2 / PI).
 Theorem putnam_2011_a3
-    (c L: R)
-    (hL : L > 0)
-    : Lim_seq (fun r => (Rpower (INR r) c * RInt (fun x => x ^ r * sin x) 0 PI / 2) / (RInt (fun x => x ^ r * cos x) 0 PI / 2)) = L <-> (c, L) = putnam_2011_a3_solution.
+    : let (c, L) := putnam_2011_a3_solution in L > 0 /\ is_lim_seq (fun r => (Rpower (INR r) c * RInt (fun x => x ^ r * sin x) 0 (PI / 2)) / (RInt (fun x => x ^ r * cos x) 0 (PI / 2))) L.
 Proof. Admitted.

coq/src/putnam_2011_b1.v

@@ -1,4 +1,4 @@
 Require Import Reals ZArith Coquelicot.Coquelicot.
 Theorem putnam_2011_b1
-    : forall (h k: Z), Z.gt h 0 /\ Z.gt k 0 -> forall (ep: R), ep > 0 /\ exists (m n: Z), ep < Rabs (IZR h * sqrt (IZR m) - IZR k * sqrt (IZR n)) < 2 * ep.
+    : forall (h k: Z), Z.gt h 0 /\ Z.gt k 0 -> forall (ep: R), ep > 0 -> exists (m n: Z), Z.gt m 0 /\ Z.gt n 0 /\ ep < Rabs (IZR h * sqrt (IZR m) - IZR k * sqrt (IZR n)) < 2 * ep.
 Proof. Admitted.

coq/src/putnam_2011_b3.v

@@ -1,7 +1,5 @@
 Require Import Reals Coquelicot.Coquelicot.
 Definition putnam_2011_b3_solution := True.
 Theorem putnam_2011_b3
-    (f g : R -> R)
-    (hfg : forall (a b : R), (a < 0 < b /\ forall (x: R), a < x < b -> g x > 0 /\ continuity_pt g 0 /\ ex_derive f (g 0) /\ ex_derive (fun x => f x / g x) 0))
-    : ex_derive f 0 <-> putnam_2011_b3_solution.
+    : (forall (f g : R -> R), g 0 <> 0 /\ continuity_pt g 0 /\ ex_derive (fun x : R => f x * g x) 0 /\ ex_derive (fun x : R => f x / g x) 0 -> ex_derive f 0) <-> putnam_2011_b3_solution.
 Proof. Admitted.

coq/src/putnam_2011_b5.v

@@ -1,6 +1,6 @@
 Require Import Reals Coquelicot.Coquelicot.
 Theorem putnam_2011_b5
     (a: nat -> R)
-    (ha : exists (A: R), forall (n: nat), Lim_seq (fun nInc => (RInt (fun x => (sum_n (fun i => 1 / (1 + (x - a i) ^ 2)) n)) (-1 * INR nInc) (INR nInc)) ^ 2) <= A * INR n)
-    : exists (B: R), B > 0 /\ forall (n: nat), sum_n (fun i => (sum_n (fun j => 1 + (a i - a j) ^ 2)) n) n >= B * INR n ^ 3.
+    (ha : exists (A: R), forall (n: nat), exists (L : R), is_lim_seq (fun nInc => (RInt (fun x => (sum_n_m (fun i => 1 / (1 + (x - a i) ^ 2)) 1 n) ^ 2) (-1 * INR nInc) (INR nInc))) L /\ L <= A * INR n)
+    : exists (B: R), B > 0 /\ forall (n: nat), sum_n_m (fun i => (sum_n_m (fun j => 1 + (a i - a j) ^ 2)) 1 n) 1 n >= B * INR n ^ 3.
 Proof. Admitted.

coq/src/putnam_2011_b6.v

@@ -3,8 +3,6 @@ Open Scope nat_scope.
 Theorem putnam_2011_b6 
     (p: nat)
     (hp : prime (Z.of_nat p) /\ odd p = true)
-    (l := seq 0 p)
-    (E: Ensemble nat)
-    : (forall (n: nat), E n -> and (le 0 n) (lt n p)) /\ cardinal nat E ((p + 1) / 2) /\
-    forall (n: nat), E n -> Z.to_nat (floor (sum_n (fun k => INR (fact k * n ^ k)) p)) mod p <> 0.
+    : exists (E: Ensemble nat), (forall (n: nat), E n -> lt n p) /\ cardinal nat E ((p + 1) / 2) /\
+    forall (n: nat), E n -> Z.to_nat (floor (sum_n (fun k => INR (fact k * n ^ k)) (p - 1))) mod p <> 0.
 Proof. Admitted.

isabelle/putnam_2011_a2.thy

@@ -2,7 +2,7 @@ theory putnam_2011_a2 imports Complex_Main
 begin
 
 definition putnam_2011_a2_solution :: real where "putnam_2011_a2_solution \<equiv> undefined"
-(* 2/pi *)
+(* 3/2 *)
 theorem putnam_2011_a2:
   fixes a b :: "nat \<Rightarrow> real"
   assumes habn: "\<forall>n::nat. a n > 0 \<and> b n > 0"