continuously differentiable

Stream: Is there code for X?

[Alex Kontorovich]

We have ContinuousOn f U and DifferentiableOn k f U; is there something like ContinuouslyDifferentiable? Or is the way people handle this to just say that there is both f and f' and f' is continuous and HasDerivAt f (f' x) x? Thanks!

[Anatole Dedecker]

We have docs#ContDiff (and all the usual variants). But it may be annoying to specialize to get nice statements specialized for $n=1$

[Alex Kontorovich]

Got it, thanks! Ok so for $n=1$, it might be easier just to do it "bare hands"..?

[Anatole Dedecker]

I haven’t tried, but it might indeed be easier. OTOH it will never get better if everyone avoids it, and certainly in mathlib we would very much prefer having better API for the general case rather than doing it manually…

[Alex Kontorovich]

So it would be "nice" if someone were to develop API for ContDiff in the case $n=1$...?

[Yury G. Kudryashov]

What kind of API specific to the case $n=1$ are you looking for?

[Anatole Dedecker]

What I meant is: in an ideal world where you have an infinite amount of time, you should try to use docs#ContDiff and fix the API so that it's not annoying to use in your case