partial derivatives guide#800
Conversation
Looks good Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
|
Thanks Tomáš! I think this is useful but you should clearly say this guide is intended for downstream users, not further contributions to Mathlib, and explicitly point out that the Mathlib way is to replace |
| Given a function $$f : \mathbb{R}^n \to \mathbb{R}^m$$, how do you write $$\frac{\partial f}{\partial x_i}$$ in Lean? | ||
|
|
||
| Lean represents $$\mathbb{R}^n$$ as `EuclideanSpace ℝ (Fin n)`. You can express partial derivatives using the `fderiv` function and the basis vector `single i 1`: | ||
|
|
There was a problem hiding this comment.
I think it would be really great, if this was qualified somewhat: if you want to contribute to mathlib, in almost all cases {E : Type*} [NormedAddCommGroup E] [InnerProductSpace \R E] [FiniteDimensional \R E] and you can just work with the derivative and it is generally possible to rephrase your theorem in terms of fderiv. If you are not in mathlib and really want to talk about the concrete EuclideanSpace ℝ (Fin n), then the above applies
5 participants
Added guide for partial derivatives based on my Zulip post #new members > partial derivative of a vector field @ 💬