feat: variational adjoint for adjoint, fderiv, gradient and deriv

[lecopivo]

Variational adjoint of adjoint, fderiv, gradient, deriv, prod.mk, prod.fst, prod.snd and corresponding theorems for HasVarAdjDerivAt

[lecopivo]

At this point you could formulate

lemma fmap (f : Y -> V -> W) (F : (X -> U) -> (Y -> V)) (hF : IsLocalizedFunctionTransform F): IsLocalizedFunctionTransform (fun g y => f y (F g y)) := ...

Then proof of add would be something like

apply fmap (f:= fun _ y => y.1 + y.2) (F:=fun g x => (F g x, G g x))
apply prod hF hG

[lecopivo]

But you can leave it as it is

[lecopivo]

Excelent work! Refactor exactly as I had in mind and great that HasVarAdjoint.adjFDeriv_apply is done!

[jstoobysmith]

Ok, so I think that is all the sorries filled in except divergence_smul, where I have put sorryful attribute. Nothing depends on this lemma anyway. I think it is then a case of tidying and then at somepoint putting your proof of the Euler-lagrange equations.

[jstoobysmith]

I believe I've now fixed all the linters etc. I also added your proof of the Euler-lagrange equation for a particle (needed to modify it a bit).

I suspect there are lots of proofs that could be golfed and/or generalized here, but I think it might be best to merge this PR now, and then we can make these changes in future ones. E.g. I haven't made the change with the Norm₂ yet.