Merge branch 'main' into rank

coq/src/putnam_1996_a4.v

@@ -5,7 +5,7 @@ Theorem putnam_1996_a4
     (SS : Ensemble (A * A * A))
     (hSdistinct: forall a b c : A, In _ SS (a, b, c) -> a <> b /\ b <> c /\ c <> a)
     (hS1 : forall a b c : A, In _ SS (a, b, c) <-> In _ SS (b, c, a))
-    (hS2 : forall a b c : A, In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a)))
+    (hS2 : forall a b c : A, a <> c -> (In _ SS (a, b, c) <-> ~ (In _ SS (c, b, a))))
     (hS3 : forall a b c d : A, (In _ SS (a, b, c) /\ In _ SS (c, d, a)) <-> (In _ SS (b, c, d) /\ In _ SS (d, a, b)))
     : exists g : A -> R, Injective g /\ (forall a b c : A, g a < g b /\ g b < g c -> In _ SS (a, b, c)).
 Proof. Admitted.

informal/putnam.json

@@ -5044,7 +5044,7 @@
     {
         "problem_name": "putnam_2022_a1",
         "informal_statement": "Determine all ordered pairs of real numbers $(a,b)$ such that the line $y = ax+b$ intersects the curve $y = \\ln(1+x^2)$ in exactly one point.",
-        "informal_solution": "Show that the solution is the set of ordered pairs $(a,b)$ which satisfy at least one of (1) $a = b = 0$, (2) $|a| \\geq 1$, and (3) $0 < |a| < 1$ and $b < \\log(1 - r_{-})^2 - |a|r_{-}$ or $b > \\log(1 + r_{+})^2 + |a|r_{+}$ where $r_{\\pm} = \\frac{1 \\pm \\sqrt{1 - a^2}}{a}$.",
+        "informal_solution": "Show that the solution is the set of ordered pairs $(a,b)$ which satisfy at least one of (1) $a = b = 0$, (2) $|a| \\geq 1$, and (3) $0 < |a| < 1$ and $b < \\log(1 + r_{-}^2) - ar_{-}$ or $b > \\log(1 + r_{+}^2) - ar_{+}$ where $r_{\\pm} = \\frac{1 \\pm \\sqrt{1 - a^2}}{a}$.",
         "tags": [
             "algebra"
         ]

isabelle/putnam_1996_a4.thy

@@ -9,7 +9,7 @@ theorem putnam_1996_a4:
   assumes hA : "CARD('A) = n"
     and hSdistinct: "\<forall>a b c::'A. ((a, b, c) \<in> S \<longrightarrow> (a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c))"
     and hS1 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (b, c, a) \<in> S"
-    and hS2 : " \<forall> a b c :: 'A. (a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S"
+    and hS2 : " \<forall> a b c :: 'A. a \<noteq> c \<longrightarrow> ((a, b, c) \<in> S \<longleftrightarrow> (c, b, a) \<notin> S)"
     and hS3 : " \<forall> a b c d :: 'A. ((a, b, c) \<in> S \<and> (c, d, a) \<in> S) \<longleftrightarrow> ((b, c, d) \<in> S \<and> (d, a, b) \<in> S)"
   shows "\<exists> g :: 'A \<Rightarrow> real. inj g \<and> (\<forall> a b c :: 'A. (g a < g b \<and> g b < g c) \<longrightarrow> (a, b, c) \<in> S)"
   sorry

lean4/src/putnam_1963_a3.lean

@@ -13,7 +13,8 @@ theorem putnam_1963_a3
     (n : ℕ)
     (hn : 0 < n)
     (f y : ℝ → ℝ)
-    (hf : ContinuousOn f (Ici 1)) :
-    ContDiffOn ℝ n y (Ici 1) ∧ (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
+    (hf : ContinuousOn f (Ici 1))
+    (hy : ContDiffOn ℝ n y (Ici 1)) :
+    (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
     ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t :=
   sorry

lean4/src/putnam_1996_a4.lean

@@ -11,7 +11,7 @@ theorem putnam_1996_a4
 (S : Set (A × A × A))
 (hSdistinct : ∀ a b c : A, ⟨a, b, c⟩ ∈ S → a ≠ b ∧ b ≠ c ∧ a ≠ c)
 (hS1 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨b, c, a⟩ ∈ S)
-(hS2 : ∀ a b c : A, ⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S)
+(hS2 : ∀ a b c : A, a ≠ c → (⟨a, b, c⟩ ∈ S ↔ ⟨c, b, a⟩ ∉ S))
 (hS3 : ∀ a b c d : A, (⟨a, b, c⟩ ∈ S ∧ ⟨c, d, a⟩ ∈ S) ↔ (⟨b,c,d⟩ ∈ S ∧ ⟨d,a,b⟩ ∈ S))
 : ∃ g : A → ℝ, Injective g ∧ (∀ a b c : A, g a < g b ∧ g b < g c → ⟨a,b,c⟩ ∈ S) :=
 sorry

lean4/src/putnam_2009_b4.lean

@@ -1,16 +1,17 @@
 import Mathlib
 
-open Topology MvPolynomial Filter Set Metric
+open intervalIntegral MvPolynomial Real
 
 abbrev putnam_2009_b4_solution : ℕ := sorry
 -- 2020050
 /--
 Say that a polynomial with real coefficients in two variables, $x,y$, is \emph{balanced} if the average value of the polynomial on each circle centered at the origin is $0$. The balanced polynomials of degree at most $2009$ form a vector space $V$ over $\mathbb{R}$. Find the dimension of $V$.
 -/
 theorem putnam_2009_b4
-(balanced : MvPolynomial (Fin 2) ℝ → Prop)
-(hbalanced : balanced = fun P ↦ ∀ r > 0, (∫ x in Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) r, MvPolynomial.eval x P) / (2 * Real.pi * r) = 0)
-(V : Set (MvPolynomial (Fin 2) ℝ)) [AddCommGroup V] [Module ℝ V]
-(hV : ∀ P : MvPolynomial (Fin 2) ℝ, P ∈ V ↔ balanced P ∧ P.totalDegree ≤ 2009)
-: (Module.rank ℝ V = putnam_2009_b4_solution) :=
-sorry
+    (IsBalanced : MvPolynomial (Fin 2) ℝ → Prop)
+    (IsBalanced_def : ∀ P, IsBalanced P ↔ ∀ r > 0,
+      (∫ t in (0 : ℝ)..(2 * π), eval ![r * cos t, r * sin t] P) / (2 * π * r) = 0)
+    (V : Submodule ℝ (MvPolynomial (Fin 2) ℝ))
+    (V_def : ∀ P, P ∈ V ↔ IsBalanced P ∧ P.totalDegree ≤ 2009) :
+    Module.rank ℝ V = putnam_2009_b4_solution :=
+  sorry

lean4/src/putnam_2017_a2.lean

@@ -1,11 +1,14 @@
 import Mathlib
 
+open Polynomial
+
 /--
 Let $Q_0(x)=1$, $Q_1(x)=x$, and $Q_n(x)=\frac{(Q_{n-1}(x))^2-1}{Q_{n-2}(x)}$ for all $n \geq 2$. Show that, whenever $n$ is a positive integer, $Q_n(x)$ is equal to a polynomial with integer coefficients.
 -/
 theorem putnam_2017_a2
-(Q : ℕ → ℝ → ℝ)
-(hQbase : ∀ x : ℝ, Q 0 x = 1 ∧ Q 1 x = x)
-(hQn : ∀ n ≥ 2, ∀ x : ℝ, Q n x = ((Q (n - 1) x) ^ 2 - 1) / Q (n - 2) x)
-: ∀ n > 0, ∃ P : Polynomial ℝ, (∀ i : ℕ, P.coeff i = round (P.coeff i)) ∧ Q n = P.eval :=
-sorry
+    (Q : ℕ → RatFunc ℚ)
+    (hQbase : Q 0 = 1 ∧ Q 1 = (X : ℚ[X]))
+    (hQn : ∀ n, Q (n + 2) = (Q (n + 1) ^ 2 - 1) / Q n)
+    (n : ℕ) (hn : 0 < n) :
+    ∃ P : ℤ[X], Q n = P.map (Int.castRingHom ℚ) :=
+  sorry

lean4/src/putnam_2022_a1.lean

@@ -3,7 +3,7 @@ import Mathlib
 open Polynomial
 
 abbrev putnam_2022_a1_solution : Set (ℝ × ℝ) := sorry
--- {(a, b) | (a = 0 ∧ b = 0) ∨ (|a| ≥ 1) ∨ (0 < |a| ∧ |a| < 1 ∧ (b < (Real.log (1 - (1 - Real.sqrt (1 - a^2))/a))^2 - |a| * (1 - Real.sqrt (1 - a^2))/a ∨ b > (Real.log (1 - (1 + Real.sqrt (1 - a^2))/a))^2 - |a| * (1 + Real.sqrt (1 - a^2))/a))}
+-- {(a, b) | (a = 0 ∧ b = 0) ∨ 1 ≤ |a| ∨ (0 < |a| ∧ |a| < 1 ∧ letI rm := (1 - √(1 - a ^ 2)) / a; letI rp := (1 + √(1 - a ^ 2)) / a; (b < Real.log (1 + rm ^ 2) - a * rm ∨ b > Real.log (1 + rp ^ 2) - a * rp))}
 /--
 Determine all ordered pairs of real numbers $(a,b)$ such that the line $y = ax+b$ intersects the curve $y = \ln(1+x^2)$ in exactly one point.
 -/