Derivative of projections in euclidean space

Stream: Is there code for X?

[Eric Wieser]

Do we have the following?

nonrec theorem EuclideanSpace.hasStrictFDerivAt_apply {ι} {𝕜} [RCLike 𝕜] (i : ι)
    (f : EuclideanSpace 𝕜 ι) :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun f : EuclideanSpace 𝕜 ι => f i) (EuclideanSpace.proj i) f := by
  have := hasStrictFDerivAt_apply (𝕜 := 𝕜) i (F' := fun _ => 𝕜) (f := f)
  -- derivatives are a function of the chosen norm; `this` is about the right topology
  -- but the wrong norm, so we can't use it
  sorry

I think the "generalizing deriv to TVS" thread would make this just work, but in the meantime maybe we already have this elsewhere?

[Eric Wieser]

(I now have a short proof of this and some related machinery)

[Eric Wieser]

Some generalization en-route: #17663

[Yury G. Kudryashov]

You can compose hasStrictFDerivAt_apply with a ContinuousLinearEquiv between PiLp and the pi type.

[Eric Wieser]

Yep, that is the proof I came up with in #17665

[Yury G. Kudryashov]

... or you can take over #9675

[Eric Wieser]

We want #17665 anyway, though the proofs will indeed be shorter after #9675