Stream: math-comp analysis

Topic: ✔ Lemma for differentiable -> derivable


view this post on Zulip abab9579 (Aug 28 2022 at 09:16):

Hello, I am lost searching for a lemma giving differentiable f x -> forall v, derivable f x v. If my memory serves correctly, this one holds (while converse does not). Where is the corresponding lemma? (Or is this easily proved in some other way?)

view this post on Zulip abab9579 (Aug 30 2022 at 04:10):

apply/derivable1P/derivable1_diffP did the job, albeit I had to prove ( *:%R^~ v)is differentiable myself..

view this post on Zulip Notification Bot (Aug 30 2022 at 04:10):

abab9579 has marked this topic as resolved.

view this post on Zulip Cyril Cohen (Aug 30 2022 at 06:18):

Didn't differentiableZl do the job?

view this post on Zulip Cyril Cohen (Aug 30 2022 at 06:25):

Feel free to PR add the missing lemma to the library.

view this post on Zulip abab9579 (Aug 30 2022 at 08:29):

Oh, differentiableZl works. Dunno why I could not see it before.. Thank you!
By the way, can I know why is_diff_scalel is restricted to scaling R?

view this post on Zulip Cyril Cohen (Aug 30 2022 at 09:39):

abab9579 said:

Oh, differentiableZl works. Dunno why I could not see it before.. Thank you!
By the way, can I know why is_diff_scalel is restricted to scaling R?

I think it's a mistake and one can generalize for x : V.

view this post on Zulip Cyril Cohen (Aug 30 2022 at 09:44):

https://github.com/math-comp/analysis/pull/736


Last updated: Jun 25 2024 at 19:01 UTC