Merge pull request #206 from ocfnash/main

Fix a few minor Lean misformalisations

lean4/src/putnam_1967_b1.lean

@@ -12,7 +12,7 @@ theorem putnam_1967_b1
 (hR : R = midpoint ℝ (L 5) (L 0))
 (hr : r > 0)
 (hcyclic : ∃ (O : EuclideanSpace ℝ (Fin 2)), ∀ i : ZMod 6, dist O (L i) = r)
-(horder : ∀ i j : ZMod 6, i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)
+(horder : ∀ i j : ZMod 6, i ≠ j → i + 1 = j ∨ i = j + 1 ∨ segment ℝ (L i) (L j) ∩ interior (convexHull ℝ {L k | k : ZMod 6}) ≠ ∅)
 (hlens : dist (L 0) (L 1) = r ∧ dist (L 2) (L 3) = r ∧ dist (L 4) (L 5) = r)
 (hdist : L 1 ≠ L 2 ∧ L 3 ≠ L 4 ∧ L 5 ≠ L 0)
 : dist P Q = dist R P ∧ dist Q R = dist P Q :=

lean4/src/putnam_1989_a1.lean

@@ -1,10 +1,10 @@
 import Mathlib
 open BigOperators
 
-abbrev putnam_1989_a1_solution : ℕ := sorry
+abbrev putnam_1989_a1_solution : ℕ∞ := sorry
 -- 1
 theorem putnam_1989_a1
-(pdigalt : List ℕ → Prop)
-(hpdigalt : ∀ pdig : List ℕ, pdigalt pdig = Odd pdig.length ∧ (∀ i : Fin pdig.length, pdig.get i = if Even (i : ℕ) then 1 else 0))
-: {p : ℕ | p > 0 ∧ p.Prime ∧ pdigalt (Nat.digits 10 p)}.encard = putnam_1989_a1_solution :=
-sorry
+    (pdigalt : List ℕ → Prop)
+    (hpdigalt : ∀ l, pdigalt l ↔ Odd l.length ∧ (∀ i, l.get i = if Even (i : ℕ) then 1 else 0)) :
+    {p : ℕ | p.Prime ∧ pdigalt (Nat.digits 10 p)}.encard = putnam_1989_a1_solution :=
+  sorry

lean4/src/putnam_1990_b5.lean

@@ -1,12 +1,12 @@
 import Mathlib
 open BigOperators
 
-open Filter Topology Nat
+open Filter Polynomial Topology Nat
 
 abbrev putnam_1990_b5_solution : Prop := sorry
 -- True
-theorem putnam_1990_b5
-(anpoly : (ℕ → ℝ) → ℕ → Polynomial ℝ)
-(hanpoly : ∀ (a : ℕ → ℝ) (n : ℕ), (anpoly a n).degree = n ∧ (∀ i : Fin (n + 1), (anpoly a n).coeff i = a i))
-: (∃ a : ℕ → ℝ, (∀ i : ℕ, a i ≠ 0) ∧ (∀ n ≥ 1, {r : ℝ | (anpoly a n).eval r = 0}.encard = n)) ↔ putnam_1990_b5_solution :=
-sorry
+theorem putnam_1990_b5 :
+    (∃ a : ℕ → ℝ, (∀ i, a i ≠ 0) ∧
+      (∀ n ≥ 1, (∑ i in Finset.Iic n, a i • X ^ i : Polynomial ℝ).roots.toFinset.card = n)) ↔
+    putnam_1990_b5_solution :=
+  sorry

lean4/src/putnam_1991_a6.lean

@@ -9,12 +9,12 @@ theorem putnam_1991_a6
 (agt bge bg1 bg2 : ℕ × (ℕ → ℕ) → Prop)
 (A g B: ℕ → ℕ)
 (hnabsum : ∀ n ≥ 1, ∀ ab : ℕ × (ℕ → ℕ), nabsum n ab = (ab.1 ≥ 1 ∧ (∀ i < ab.1, ab.2 i > 0) ∧ (∀ i ≥ ab.1, ab.2 i = 0) ∧ (∑ i : Fin ab.1, ab.2 i) = n))
