Merge pull request #209 from ocfnash/main

Fix a few minor Lean misformalisations

lean4/src/putnam_1974_a4.lean

@@ -3,10 +3,12 @@ open BigOperators
 
 open Set Nat
 
-noncomputable abbrev putnam_1974_a4_solution : ℕ → ℝ := sorry
--- (fun n => (n / 2^(n-1)) * (n-1).choose (floor ((n-1)/2)))
+noncomputable abbrev putnam_1974_a4_solution : ℕ → ℚ := sorry
+-- (fun n ↦ (1 : ℚ) / (2 ^ (n - 1)) * (n * (n - 1).choose ⌊n / 2⌋₊))
+
 theorem putnam_1974_a4
-(n : ℕ)
-(hn : n > 0)
-: (1 : ℝ)/(2^(n-1)) * ∑ k in Finset.Icc 0 ((ceil (n/2)) - 1), (n - 2*k)*(n.choose k) = putnam_1974_a4_solution n :=
-sorry
+    (n : ℕ)
+    (hn : 0 < n) :
+    (1 : ℚ) / (2 ^ (n - 1)) * ∑ k in Finset.Icc 0 ⌊n / 2⌋₊, (n - 2 * k) * (n.choose k) =
+    putnam_1974_a4_solution n :=
+  sorry

lean4/src/putnam_1974_b1.lean

@@ -3,12 +3,13 @@ open BigOperators
 
 open Set Nat Polynomial
 
-abbrev putnam_1974_b1_solution : (Fin 5 → (ℝ × ℝ)) -> Prop := sorry
--- fun points => (∃ (B : ℝ) (ordering : Equiv.Perm (Fin 5)), ∀ i : Fin 5, Real.sqrt (((points (ordering i)).1 - (points (ordering (i+1))).1)^2 + ((points (ordering i)).2 - (points (ordering (i+1))).2)^2) = B)
+abbrev putnam_1974_b1_solution : (Fin 5 → EuclideanSpace ℝ (Fin 2)) → Prop := sorry
+-- fun p ↦ ∃ᵉ (B > 0) (o : Equiv.Perm (Fin 5)), ∀ i, dist (p (o i)) (p (o (i + 1))) = B
+
 theorem putnam_1974_b1
-(on_unit_circle : (Fin 5 → (ℝ × ℝ)) -> Prop)
-(distance_fun : (Fin 5 → (ℝ × ℝ)) -> ℝ)
-(h_on_unit_circle : on_unit_circle = fun points => ∀ i : Fin 5, Real.sqrt ((points i).1^2 + (points i).2^2) = 1)
-(hdistance_fun : distance_fun = fun points => ∑ idx : Fin 5 × Fin 5, if idx.1 < idx.2 then Real.sqrt (((points idx.1).1 - (points idx.2).1)^2 + ((points idx.1).2 - (points idx.2).2)^2) else 0)
-: ∀ points : Fin 5 → (ℝ × ℝ), on_unit_circle points → (distance_fun points = sSup {R | ∃ pts, on_unit_circle pts ∧ R = distance_fun pts} ↔ putnam_1974_b1_solution points) :=
-sorry
+    (d : (Fin 5 → EuclideanSpace ℝ (Fin 2)) → ℝ)
+    (d_def : ∀ p, d p = ∑ ⟨i, j⟩ : Fin 5 × Fin 5, if i < j then dist (p i) (p j) else 0)
+    (p : Fin 5 → EuclideanSpace ℝ (Fin 2))
+    (hp : ∀ i, ‖p i‖ = 1) :
+    d p = sSup {d q | (q) (hq : ∀ i, ‖q i‖ = 1)} ↔ putnam_1974_b1_solution p :=
+  sorry

lean4/src/putnam_1976_a2.lean

@@ -4,13 +4,15 @@ open BigOperators
 open MvPolynomial
 
 theorem putnam_1976_a2
