I would like to state a simple equation in Isabelle:
\nabla f (x) = 0
where 0 is n dimensional and f : R^n --> R. What I have so far is:
`fixes f :: "ℝ vec['n] ⇒ real"
and x :: "ℝ vec['n]" ...
`have "vector_derivative f (at x) = (0::ℝ vec['n])"
But this is inappropriate syntax. I'm not really sure how to proceed, any help is much appreciated!
I'm not sure how you came up with that syntax. That is nowhere close to any syntax I am aware of in Isabelle.
Apart from that, vector_derivative is not the gradient. The gradient is defined for functions from a real vector space to the reals (e.g. real ^ n ⇒ real). The vector derivative is defined for functions from the reals to a real vector space (e.g. real ⇒ real ^ n).
The gradient in Isabelle is given by the gderiv predicate, with the somewhat archaic notation GDERIV f x :> D meaning that f has a gradient at x and that gradient is D.
So if you want to assume that the gradient of your function vanishes at 0, you can write that as
lemma
fixes f :: "real ^ 'n ⇒ real"
assumes "GDERIV f x :> 0"
shows foo
Note that unless you have a specific function that you're working with, it is generally nicer to replace real ^ 'n with the more general 'a :: euclidean_space. That allows you to also e.g. instantiate your theorem with types like real x real or complex that are isomorphic to a real ^ 'n but not identical to it.
I'm not sure how well-developed the library is for gderiv (the archaic notation suggests not very). If you do work with it, you might have to prove a lot of theorems yourself, and/or unfold its definition and work with the more well-established has_derivative (which is the Fréchet derivative, which generalises most other notions of derivative in Isabelle):
(GDERIV f x :> D) ⟷ (f has_derivative (λh. h ∙ D)) (at x)
where ∙ denotes the inner product.