-(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a = (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ a.2 (a.1 - 2) > a.2 (a.1 - 1))
+(hagt : ∀ a : ℕ × (ℕ → ℕ), agt a ↔ (∀ i : Fin (a.1 - 2), a.2 i > a.2 (i + 1) + a.2 (i + 2)) ∧ 1 < a.1 → a.2 (a.1 - 2) > a.2 (a.1 - 1))
 (hA : ∀ n ≥ 1, A n = {a : ℕ × (ℕ → ℕ) | nabsum n a ∧ agt a}.encard)
 (hbge : ∀ b : ℕ × (ℕ → ℕ), bge b = ∀ i : Fin (b.1 - 1), b.2 i ≥ b.2 (i + 1))
 (hg : g 0 = 1 ∧ g 1 = 2 ∧ (∀ j ≥ 2, g j = g (j - 1) + g (j - 2) + 1))
-(hbg1 : ∀ b : ℕ × (ℕ → ℕ), bg1 b = ∀ i : Fin b.1, ∃ j : ℕ, b.2 i = g j)
-(hbg2 : ∀ b : ℕ × (ℕ → ℕ), bg2 b = ∃ k : ℕ, b.2 0 = g k ∧ (∀ j ≤ k, ∃ i : Fin b.1, b.2 i = g j))
+(hbg1 : ∀ b : ℕ × (ℕ → ℕ), bg1 b ↔ ∀ i : Fin b.1, ∃ j : ℕ, b.2 i = g j)
+(hbg2 : ∀ b : ℕ × (ℕ → ℕ), bg2 b ↔ ∃ k : ℕ, b.2 0 = g k ∧ (∀ j ≤ k, ∃ i : Fin b.1, b.2 i = g j))
 (hB : ∀ n ≥ 1, B n = {b : ℕ × (ℕ → ℕ) | nabsum n b ∧ bge b ∧ bg1 b ∧ bg2 b}.encard)
 : ∀ n ≥ 1, A n = B n :=
 sorry

lean4/src/putnam_1992_b2.lean

@@ -4,7 +4,8 @@ open BigOperators
 open Topology Filter Nat Function Polynomial
 
 theorem putnam_1992_b2
-(Q : ℕ → ℕ → ℕ)
-(hQ : Q = fun n k ↦ coeff ((1 + X + X ^ 2 + X ^ 3) ^ n) k)
-: (∀ n k : ℕ, Q n k = ∑ j : Finset.range (k + 1), choose n j * choose n (k - 2 * j)) :=
-sorry
+    (Q : ℕ → ℕ → ℕ)
+    (hQ : Q = fun n k ↦ coeff ((1 + X + X ^ 2 + X ^ 3) ^ n) k)
+    (n k : ℕ) :
+    Q n k = ∑ j in Finset.Iic k, choose n j * (if 2 * j ≤ k then choose n (k - 2 * j) else 0) :=
+  sorry

lean4/src/putnam_1999_a3.lean

@@ -4,9 +4,10 @@ open BigOperators
 open Filter Topology Metric
 
 theorem putnam_1999_a3
-(f : ℝ → ℝ)
-(hf : f = fun x => 1/(1 - 2 * x - x^2))
-(a : ℕ → ℝ)
-(hf : ∃ ε > 0, ∀ x ∈ ball 0 ε, Tendsto (λ n => ∑ i in Finset.range n, (a n) * x^n) atTop (𝓝 (f x)))
-: ∀ n : ℕ, ∃ m : ℕ, (a n)^2 + (a (n + 1))^2 = a m :=
-sorry
+    (f : ℝ → ℝ)
+    (hf : f = fun x ↦ 1 / (1 - 2 * x - x ^ 2))
+    (a : ℕ → ℝ)
+    (hf' : ∀ᶠ x in 𝓝 0, Tendsto (fun N : ℕ ↦ ∑ n in Finset.range N, (a n) * x ^ n) atTop (𝓝 (f x)))
+    (n : ℕ) :
+    ∃ m : ℕ, (a n) ^ 2 + (a (n + 1)) ^ 2 = a m :=
+  sorry

lean4/src/putnam_2004_b5.lean

@@ -6,7 +6,9 @@ open Nat Topology Filter
 abbrev putnam_2004_b5_solution : ℝ := sorry
 -- 2 / Real.exp 1
 theorem putnam_2004_b5
-(xprod : ℝ → ℝ)
-(hxprod : ∀ x ≥ 0, Tendsto (fun N : ℕ => ∏ n : Fin N, ((1 + x ^ (n.1 + 1)) / (1 + x ^ n.1)) ^ (x ^ n.1)) atTop (𝓝 (xprod x)))
-: Tendsto xprod (𝓝[<] 1) (𝓝 putnam_2004_b5_solution) :=
-sorry
+    (xprod : ℝ → ℝ)
+    (hxprod : ∀ x ∈ Set.Ioo 0 1,
+      Tendsto (fun N ↦ ∏ n in Finset.range N, ((1 + x ^ (n + 1)) / (1 + x ^ n)) ^ (x ^ n))
+      atTop (𝓝 (xprod x))) :
+    Tendsto xprod (𝓝[<] 1) (𝓝 putnam_2004_b5_solution) :=
+  sorry

lean4/src/putnam_2005_a3.lean

@@ -4,11 +4,14 @@ open BigOperators
 open Nat Set
 
 theorem putnam_2005_a3
-(p : Polynomial ℂ)
-(n : ℕ)
-(g : ℂ → ℂ)
-(pdeg : p.degree = n)
-(pzeros : ∀ z : ℂ, p.eval z = 0 → Complex.abs z = 1)
-(hg : ∀ z : ℂ, g z = (p.eval z) / z ^ ((n : ℂ) / 2))
-: ∀ z : ℂ, (deriv g z = 0) → (Complex.abs z = 1) :=
-sorry
+    (p : Polynomial ℂ)
+    (n : ℕ)
+    (hn : 0 < n)
+    (g : ℂ → ℂ)
+    (pdeg : p.degree = n)
+    (pzeros : ∀ z : ℂ, p.eval z = 0 → Complex.abs z = 1)
+    (hg : ∀ z : ℂ, g z = (p.eval z) / z ^ ((n : ℂ) / 2))
+    (z : ℂ)
+    (hz : deriv g z = 0) :
+    Complex.abs z = 1 :=
+  sorry

lean4/src/putnam_2010_a1.lean

@@ -4,9 +4,12 @@ open BigOperators
 noncomputable abbrev putnam_2010_a1_solution : ℕ → ℕ := sorry
 -- (fun n : ℕ => Nat.ceil ((n : ℝ) / 2))
 theorem putnam_2010_a1
-(n : ℕ)
-(kboxes : ℕ → Prop)
-(npos : n > 0)
-(hkboxes : ∀ k : ℕ, kboxes k = (∃ boxes : Fin n → Fin k, ∀ i j : Fin k, (∑' x : boxes ⁻¹' {i}, (x : ℕ)) = (∑' x : boxes ⁻¹' {j}, (x : ℕ))))
-: kboxes (putnam_2010_a1_solution n) ∧ (∀ k : ℕ, kboxes k → k ≤ putnam_2010_a1_solution n) :=
-sorry
+    (n : ℕ)
+    (kboxes : ℕ → Prop)
+    (npos : n > 0)
+    (hkboxes : ∀ k : ℕ, kboxes k =
+      (∃ boxes : Finset.Icc 1 n → Fin k, ∀ i j : Fin k,
+        ∑ x in Finset.univ.filter (boxes · = i), (x : ℕ) =
+        ∑ x in Finset.univ.filter (boxes · = j), (x : ℕ))) :
+    IsGreatest kboxes (putnam_2010_a1_solution n) :=
+  sorry

lean4/src/putnam_2015_b6.lean

@@ -1,12 +1,13 @@
 import Mathlib
 open BigOperators
 
-open Function
+open Filter Topology
 
 noncomputable abbrev putnam_2015_b6_solution : ℝ := sorry
 -- Real.pi ^ 2 / 16
 theorem putnam_2015_b6
-(A : ℕ → ℕ)
-(hA : ∀ k > 0, A k = {j : ℕ | Odd j ∧ j ∣ k ∧ j < Real.sqrt (2 * k)}.encard)
-: ∑' k : Set.Ici 1, (-1 : ℝ) ^ ((k : ℝ) - 1) * (A k / (k : ℝ)) = putnam_2015_b6_solution :=
-sorry
+    (A : ℕ → ℕ)
+    (hA : ∀ k > 0, A k = {j : ℕ | Odd j ∧ j ∣ k ∧ j < Real.sqrt (2 * k)}.encard) :
+    Tendsto (fun K : ℕ ↦ ∑ k in Finset.Icc 1 K, (-1 : ℝ) ^ ((k : ℝ) - 1) * (A k / (k : ℝ)))
+      atTop (𝓝 putnam_2015_b6_solution) :=
+  sorry