Merge pull request #148 from trishullab/john

Batch 53 Coq

coq/src/putnam_1963_a2.v

@@ -0,0 +1,9 @@
+Require Import Nat.
+Theorem putnam_1963_a2
+    (f : nat -> nat)
+    (hfpos : forall n : nat, gt (f n) 0)
+    (hfinc : forall i j : nat, gt i 0 -> gt j i -> gt (f j) (f i))
+    (hf2 : f 2 = 2)
+    (hfmn : forall m n : nat, gt m 0 -> gt n 0 -> gcd m n = 1 -> f (m * n) = f m * f n)
+    : (forall (n : nat), n > 0 -> f n = n).
+Proof. Admitted.

coq/src/putnam_1963_a4.v

@@ -0,0 +1,6 @@
+Require Import Reals. From Coquelicot Require Import Rbar Lim_seq.
+Theorem putnam_1963_a4
+    (apos : (nat -> R) -> Prop := fun a : nat -> R => forall n : nat, a n > 0)
+    (f : (nat -> R) -> nat -> R := fun a : nat -> R => fun n : nat => (INR n) * (((1 + a (S n)) / (a n)) - 1))
+    : ((forall a : nat -> R, apos a -> LimSup_seq (f a) >= 1) /\ ~(exists c : R, c > 1 /\ forall a : nat -> R, apos a -> LimSup_seq (f a) >= c)).
+Proof. Admitted.

coq/src/putnam_1963_b1.v

@@ -0,0 +1,9 @@
+Require Import ZArith. From mathcomp Require Import fintype ssralg ssrnat ssrnum poly polydiv.
+Open Scope ring_scope.
+Definition putnam_1963_b1_solution : Z := 2.
+Theorem putnam_1963_b1
+    (R : numDomainType)
+    (ZtoR : Z -> {poly R} := fun a => if (0 <=? a)%Z then (Z.to_nat a)%:R else -(Z.to_nat (-a))%:R)
+    : (forall a : Z, ('X^2 - 'X + ZtoR a) %| ('X^13 + 'X + 90%:R) = true <-> a = putnam_1963_b1_solution).
+Proof. Admitted.
+

coq/src/putnam_1963_b2.v

@@ -0,0 +1,7 @@
+Require Import ZArith Ensembles Reals. From Coquelicot Require Import Hierarchy.
+Definition putnam_1963_b2_solution : Prop := True.
+Theorem putnam_1963_b2
+    (T : Ensemble R := fun x => exists m n : Z, x = (Rpower 2 (IZR m)) * (Rpower 3 (IZR n)))
+    (P : Ensemble R := fun x => x > 0)
+    : ((forall A : Ensemble R, Included R A P -> open A -> A <> Empty_set R -> Intersection R A T <> Empty_set R) <-> putnam_1963_b2_solution).
+Proof. Admitted.

coq/src/putnam_1963_b3.v

@@ -0,0 +1,9 @@
+Require Import Ensembles Reals Rtrigo_def Coquelicot.Coquelicot.
+Open Scope R.
+Definition putnam_1963_b3_solution : Ensemble (R -> R) := 
+    Union (R -> R) (Union (R -> R) (fun f => exists A k : R, f = (fun x => A * sinh (k * x))) (fun f => exists A : R, f = (fun x => A * x))) (fun f => exists A k : R, f = fun x => (A * sin (k * x))).
+Theorem putnam_1963_b3
+    (f : R -> R)
+    (fdiff : forall x, ex_derive f x /\ ex_derive (Derive f) x)
+    : ((forall x y : R, (f x) ^ 2 - (f y) ^ 2 = f (x + y) * f (x - y)) <-> In (R -> R) putnam_1963_b3_solution f).
+Proof. Admitted.

coq/src/putnam_1963_b5.v

@@ -0,0 +1,7 @@
+Require Import Reals ZArith. From Coquelicot Require Import Series Lim_seq Hierarchy Rbar.
+Theorem putnam_1963_b5
+    (a : Z -> R)
+    (haineq : forall n : Z, (n >= 1)%Z -> forall k : Z, ((n <= k)%Z /\ (k <= 2 * n)%Z) -> (0 <= a k /\ a k <= 100 * a n))
+    (haseries : ex_lim_seq (fun nInc => sum_n (fun n => a (Z.of_nat n)) nInc))
+    : (is_lim_seq (fun n : nat => (INR n) * (a (Z.of_nat n))) 0).
+Proof. Admitted.

