Merge pull request #229 from ocfnash/main

Fix a few minor Lean misformalisations

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"
         ]

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_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.
 -/