Merge pull request #203 from ocfnash/fix_misformalisations

Fix some minor Lean misformalisations

Author: GeorgeTsoukalas

lean4/src/putnam_2006_b3.lean

@@ -4,11 +4,15 @@ open BigOperators
 abbrev putnam_2006_b3_solution : ℕ → ℕ := sorry
 -- (fun n : ℕ => (Nat.choose n 2) + 1)
 theorem putnam_2006_b3
-(SABpart : Finset (Fin 2 → ℝ) → Finset (Finset (Fin 2 → ℝ)) → Prop)
-(LS : Finset (Fin 2 → ℝ) → ℕ)
-(n : ℕ)
-(hSABpart : ∀ (S : Finset (Fin 2 → ℝ)) (AB : Finset (Finset (Fin 2 → ℝ))), SABpart S AB = (AB.card = 2 ∧ ∃ A ∈ AB, ∃ B ∈ AB, (A ∪ B = S) ∧ (A ∩ B = ∅) ∧ (∃ m b : ℝ, (∀ p ∈ A, p 1 > m * p 0 + b) ∧ (∀ p ∈ B, p 1 < m * p 0 + b))))
-(hLS : ∀ S : Finset (Fin 2 → ℝ), LS S = {AB : Finset (Finset (Fin 2 → ℝ)) | SABpart S AB}.encard)
-(npos : n > 0)
-: (∃ S : Finset (Fin 2 → ℝ), S.card = n ∧ LS S = putnam_2006_b3_solution n) ∧ (∀ S : Finset (Fin 2 → ℝ), S.card = n → LS S ≤ putnam_2006_b3_solution n) :=
-sorry
+    (IsLinearPartition : Finset (Fin 2 → ℝ) → Finset (Finset (Fin 2 → ℝ)) → Prop)
+    (IsLinearPartition_def : ∀ S AB, IsLinearPartition S AB ↔
+      (AB.card = 2 ∧ ∃ A ∈ AB, ∃ B ∈ AB,
+        A ≠ B ∧ (A ∪ B = S) ∧ (A ∩ B = ∅) ∧
+        (∃ m b : ℝ,
+          (∀ p ∈ A, p 1 > m * p 0 + b) ∧
+          (∀ p ∈ B, p 1 < m * p 0 + b))))
+    (L : Finset (Fin 2 → ℝ) → ℕ)
+    (hL : ∀ S, L S = {AB | IsLinearPartition S AB}.encard)
+    (n : ℕ) (npos : 0 < n) :
+    IsGreatest {L S | (S) (hS : S.card = n)} (putnam_2006_b3_solution n) :=
+  sorry

lean4/src/putnam_2011_a4.lean

@@ -6,9 +6,11 @@ open Topology Filter Matrix
 abbrev putnam_2011_a4_solution : Set ℕ := sorry
 -- {n : ℕ | Odd n}
 theorem putnam_2011_a4
-(n : ℕ)
-(nmat : Prop)
-(npos : n > 0)
-(hnmat : ∃ A : Matrix (Fin n) (Fin n) ℤ, (∀ r : Fin n, Even ((A r) ⬝ᵥ (A r))) ∧ (∀ r1 r2 : Fin n, r1 ≠ r2 → Odd ((A r1) ⬝ᵥ (A r2))))
-: nmat ↔ n ∈ putnam_2011_a4_solution :=
-sorry
+    (nmat : ℕ → Prop)
+    (hnmat : ∀ n, nmat n ↔
+      ∃ A : Matrix (Fin n) (Fin n) ℤ,
+        (∀ r, Even ((A r) ⬝ᵥ (A r))) ∧
+        Pairwise fun r1 r2 ↦ Odd ((A r1) ⬝ᵥ (A r2)))
+    (n : ℕ) (npos : 0 < n) :
+    nmat n ↔ n ∈ putnam_2011_a4_solution :=
+  sorry

lean4/src/putnam_2013_b4.lean

@@ -4,11 +4,10 @@ open BigOperators
 open Function Set
 
 theorem putnam_2013_b4