coq/src/putnam_1963_b6.v

@@ -0,0 +1,10 @@
+Require Import Ensembles. From GeoCoq Require Import Main.Tarski_dev.Ch16_coordinates_with_functions.
+(* Note: This formalization assumes a 3D space; 1D and 2D spaces can be seen as lines and planes in this larger space. *)
+Context `{T3D:Tarski_3D}.
+Theorem putnam_1963_b6
+    (T : Ensemble Tpoint -> Ensemble Tpoint := fun A => (fun r => exists p q, In Tpoint A p /\ In Tpoint A q /\ Bet p r q))
+    (A : nat -> Ensemble Tpoint)
+    (hA0 : (A 0) <> Empty_set Tpoint)
+    (hAn : forall n : nat, n >= 1 -> A n = T (A (n - 1)))
+    : (forall n : nat, n >= 2 -> A n = A (n + 1)).
+Proof. Admitted.

isabelle/putnam_1963_a2.thy

@@ -4,7 +4,7 @@ begin
 theorem putnam_1963_a2:
   fixes f::"nat\<Rightarrow>nat"
   assumes hfpos : "\<forall>n. f n > 0"
-    and hfinc : "strict_mono f"
+    and hfinc : "strict_mono_on {1..} f"
     and hf2 : "f 2 = 2"
     and hfmn : "\<forall>m n. m > 0 \<longrightarrow> n > 0 \<longrightarrow> coprime m n \<longrightarrow> f (m * n) = f m * f n"
   shows "\<forall>n > 0. f n = n"

isabelle/putnam_1963_a4.thy

@@ -5,7 +5,7 @@ theorem putnam_1963_a4:
   fixes apos::"(nat\<Rightarrow>real) \<Rightarrow> bool" and f::"(nat\<Rightarrow>real) \<Rightarrow> nat \<Rightarrow> ereal"
   defines "apos \<equiv> \<lambda>a. \<forall>n. a n > 0"
     and "f \<equiv> \<lambda>a::(nat\<Rightarrow>real). \<lambda>n::nat. ereal (n * (((1 + a (n+1)) / (a n)) - 1))"
-  shows "(\<forall>a::(nat\<Rightarrow>real). apos a \<longrightarrow> (limsup (f a)) \<ge> 1) \<and> (\<exists>a. apos a \<and> (limsup (f a)) = 1)"
+  shows "(\<forall>a::(nat\<Rightarrow>real). apos a \<longrightarrow> (limsup (f a)) \<ge> 1) \<and> \<not>(\<exists> c > 1. \<forall>a. apos a \<longrightarrow> (limsup (f a)) \<ge> c)"
   sorry
 
 end

lean4/src/putnam_1963_a2.lean

@@ -6,7 +6,7 @@ open Topology Filter
 theorem putnam_1963_a2
 (f : ℕ → ℕ)
 (hfpos : ∀ n, f n > 0)
-(hfinc : StrictMono f)
+(hfinc : StrictMonoOn f (Set.Ici 1))
 (hf2 : f 2 = 2)
 (hfmn : ∀ m n, m > 0 → n > 0 → IsRelPrime m n → f (m * n) = f m * f n)
 : ∀ n > 0, f n = n :=

lean4/src/putnam_1963_a4.lean

@@ -6,5 +6,5 @@ open Topology Filter
 theorem putnam_1963_a4
 (apos : (ℕ → ℝ) → Prop := fun a => ∀ n, a n > 0)
 (f : (ℕ → ℝ) → ℕ → ℝ := fun a n => n * (((1 + a (n+1)) / (a n)) - 1))
-: (∀ a, apos a → limsup (f a) ⊤ ≥ 1) ∧ (∃ a, apos a ∧ limsup (f a) ⊤ = 1) :=
+: (∀ a, apos a → limsup (f a) atTop ≥ 1) ∧ (¬∃ c > 1, ∀ a, apos a → limsup (f a) atTop ≥ c) :=
 sorry