Marie Kerjean (Jan 04 2021 at 10:25): Marie Kerjean (Jan 04 2021 at 10:25):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
shiftinderive.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!
Marie Kerjean (Jan 04 2021 at 16:09):I'll draft a PR.
Reynald Affeldt (Jan 05 2021 at 01:08):If it works, it's good to me!
You had an explanation for favoring the use of shift iirc...
Reynald Affeldt (Jan 05 2021 at 01:09):It had to do with the joint use of shift and center, no?
Marie Kerjean (Jan 12 2021 at 10:53):@Cyril Cohen do you remember the reason for using shift and center here ?
Cyril Cohen (Jan 12 2021 at 11:40):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.
Reynald Affeldt (Jan 12 2021 at 11:56):which sounds like a good thing :-/
Reynald Affeldt (Jan 12 2021 at 11:58):I had the same question as Marie some time ago and I remembered that I bought your justification in the end :-)
Assia Mahboubi (Jan 19 2021 at 14:59):But I suggest not to call it shift, which is misleading. Moreover, the translation happens on the left, which is also not usual.
Assia Mahboubi (Jan 19 2021 at 15:00):Also, it is not that readable I would say to the price to pay for future features is a bit high.
Assia Mahboubi (Jan 19 2021 at 15:00):My 5 cents.
Last updated: Feb 05 2023 at 07:03 UTC