What is the reason for the use of shift
in derive.v
, when defining differentiability:
Definition derive (f : V -> W) a v :=
lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
Wouldn't it be more readable and usable to use :
Definition derive (f : V -> W) a v :=
lim ((fun h => h^-1 *: ((f ( a + h *: v) - f a)) @ nbhs' (0 : R^o)).
Marie Kerjean said:
What is the reason for the use of
shift
inderive.v
, when defining differentiability:Definition derive (f : V -> W) a v := lim ((fun h => h^-1 *: ((f \o shift a) (h *: v) - f a)) @ nbhs' (0 : R^o)).
Wouldn't it be more readable and usable to use :
Definition derive (f : V -> W) a v := lim ((fun h => h^-1 *: ((f ( a + h *: v) - f a)) @ nbhs' (0 : R^o)).
If it works, it's good to me!
I'll draft a PR.
If it works, it's good to me!
You had an explanation for favoring the use of shift
iirc...
It had to do with the joint use of shift
and center
, no?
@Cyril Cohen do you remember the reason for using shift
and center
here ?
Sure ... it was an easy way to factor a function into continous parts (and in the future affine, polynomia, algebraic, etc)... and also a way to enforce everyone uses additions to the same side.
which sounds like a good thing :-/
I had the same question as Marie some time ago and I remembered that I bought your justification in the end :-)
But I suggest not to call it shift
, which is misleading. Moreover, the translation happens on the left, which is also not usual.
Also, it is not that readable I would say to the price to pay for future features is a bit high.
My 5 cents.
Last updated: Feb 05 2023 at 07:03 UTC