-(P Q : MvPolynomial (Fin 2) ℤ)
-(hP : P = (X 0)^2*(X 1) + (X 0)*(X 1)^2)
-(hQ : Q = (X 0)^2 + (X 0)*(X 1) + (X 2)^2)
-(F G : ℕ → MvPolynomial (Fin 2) ℤ)
-(hF : F = fun n : ℕ => ((X 0) + (X 1))^n - (X 0)^n - (X 1)^n)
-(hG : G = fun n : ℕ => ((X 0) + (X 1))^n + (X 0)^n + (X 1)^n)
-(i : Fin 2 → MvPolynomial (Fin 2) ℤ)
-(hi : i = fun j : Fin 2 => ite (j = 0) P Q)
-: ∀ n : ℕ, n > 0 → ∃ A : MvPolynomial (Fin 2) ℤ, F n = aeval i A ∨ G n = aeval i A :=
-sorry
+    (P Q : MvPolynomial (Fin 2) ℤ)
+    (hP : P = X 0 ^ 2 * X 1 + X 0 * X 1 ^ 2)
+    (hQ : Q = X 0 ^ 2 + X 0 * X 1 + X 1 ^ 2)
+    (F G : ℕ → MvPolynomial (Fin 2) ℤ)
+    (hF : ∀ n, F n = (X 0 + X 1) ^ n - X 0 ^ n - X 1 ^ n)
+    (hG : ∀ n, G n = (X 0 + X 1) ^ n + X 0 ^ n + X 1 ^ n)
+    (n : ℕ)
+    (hn : 0 < n) :
+    ∃ A : MvPolynomial (Fin 2) ℤ,
+      F n = aeval ![P, Q] A ∨
+      G n = aeval ![P, Q] A :=
+  sorry

lean4/src/putnam_1977_a3.lean

@@ -4,6 +4,8 @@ open BigOperators
 abbrev putnam_1977_a3_solution : (ℝ → ℝ) → (ℝ → ℝ) → (ℝ → ℝ) := sorry
 -- fun f g x ↦ g x - f (x - 3) + f (x - 1) + f (x + 1) - f (x + 3)
 theorem putnam_1977_a3
-(f g : ℝ → ℝ)
-: let h := putnam_1977_a3_solution f g; (∀ x : ℝ, f x = (h (x + 1) + h (x - 1)) / 2 ∧ g x = (h (x + 4) + h (x - 4)) / 2) :=
-sorry
+    (f g h : ℝ → ℝ)
+    (hf : ∀ x, f x = (h (x + 1) + h (x - 1)) / 2)
+    (hg : ∀ x, g x = (h (x + 4) + h (x - 4)) / 2) :
+    h = putnam_1977_a3_solution f g :=
+  sorry

lean4/src/putnam_1982_b4.lean

@@ -6,8 +6,8 @@ open Set Function Filter Topology Polynomial Real
 abbrev putnam_1982_b4_solution : Prop × Prop := sorry
 -- (True, True)
 theorem putnam_1982_b4
-(hn : Finset ℤ → Prop)
-(hn_def : hn = fun n : Finset ℤ => ∀ k : ℤ, ∏ i in n, i ∣ ∏ i in n, (i + k))
-: ((∀ n : Finset ℤ, hn n → (∃ i ∈ n, |i| = 1)) ↔ putnam_1982_b4_solution.1) ∧
-((∀ n : Finset ℤ, (hn n ∧ ∀ i ∈ n, i > 0) → n = Finset.Icc (1 : ℤ) (n.card)) ↔ putnam_1982_b4_solution.2) :=
-sorry
+    (P : Finset ℤ → Prop)
+    (P_def : ∀ n, P n ↔ n.Nonempty ∧ ∀ k, ∏ i in n, i ∣ ∏ i in n, (i + k)) :
+    ((∀ n, P n → 1 ∈ n ∨ -1 ∈ n) ↔ putnam_1982_b4_solution.1) ∧
+    ((∀ n, P n → (∀ i ∈ n, 0 < i) → n = Finset.Icc (1 : ℤ) n.card) ↔ putnam_1982_b4_solution.2) :=
+  sorry

lean4/src/putnam_1989_b3.lean

@@ -4,12 +4,15 @@ open BigOperators
 open Nat Filter Topology
 
 noncomputable abbrev putnam_1989_b3_solution : ℕ → ℝ → ℝ := sorry
--- fun n c ↦ c * factorial n / (3 ^ n * ∏ m in Finset.Icc (1 : ℤ) n, (1 - 2 ^ (-m)))
+-- fun n c ↦ c * n ! / (3 ^ n * ∏ m in Finset.Icc (1 : ℤ) n, (1 - 2 ^ (-m)))
 theorem putnam_1989_b3
