From dda4b9de9757cbd7436dd934b48a43689c581c6e Mon Sep 17 00:00:00 2001 From: George Tsoukalas <99286219+GeorgeTsoukalas@users.noreply.github.com> Date: Fri, 6 Dec 2024 10:22:12 -0600 Subject: [PATCH] Update lean4/src/putnam_1986_a5.lean Co-authored-by: Eric Wieser --- lean4/src/putnam_1986_a5.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4/src/putnam_1986_a5.lean b/lean4/src/putnam_1986_a5.lean index c8e3971..7b16258 100644 --- a/lean4/src/putnam_1986_a5.lean +++ b/lean4/src/putnam_1986_a5.lean @@ -7,6 +7,7 @@ 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) + (C : Fin n → Fin n → ℝ) + (hf' : ∀ i j : Fin n, ∀ x : Fin n → ℝ, fderiv ℝ (f i) x (Pi.single j 1) - fderiv ℝ (f j) x (Pi.single i 1) = C i j) : ∃ g : (Fin n → ℝ) → ℝ, ∀ i : Fin n, IsLinearMap ℝ (λ x ↦ f i x + fderiv ℝ g x (Pi.single i 1)) := sorry