-(μ : (Set.Icc (0 : ℝ) 1 → ℝ) → ℝ)
-(Var : (Set.Icc (0 : ℝ) 1 → ℝ) → ℝ)
-(M : (Set.Icc (0 : ℝ) 1 → ℝ) → ℝ)
-(hμ : ∀ f : Set.Icc (0 : ℝ) 1 → ℝ, μ f = ∫ x : Set.Icc (0 : ℝ) 1, f x)
-(hVar : ∀ f : Set.Icc (0 : ℝ) 1 → ℝ, Var f = ∫ x : Set.Icc (0 : ℝ) 1, (f x - μ f) ^ 2)
-(hM : ∀ f : Set.Icc (0 : ℝ) 1 → ℝ, (∃ x : Set.Icc (0 : ℝ) 1, |f x| = M f) ∧ (∀ x : Set.Icc (0 : ℝ) 1, |f x| ≤ M f))
-: ∀ f g : Set.Icc (0 : ℝ) 1 → ℝ, (Continuous f ∧ Continuous g) → Var (f * g) ≤ 2 * Var f * (M g) ^ 2 + 2 * Var g * (M f) ^ 2 :=
+    (μ Var M : C(Icc (0 : ℝ) 1, ℝ) → ℝ)
+    (hμ : ∀ f, μ f = ∫ x, f x)
+    (hVar : ∀ f, Var f = ∫ x, (f x - μ f) ^ 2)
+    (hM : ∀ f : C(Icc (0 : ℝ) 1, ℝ), IsGreatest (range <| abs ∘ f) (M f))
+    (f g : C(Icc (0 : ℝ) 1, ℝ)) :
+    Var (f * g) ≤ 2 * Var f * (M g) ^ 2 + 2 * Var g * (M f) ^ 2 :=
 sorry

lean4/src/putnam_2017_a1.lean

@@ -4,10 +4,13 @@ open BigOperators
 abbrev putnam_2017_a1_solution : Set ℤ := sorry
 -- {x : ℤ | x > 0 ∧ (x = 1 ∨ 5 ∣ x)}
 theorem putnam_2017_a1
-(Q : Set (Set ℤ))
-(Spos : ∀ S ∈ Q, ∀ x ∈ S, x > 0)
-(S2 : ∀ S ∈ Q, 2 ∈ S)
-(Sn : ∀ S ∈ Q, ∀ n, n ^ 2 ∈ S → n ∈ S)
-(Sn5 : ∀ S ∈ Q, ∀ n, n ∈ S → (n + 5) ^ 2 ∈ S)
-: Set.univ \ (⋂ T ∈ Q, T) = putnam_2017_a1_solution :=
-sorry
+    (IsQualifying : Set ℤ → Prop)
+    (IsQualifying_def : ∀ S, IsQualifying S ↔
+      (∀ n ∈ S, 0 < n) ∧
+      2 ∈ S ∧
+      (∀ n, n ^ 2 ∈ S → n ∈ S) ∧
+      (∀ n ∈ S, (n + 5) ^ 2 ∈ S))
+    (S : Set ℤ)
+    (hS : IsLeast IsQualifying S) :
+    Sᶜ ∩ {n | 0 < n} = putnam_2017_a1_solution :=
+  sorry

lean4/src/putnam_2018_a3.lean

@@ -3,10 +3,8 @@ open BigOperators
 
 noncomputable abbrev putnam_2018_a3_solution : ℝ := sorry
 -- 480/49
-theorem putnam_2018_a3
-(P : Set (Fin 10 → ℝ))
-(f : (Fin 10 → ℝ) → ℝ → ℝ)
-(hf : f = fun x => fun k => ∑ i : Fin 10, Real.cos (k * (x i)))
-(hP : ∀ x ∈ P, f x 1 = 0)
-: ∀ y ∈ P, f y 3 ≤ putnam_2018_a3_solution ∧ ∃ x ∈ P, f x 3 = putnam_2018_a3_solution :=
-sorry
+theorem putnam_2018_a3 :
+    IsGreatest
+      {∑ i, Real.cos (3 * x i) | (x : Fin 10 → ℝ) (hx : ∑ i, Real.cos (x i) = 0)}
+      putnam_2018_a3_solution := by
+  sorry