-(f : ℝ → ℝ)
-(hfdiff : Differentiable ℝ f)
-(hfderiv : ∀ x > 0, deriv f x = -3 * f x + 6 * f (2 * x))
-(hdecay : ∀ x ≥ 0, |f x| ≤ Real.exp (-Real.sqrt x))
-(μ : ℕ → ℝ := fun n ↦ ∫ x in Set.Ioi 0, x ^ n * (f x))
-: ((∀ n : ℕ, μ n = putnam_1989_b3_solution n (μ 0)) ∧ (∃ L : ℝ, Tendsto (fun n ↦ (μ n) * 3 ^ n / factorial n) atTop (𝓝 L)) ∧ (Tendsto (fun n ↦ (μ n) * 3 ^ n / factorial n) atTop (𝓝 0) → μ 0 = 0)) :=
-sorry
+    (f : ℝ → ℝ)
+    (hfdiff : Differentiable ℝ f)
+    (hfderiv : ∀ x > 0, deriv f x = -3 * f x + 6 * f (2 * x))
+    (hdecay : ∀ x ≥ 0, |f x| ≤ Real.exp (- √x))
+    (μ : ℕ → ℝ)
+    (μ_def : ∀ n, μ n = ∫ x in Set.Ioi 0, x ^ n * f x) :
+    (∀ n, μ n = putnam_1989_b3_solution n (μ 0)) ∧
+    (∃ L, Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 L)) ∧
+    (Tendsto (fun n ↦ (μ n) * 3 ^ n / n !) atTop (𝓝 0) → μ 0 = 0) := by
+  sorry

lean4/src/putnam_1990_a6.lean

@@ -5,8 +5,8 @@ open Filter Topology Nat
 
 abbrev putnam_1990_a6_solution : ℕ := sorry
 -- 17711
-theorem putnam_1990_a6
-(STadmiss : (Fin 2 → (Finset (Fin 10))) → Prop)
-(hSTadmiss : ∀ ST : Fin 2 → (Finset (Fin 10)), STadmiss ST = ((∀ s ∈ ST 0, (s+1) > (ST 1).card) ∧ (∀ t ∈ ST 1, (t+1) > (ST 0).card)))
-: {ST : Fin 2 → (Finset (Fin 10)) | STadmiss ST}.encard = putnam_1990_a6_solution :=
-sorry
+theorem putnam_1990_a6 :
+    ((Finset.univ : Finset <| Finset (Set.Icc 1 10) × Finset (Set.Icc 1 10)).filter
+      fun ⟨S, T⟩ ↦ (∀ s ∈ S, T.card < s) ∧ (∀ t ∈ T, S.card < t)).card =
+    putnam_1990_a6_solution := by
+  sorry

lean4/src/putnam_1990_b1.lean

@@ -6,8 +6,9 @@ open Filter Topology Nat
 abbrev putnam_1990_b1_solution : Set (ℝ → ℝ) := sorry
 -- {fun x : ℝ => (Real.sqrt 1990) * Real.exp x, fun x : ℝ => -(Real.sqrt 1990) * Real.exp x}
 theorem putnam_1990_b1
-(f : ℝ → ℝ)
-(fint : Prop)
-(hfint : fint = ∀ x : ℝ, (f x) ^ 2 = (∫ t in Set.Ioo 0 x, (f t) ^ 2 + (deriv f t) ^ 2) + 1990)
-: (ContDiff ℝ 1 f ∧ fint) ↔ f ∈ putnam_1990_b1_solution :=
-sorry
+    (P : (ℝ → ℝ) → Prop)
+    (P_def : ∀ f, P f ↔ ∀ x,
+      (f x) ^ 2 = (∫ t in (0 : ℝ)..x, (f t) ^ 2 + (deriv f t) ^ 2) + 1990)
+    (f : ℝ → ℝ) :
+    (ContDiff ℝ 1 f ∧ P f) ↔ f ∈ putnam_1990_b1_solution :=
+  sorry

lean4/src/putnam_1991_a4.lean

@@ -1,16 +1,15 @@
 import Mathlib
 open BigOperators
 
