about fderiv and the transformation of the types

Stream: maths

[Chenyi Li]

Hi! If I want to express the fderiv of a continuous differentiable function $f :\mathbb{R}^d \rightarrow \mathbb{R}$, that is $\nabla f : \mathbb{R}^n \rightarrow \mathbb{R}^n$ . I found the type of the fderiv at one point is as $E →L[\mathbb{K}] F$, which is $(fin \ d \rightarrow \mathbb{R}) \rightarrow L[\mathbb{R}] \ \mathbb{R}$ in this case. If I want to do the inner product $\nabla f(x)^T(y-x)$, where $x,y$ are points in $\mathbb{R}^d$. How can I accomplish this goal, or rather how can I transform the type of $\nabla f(x)$ to a type the same as $y-x$, then I can use has_inner.inner to accomplish the inner product? Thank you very much !

[Notification Bot]

This topic was moved here from #mathlib4 > about fderiv and the transformation of the types by Heather Macbeth.

[Heather Macbeth]

Hi @Chenyi Li, it sounds like you might implicitly be working with $f : E \to \mathbb{R}$ where $E$ is a finite-dimensional inner product space. Can you generalize to this situation?

[Heather Macbeth]

If you have $f: E \to \mathbb{R}$, then the fderiv $Df$ is of type $E\to (E\to_{L[\mathbb{R}]}\mathbb{R})$, so it already typechecks to consider, for $x,y:E$, the object $Df(x)(y-x)$. That object is a real number. And in fact, you're not even using an inner product on $E$ for this.

[Chenyi Li]

Let me have a try, thank you very much！