lean4/src/putnam_2018_b3.lean

@@ -2,7 +2,7 @@ import Mathlib
 open BigOperators
 
 abbrev putnam_2018_b3_solution : Set ℕ := sorry
--- {2^2, 2^4, 2^8, 2^16}
+-- {2^2, 2^4, 2^16, 2^256}
 theorem putnam_2018_b3
 (n : ℕ)
 (hn : n > 0)

lean4/src/putnam_2019_b3.lean

@@ -12,6 +12,6 @@ theorem putnam_2019_b3
 (u : Matrix (Fin n) (Fin 1) ℝ)
 (hu : uᵀ*u = 1)
 (P : Matrix (Fin n) (Fin n) ℝ)
-(hP : P = 1 - (u * uᵀ))
+(hP : P = 1 - 2 * (u * uᵀ))
 : (Q - 1).det ≠ 0 → (P * Q - 1).det = 0 :=
 sorry

lean4/src/putnam_2021_a2.lean

@@ -7,6 +7,6 @@ abbrev putnam_2021_a2_solution : ℝ := sorry
 -- Real.exp 1
 theorem putnam_2021_a2
 (g : ℝ → ℝ)
-(hg : ∀ x > 0, Tendsto (fun r : ℝ => ((x + 1) ^ (r + 1) - x ^ (r + 1)) ^ (1 / r)) (𝓝 0) (𝓝 (g x)))
+(hg : ∀ x > 0, Tendsto (fun r : ℝ => ((x + 1) ^ (r + 1) - x ^ (r + 1)) ^ (1 / r)) (𝓝[>] 0) (𝓝 (g x)))
 : Tendsto (fun x : ℝ => g x / x) atTop (𝓝 putnam_2021_a2_solution) :=
 sorry

lean4/src/putnam_2021_b2.lean

@@ -5,10 +5,9 @@ open Filter Topology
 
 noncomputable abbrev putnam_2021_b2_solution : ℝ := sorry
 -- 2 / 3
-theorem putnam_2021_b2
-(S : (ℕ → ℝ) → ℝ)
-(asum : (ℕ → ℝ) → Prop)
-(hS : ∀ a : ℕ → ℝ, S a = ∑' n : ℕ, (n + 1) / 2 ^ (n + 1) * (∏ k : Fin (n + 1), a k.1) ^ ((1 : ℝ) / (n + 1)))
-(hasum : ∀ a : ℕ → ℝ, asum a = (∀ k : ℕ, a k ≥ 0) ∧ ∑' k : ℕ, a k = 1)
-: (∃ a : ℕ → ℝ, asum a ∧ S a = putnam_2021_b2_solution) ∧ (∀ a : ℕ → ℝ, asum a → S a ≤ putnam_2021_b2_solution) :=
-sorry
+theorem putnam_2021_b2 :
+    IsGreatest
+      {S | ∃ a : ℕ+ → ℝ, (∑' k, a k = 1) ∧ (∀ k, 0 ≤ a k) ∧
+        S = ∑' n : ℕ+, n / 2 ^ (n : ℕ) * (∏ k in Finset.Icc 1 n, a k) ^ (1 / n : ℝ)}
+      putnam_2021_b2_solution :=
+  sorry

lean4/src/putnam_2023_b6.lean

@@ -4,7 +4,7 @@ open BigOperators
 open Nat Topology Filter
 
 abbrev putnam_2023_b6_solution : ℕ → ℤ := sorry
--- (fun n : ℕ => (-1) ^ (Nat.ceil (n / 2) - 1) * 2 * Nat.ceil (n / 2))
+-- (fun n : ℕ => (-1) ^ (⌈(n / 2 : ℚ)⌉₊ + 1) * 2 * ⌈(n / 2 : ℚ)⌉₊)
 theorem putnam_2023_b6
 (n : ℕ)
 (S : Matrix (Fin n) (Fin n) ℤ)