## Stream: math-comp analysis

### Topic: shift in derive

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

#### 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!

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