hasDerivWithinAt_pi for EuclideanSpace or Lp normed spaces

Stream: Is there code for X?

[Michael Novak]

Is there a theorem like docs#hasDerivWithinAt_pi for EuclideanSpace or normed Lp spaces? I can't find something exactly like this. Alternatively is there some other way of getting this?

[Yury G. Kudryashov]

You can add a pi version of docs#WithLp.prodContinuousLinearEquiv (probably, generalizing docs#EuclideanSpace.equiv), then combine the existing theorem with theorems about differentiabilty of ContinuousLinearEquivs.

[Michael Novak]

Yury G. Kudryashov said:

You can add a pi version of docs#WithLp.prodContinuousLinearEquiv (probably, generalizing docs#EuclideanSpace.equiv), then combine the existing theorem with theorems about differentiabilty of ContinuousLinearEquivs.

Thank you very much!

[Albert Smith]

The equiv Yury suggests already exists, I believe, as docs#PiLp.continuousLinearEquiv

[Yury G. Kudryashov]

I forgot that loogle doesn't see through abbrevs.

[Yury G. Kudryashov]

:man_facepalming: See docs#differentiableWithinAt_piLp and other lemmas in that file.

[Albert Smith]

It seems there's also docs#hasFDerivWithinAt_euclidean for the special case of Euclidean space