-open Filter Topology
+open Filter FiniteDimensional Metric Topology
 
 abbrev putnam_1991_a4_solution : Prop := sorry
 -- True
-theorem putnam_1991_a4
-(climit : (ℕ → (EuclideanSpace ℝ (Fin 2))) → Prop)
-(rareas : (ℕ → ℝ) → Prop)
-(crline : (ℕ → (EuclideanSpace ℝ (Fin 2))) → (ℕ → ℝ) → Prop)
-(hclimit : ∀ c : ℕ → (EuclideanSpace ℝ (Fin 2)), climit c = ¬∃ (p : EuclideanSpace ℝ (Fin 2)), ∀ ε : ℝ, ε > 0 → ∃ i : ℕ, c i ∈ Metric.ball p ε)
-(hrareas : ∀ r : ℕ → ℝ, rareas r = ∃ A : ℝ, Tendsto (fun n : ℕ => ∑ i : Fin n, Real.pi * (r i) ^ 2) atTop (𝓝 A))
-(hcrline : ∀ (c : ℕ → (EuclideanSpace ℝ (Fin 2))) (r : ℕ → ℝ), crline c r = (∀ v w : EuclideanSpace ℝ (Fin 2), w ≠ 0 → ∃ i : ℕ, {p : EuclideanSpace ℝ (Fin 2) | ∃ t : ℝ, p = v + t • w} ∩ Metric.closedBall (c i) (r i) ≠ ∅))
-: (∃ (c : ℕ → (EuclideanSpace ℝ (Fin 2))) (r : ℕ → ℝ), (∀ i : ℕ, r i ≥ 0) ∧ climit c ∧ rareas r ∧ crline c r) ↔ putnam_1991_a4_solution :=
-sorry
+theorem putnam_1991_a4 :
+    (∃ (c : ℕ → EuclideanSpace ℝ (Fin 2)) (r : ℕ → ℝ),
+      (¬ ∃ p, MapClusterPt p atTop c) ∧
+      (Summable <| fun i ↦ r i ^ 2) ∧
+      (∀ L : AffineSubspace ℝ (EuclideanSpace ℝ (Fin 2)),
+        finrank L.direction = 1 → ∃ i, (↑L ∩ closedBall (c i) (r i)).Nonempty)) ↔
+    putnam_1991_a4_solution :=
+  sorry

lean4/src/putnam_2018_b5.lean

@@ -1,14 +1,13 @@
 import Mathlib
 open BigOperators
 
+open Function
+
 theorem putnam_2018_b5
-(f : ℝ → ℝ → (Fin 2 → ℝ))
-(fpart1 : Fin 2 → ℝ → (ℝ → ℝ))
-(fpart2 : Fin 2 → ℝ → (ℝ → ℝ))
-(hfpart1 : fpart1 = (fun (i : Fin 2) (x2 : ℝ) => (fun x1 : ℝ => (f x1 x2) i)))
-(hfpart2 : fpart2 = (fun (i : Fin 2) (x1 : ℝ) => (fun x2 : ℝ => (f x1 x2) i)))
-(hfdiff : ∀ (i : Fin 2) (x : ℝ), ContDiff ℝ 1 (fpart1 i x) ∧ ContDiff ℝ 1 (fpart2 i x))
-(hfpos : ∀ (i : Fin 2) (x : ℝ), deriv (fpart1 i x) > 0 ∧ deriv (fpart2 i x) > 0)
-(hfexprgt0 : ∀ x1 x2 : ℝ, (deriv (fpart1 0 x2) x1) * (deriv (fpart2 1 x1) x2) - (1 / 4) * ((deriv (fpart2 0 x1) x2) + (deriv (fpart1 1 x2) x1)) ^ 2 > 0)
-: Function.Injective f :=
-sorry
+    (f : (Fin 2 → ℝ) → (Fin 2 → ℝ))
+    (h₁ : ContDiff ℝ 1 f)
+    (h₂ : ∀ x i j, 0 < fderiv ℝ f x i j)
+    (h₃ : ∀ x, 0 < fderiv ℝ f x 0 0 * fderiv ℝ f x 1 1 -
+      (1 / 4) * (fderiv ℝ f x 0 1 + fderiv ℝ f x 1 0) ^ 2) :
+    Injective f :=
+  sorry