Corestriction of a differentiable function

Stream: new members

[Sophie Morel]

Hi, I wonder if the following result is in mathlib:
Let f:E->F be a smooth function between normed vector spaces, let F' be a subspace of F that contains the image of f. Then the corestriction of f, a function from E to F', is also smooth.

In fact it should be an if and only if, but I only need the direction I stated. Also, I'm pretty sure that I can prove it by hand, but I'm lazy and would like to avoid reinventing the wheel.

I read analysis.calculus.cont_diff but couldn't find that kind of result. I also don't see similar results for functions between manifolds.

[Patrick Massot]

I don't think we have that lemma. I will prove it tonight if @Sebastien Gouezel or @Yury G. Kudryashov don't do it in the mean time.

[Sebastien Gouezel]

I don't think we have that, but it would definitely be a welcome addition to mathlib!

[Sebastien Gouezel]

Note that this result is very easy if F' is complemented, i.e., admits a closed supplement, because then the corestriction is the composition of f with the projection on F' with respect to the closed complement. But I think it should hold even without this assumption (because all the successive derivatives will takes values in F', and can therefore also be corestricted).

[Sophie Morel]

Thanks ! In my case, F' is obviously complemented (it is a closed hyperplane), so I'm happy that I did not start immediately trying to construct derivatives with values in F' before Sébastien pointed out that there is a shortcut in that case.
Also, to be honest, I did not think about the case of functions differentiable on a subset of E (where derivatives are not necessarily unique), so I am not sure what should happen there.

Related question: is the notion of submanifold in mathlib ? I tried to find that of immersions, but the only mentions I could find are in the section of the Whitney embedding theorem, and I didn't find a definition of immersions there.

[Sebastien Gouezel]

No, we have no submanifolds, immersions, submersions and so on. That's definitely on the agenda, but for after the port.

[Yury G. Kudryashov]

Do you assume that F' is a closed subspace?

[Sophie Morel]

Probably, I don't see how to make the proof work without that assumption. Good point.

[Sebastien Gouezel]

It's definitely wrong if you don't assume that F' is closed.

[Sebastien Gouezel]

It's also wrong for functions defined on subsets. Here is a silly example. Let F' be a subspace of F which is not complemented. Consider the function f : F -> Fwhich is the identity on F', and 0 elsewhere. It is differentiable within F' (one can for instance take for differential the identity), but the corestriction is not differentiable within F'. Indeed, a derivative would be a linear map from F to F' equal to the identity on F', i.e., a projection on F'. A kernel of this projection would be a complement to F', contradiction.

[Sebastien Gouezel]

Example showing that F' needs to be closed. Let f (z) = (1, z, z^2, ...) from the complex unit disk to the space F = l^1 of summable sequences. Let F' be the span of the values of f. Then f is differentiable as a function to F (it is even analytic), but its derivative at 0 is (0, 1, 0, 0, ...) which does not belong to F' (one can check that with Vandermonde determinants) so f is not differentiable as a function to F'.

[Patrick Massot]

While hiking I also thought that assuming F' closed was probably necessary. Is there still anything that needs to be urgently proved?

[Sophie Morel]

As far as I'm concerned nothing is urgent, because I can always use a continuous retraction on F' (which exists in my case) to get the result, as Sébastien suggested. I want to construct the retraction anyway for other reasons.

[Patrick Massot]

Ok, good.

[Sophie Morel]

Oh, there is nothing good about the code that I've been writing this afternoon, believe me... :face_vomiting:

[Yury G. Kudryashov]

It is probably true for partial functions in terms of cont_diff_within_at.