From f9456b6883988690e4236f25c31617fdb9c8e9c0 Mon Sep 17 00:00:00 2001
From: George Tsoukalas <george.tsoukalas@utexas.edu>
Date: Sat, 9 Nov 2024 20:59:11 +0000
Subject: [PATCH] Rewrite Lean formalization.

---
 lean4/src/putnam_1986_a5.lean | 24 +++++++-----------------
 lean4/src/putnam_1987_a5.lean | 32 +++++++++++---------------------
 lean4/src/putnam_1989_b6.lean | 28 ++++++++++++----------------
 3 files changed, 30 insertions(+), 54 deletions(-)

diff --git a/lean4/src/putnam_1986_a5.lean b/lean4/src/putnam_1986_a5.lean
index 699b7ba6..92e17e16 100644
--- a/lean4/src/putnam_1986_a5.lean
+++ b/lean4/src/putnam_1986_a5.lean
@@ -1,22 +1,12 @@
 import Mathlib
 
-open  Real Equiv
-
 /--
 Suppose $f_1(x),f_2(x),\dots,f_n(x)$ are functions of $n$ real variables $x=(x_1,\dots,x_n)$ with continuous second-order partial derivatives everywhere on $\mathbb{R}^n$. Suppose further that there are constants $c_{ij}$ such that $\frac{\partial f_i}{\partial x_j}-\frac{\partial f_j}{\partial x_i}=c_{ij}$ for all $i$ and $j$, $1 \leq i \leq n$, $1 \leq j \leq n$. Prove that there is a function $g(x)$ on $\mathbb{R}^n$ such that $f_i+\partial g/\partial x_i$ is linear for all $i$, $1 \leq i \leq n$. (A linear function is one of the form $a_0+a_1x_1+a_2x_2+\dots+a_nx_n$.)
 -/
-theorem putnam_1986_a5
-(n : ℕ)
-(f : Fin n → ((Fin n → ℝ) → ℝ))
-(xrepl : (Fin n → ℝ) → Fin n → ℝ → (Fin n → ℝ))
-(contdiffx : ((Fin n → ℝ) → ℝ) → Fin n → (Fin n → ℝ) → Prop)
-(partderiv : ((Fin n → ℝ) → ℝ) → Fin n → ((Fin n → ℝ) → ℝ))
-(hpartderiv : partderiv = (fun (func : (Fin n → ℝ) → ℝ) (i : Fin n) => (fun x : Fin n → ℝ => deriv (fun xi : ℝ => func (xrepl x i xi)) (x i))))
-(npos : n ≥ 1)
-(hxrepl : xrepl = (fun (x : Fin n → ℝ) (i : Fin n) (xi : ℝ) => (fun j : Fin n => if j = i then xi else x j)))
-(hcontdiffx : contdiffx = (fun (func : (Fin n → ℝ) → ℝ) (i : Fin n) (x : Fin n → ℝ) => ContDiff ℝ 1 (fun xi : ℝ => func (xrepl x i xi))))
-(hfcontdiff1 : ∀ i : Fin n, ∀ j : Fin n, ∀ x : Fin n → ℝ, contdiffx (f i) j x)
-(hfcontdiff2 : ∀ i : Fin n, ∀ j1 j2 : Fin n, ∀ x : Fin n → ℝ, contdiffx (partderiv (f i) j1) j2 x)
-(hfc : ∃ c : Fin n → Fin n → ℝ, ∀ i j : Fin n, partderiv (f i) j - partderiv (f j) i = (fun x : Fin n → ℝ => c i j))
-: ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (f i + partderiv g i) :=
-sorry
+theorem putnam_1986_a5'
+  (n : ℕ) (hn : 1 ≤ n)
+  (f : Fin n → ((Fin n → ℝ) → ℝ))
+  (hf : ∀ i, ContDiff ℝ 2 (f i))
+  (hf' : ∀ i j : Fin n, ∃ C : ℝ, ∀ x : Fin n → ℝ, fderiv ℝ (f i) x (Pi.single j 1) - fderiv ℝ (f j) x (Pi.single i 1) = C)
+  : ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (λ x ↦ f i x + fderiv ℝ g x (Pi.single i 1)) :=
+  sorry
diff --git a/lean4/src/putnam_1987_a5.lean b/lean4/src/putnam_1987_a5.lean
index aae45c50..e7e5b7d9 100644
--- a/lean4/src/putnam_1987_a5.lean
+++ b/lean4/src/putnam_1987_a5.lean
@@ -1,7 +1,5 @@
 import Mathlib
 
-open MvPolynomial Real
-
 abbrev putnam_1987_a5_solution : Prop := sorry
 -- False
 /--
@@ -12,22 +10,14 @@ Let $\vec{G}(x,y)=\left(\frac{-y}{x^2+4y^2},\frac{x}{x^2+4y^2},0\right)$. Prove
 \item[(iii)] $\vec{F}(x,y,0)=\vec{G}(x,y)$.
 \end{enumerate}
 -/
-theorem putnam_1987_a5
-(vec2 : ℝ → ℝ → (Fin 2 → ℝ))
-(vec3 : ℝ → ℝ → ℝ → (Fin 3 → ℝ))
-(G : (Fin 2 → ℝ) → (Fin 3 → ℝ))
-(hG : G = (fun v : Fin 2 → ℝ => vec3 (-v 1 / ((v 0) ^ 2 + 4 * (v 1) ^ 2)) (v 0 / ((v 0) ^ 2 + 4 * (v 1) ^ 2)) 0))
-(vrepl : (Fin 3 → ℝ) → Fin 3 → ℝ → (Fin 3 → ℝ))
-(hvrepl : vrepl = (fun (v : Fin 3 → ℝ) (i : Fin 3) (vi : ℝ) => (fun j : Fin 3 => if j = i then vi else v j)))
-(contdiffv : ((Fin 3 → ℝ) → ℝ) → Fin 3 → (Fin 3 → ℝ) → Prop)
-(hcontdiffv : contdiffv = (fun (Fi : (Fin 3 → ℝ) → ℝ) (j : Fin 3) (v : Fin 3 → ℝ) => ContDiffAt ℝ 1 (fun vj : ℝ => Fi (vrepl v j vj)) (v j)))
-(partderiv : ((Fin 3 → ℝ) → ℝ) → Fin 3 → ((Fin 3 → ℝ) → ℝ))
-(hpartderiv : partderiv = (fun (Fi : (Fin 3 → ℝ) → ℝ) (j : Fin 3) => (fun v : Fin 3 → ℝ => deriv (fun vj : ℝ => Fi (vrepl v j vj)) (v j))))
-(Fprop1 Fprop2 Fprop3 : (Fin 3 → ((Fin 3 → ℝ) → ℝ)) → Prop)
-(hFprop1 : Fprop1 = (fun F : Fin 3 → ((Fin 3 → ℝ) → ℝ) => ∀ i : Fin 3, ∀ j : Fin 3, ∀ v ≠ 0, contdiffv (F i) j v))
-(hFprop2 : Fprop2 = (fun F : Fin 3 → ((Fin 3 → ℝ) → ℝ) => ∀ v ≠ 0, vec3 ((partderiv (F 2) 1 - partderiv (F 1) 2) v) ((partderiv (F 0) 2 - partderiv (F 2) 0) v) ((partderiv (F 1) 0 - partderiv (F 0) 1) v) = 0))
-(hFprop3 : Fprop3 = (fun F : Fin 3 → ((Fin 3 → ℝ) → ℝ) => ∀ x y : ℝ, (fun i : Fin 3 => (F i) (vec3 x y 0)) = G (vec2 x y)))
-(hvec2 : ∀ x y : ℝ, (vec2 x y) 0 = x ∧ (vec2 x y) 1 = y)
-(hvec3 : ∀ x y z : ℝ, (vec3 x y z) 0 = x ∧ (vec3 x y z) 1 = y ∧ (vec3 x y z) 2 = z)
-: (∃ F : Fin 3 → ((Fin 3 → ℝ) → ℝ), Fprop1 F ∧ Fprop2 F ∧ Fprop3 F) ↔ putnam_1987_a5_solution :=
-sorry
+theorem putnam_1987_a5'
+    (G : (Fin 2 → ℝ) → (Fin 3 → ℝ))
+    (G_def : ∀ x y, G ![x, y] = ![(-y / (x ^ 2 + 4 * y ^ 2)), (x / (x ^ 2 + 4 * y ^ 2)), 0]) :
+    (∃ F : (Fin 3 → ℝ) → (Fin 3 → ℝ),
+      ContDiffOn ℝ 1 F {v | v ≠ ![0,0,0]} ∧
+      (∀ x, x ≠ 0 →
+        (fderiv ℝ F x (Pi.single 1 1) 2 - fderiv ℝ F x (Pi.single 2 1) 1 = 0 ∧
+        fderiv ℝ F x (Pi.single 2 1) 0 - fderiv ℝ F x (Pi.single 0 1) 2 = 0 ∧
+        fderiv ℝ F x (Pi.single 0 1) 1 - fderiv ℝ F x (Pi.single 1 1) 0 = 0)) ∧
+      ∀ x y, F ![x, y, 0] = G ![x, y]) ↔ putnam_1987_a5_solution :=
+  sorry
diff --git a/lean4/src/putnam_1989_b6.lean b/lean4/src/putnam_1989_b6.lean
index e91a9056..97289db8 100644
--- a/lean4/src/putnam_1989_b6.lean
+++ b/lean4/src/putnam_1989_b6.lean
@@ -1,23 +1,19 @@
 import Mathlib
 
-open Nat Filter Topology Set
+open Nat Filter Topology Set ProbabilityTheory
 
 -- Note: uses (ℝ → ℝ) instead of (Set.Icc 0 1 → ℝ)
 /--
 Let $(x_1,x_2,\dots,x_n)$ be a point chosen at random from the $n$-dimensional region defined by $0<x_1<x_2<\dots<x_n<1$. Let $f$ be a continuous function on $[0,1]$ with $f(1)=0$. Set $x_0=0$ and $x_{n+1}=1$. Show that the expected value of the Riemann sum $\sum_{i=0}^n (x_{i+1}-x_i)f(x_{i+1})$ is $\int_0^1 f(t)P(t)\,dt$, where $P$ is a polynomial of degree $n$, independent of $f$, with $0 \leq P(t) \leq 1$ for $0 \leq t \leq 1$.
 -/
-theorem putnam_1989_b6
-(n : ℕ)
-(Sx : Set (Fin n → ℝ))
-(fprop : (ℝ → ℝ) → Prop)
-(xext : (Fin n → ℝ) → (ℕ → ℝ))
-(fxsum : (ℝ → ℝ) → (Fin n → ℝ) → ℝ)
-(fEV : (ℝ → ℝ) → ℝ)
-(hSx : Sx = {x : Fin n → ℝ | 0 < x ∧ StrictMono x ∧ x < 1})
-(hfprop : fprop = (fun f : ℝ → ℝ => ContinuousOn f (Set.Icc 0 1) ∧ f 1 = 0))
-(hfxsum : fxsum = (fun (f : ℝ → ℝ) (x : Fin n → ℝ) => ∑ i in Finset.Icc 0 n, ((xext x) (i + 1) - (xext x) i) * f ((xext x) (i + 1))))
-(hfEV : fEV = (fun f : ℝ → ℝ => (∫ x in Sx, fxsum f x) / (∫ x in Sx, 1)))
-(npos : n ≥ 1)
-(hxext : ∀ x : Fin n → ℝ, (xext x) 0 = 0 ∧ (xext x) (n + 1) = 1 ∧ (∀ i : Fin n, (xext x) (i + 1) = x i))
-: ∃ P : Polynomial ℝ, P.degree = n ∧ (∀ t ∈ Set.Icc 0 1, 0 ≤ P.eval t ∧ P.eval t ≤ 1) ∧ (∀ f : ℝ → ℝ, fprop f → fEV f = (∫ t in Set.Ioo 0 1, f t * P.eval t)) :=
-sorry
+theorem putnam_1989_b6'
+  (n : ℕ) (hn : 0 < n)
+  (S : (ℝ → ℝ) → (Fin (n + 2) → Icc (0 : ℝ) 1) → ℝ)
+  (hS : ∀ f x, S f x = if StrictMono x ∧ x 0 = 0 ∧ x (-1) = 1 then ∑ i in Icc 0 n, (x (i + 1) - x i) * f (x (i + 1)) else 0)
+  : ∃ P : Polynomial ℝ,
+    P.degree = n ∧
+    (∀ t ∈ Icc 0 1, P.eval t ∈ Icc 0 1) ∧
+    (∀ f : ℝ → ℝ,
+      f 1 = 0 ∧ ContinuousOn f (Icc 0 1) →
+      𝔼[(↑) ∘ (S f)] = ∫ t in (0)..1, (f t) * (P.eval t)) :=
+  sorry