Whitney Extension Theorem (even in 1-d)

Stream: Is there code for X?

[Matthew Cushman]

Does there exist any formalization of the Whitney Extension theorem? I'm mainly looking for the simplest 1-d case: given a smooth function on the non-negative reals (smooth on positive, with one-sided derivatives of all orders and those derivatives have limits at 0), it can be extended to a smooth function on all of R.

[Michael Rothgang]

CC @Yury G. Kudryashov in case you also thought about this. (I know you formalised "baby Whitney embedding", and that the full version requires Sard's theorem.)

[Michael Rothgang]

Searching zulip turns up almost nothing: this was discussed, but AFAICT nobody ever worked on this.

[Michael Rothgang]

It would be nice to have. (If the proof is not much harder in n-dimenions, going straight for that would be nice.)

[Yury G. Kudryashov]

This question is about Whitney extension thm, not Whitney embedding thm.

[Yury G. Kudryashov]

For dimension one, I think that we should add (if we don't have it yet) a theorem saying that you can achieve any Taylor series you want.

[Matthew Cushman]

Makes sense, this is what I am thinking of doing as well (afaict it’s not in mathlib yet)

[Yury G. Kudryashov]

AFAIR, @Terence Tao recently mentioned Whitney Extension Theorem in another thread. What's the current set of best theorems in this direction? How long are the proofs?