Refactor curl definition

trishullab · Nov 20, 2024 · 8de8461 · 8de8461
1 parent 5330134
commit 8de8461
Showing 1 changed file with 6 additions and 4 deletions.
diff --git a/lean4/src/putnam_1987_a5.lean b/lean4/src/putnam_1987_a5.lean
@@ -11,13 +11,15 @@ Let $\vec{G}(x,y)=\left(\frac{-y}{x^2+4y^2},\frac{x}{x^2+4y^2},0\right)$. Prove
 \end{enumerate}
 -/
 theorem putnam_1987_a5
+    (curl : ((Fin 3 → ℝ) → (Fin 3 → ℝ)) → ((Fin 3 → ℝ) → (Fin 3 → ℝ)))
+    (curl_def : ∀ f x, curl f x = ![
+      fderiv ℝ f x (Pi.single 1 1) 2 - fderiv ℝ f x (Pi.single 2 1) 1,
+      fderiv ℝ f x (Pi.single 2 1) 0 - fderiv ℝ f x (Pi.single 0 1) 2,
+      fderiv ℝ f x (Pi.single 0 1) 1 - fderiv ℝ f x (Pi.single 1 1) 0])
     (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, x ≠ 0 → curl F x = 0) ∧
       ∀ x y, F ![x, y, 0] = G ![x, y]) ↔ putnam_1987_a5_solution :=
   sorry