Stream: math-comp analysis

Topic: shift in derive


view this post on Zulip 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)).

view this post on Zulip Cyril Cohen (Jan 04 2021 at 15:37):

Marie Kerjean said:

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)).

If it works, it's good to me!

view this post on Zulip Marie Kerjean (Jan 04 2021 at 16:09):

I'll draft a PR.

view this post on Zulip 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...

view this post on Zulip Reynald Affeldt (Jan 05 2021 at 01:09):

It had to do with the joint use of shift and center, no?

view this post on Zulip Marie Kerjean (Jan 12 2021 at 10:53):

@Cyril Cohen do you remember the reason for using shift and center here ?

view this post on Zulip 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.

view this post on Zulip Reynald Affeldt (Jan 12 2021 at 11:56):

which sounds like a good thing :-/

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Assia Mahboubi (Jan 19 2021 at 15:00):

My 5 cents.


Last updated: Aug 19 2022 at 19:03 UTC