Representing n-times differentiable fn in theorem statement

Stream: new members

[Anika-Roy]

img.png
Hello!
I'm a beginner in lean and trying to formalize this theorem statement, using mathlib4. I'm confused about how to go about defining a function that is n-times differentiable. Could anyone help me out?

I apologize if this should be asked on another channel, please redirect me to the same!

[Tomas Skrivan]

I think you are looking for docs#ContDiff

[Tomas Skrivan]

It also assumes that n-th derivative is also continuous.

[Ruben Van de Velde]

So maybe ContDiff (n-1)?

[Sébastien Gouëzel]

I'd say first try to prove your lemma assuming ContDiff n, and only then consider generalizing if you really need the stronger result where the function is just C^{n-1} with differentiable (n-1)-th derivative.

[Anika-Roy]

That was very helpful, thank you to all!
I'll definitely try again myself :+1: