Stream: math-comp analysis

Topic: derive


view this post on Zulip Marie Kerjean (Nov 19 2020 at 11:33):

Is there a lemma in derive.v stating the uniqueness of the differential of a differentiable function ? I can't find it.

view this post on Zulip Cyril Cohen (Nov 19 2020 at 11:54):

Lemma diff_unique (V W : normedModType R) (f : V -> W)
  (df : {linear V -> W}) x :
  continuous df -> f \o shift x = cst (f x) + df +o_ (0 : V) id ->
  'd f x = df :> (V -> W).

view this post on Zulip Cyril Cohen (Nov 19 2020 at 11:55):

(I guess the equality in the end should have been swapped though)

view this post on Zulip Marie Kerjean (Nov 19 2020 at 12:47):

So if I want to show that a function is derivable by providing its differential ad hoc, what should I do ? Meaning I want to prove derivable f a, by showing it is differentiable with its differential being a certain linear map.

view this post on Zulip Marie Kerjean (Nov 19 2020 at 15:29):

Am I right to undderstand that diff_unique, and all the lemmas which depend on it, do not apply to complex analysis, because the norm on V and Wneeds to target a realDomainType ? Should everything be redefined for complex analysis ?

view this post on Zulip Cyril Cohen (Nov 19 2020 at 17:35):

I guess that everything should indeed be generalized...

view this post on Zulip Assia Mahboubi (Nov 20 2020 at 10:55):

What do you mean by "generalized"? to any numFieldType?

view this post on Zulip Assia Mahboubi (Nov 20 2020 at 10:56):

Sounds a bit weird. This seems to be as an oddity of "forgetting" that the norm is not real-valued.

view this post on Zulip Cyril Cohen (Nov 20 2020 at 11:25):

I'm not sure I understand your remark

view this post on Zulip Marie Kerjean (Nov 20 2020 at 13:01):

I did not noticed it before, but using case: (real_le0P (normr_real x)) instead of case: ler0P |x| or lerP |x| 0 in several lines of derive.v should allow to generalize all the sections using a realFieldType to using a numFieldType. Do you see an obstacle or could I suggest a PR ?

view this post on Zulip Marie Kerjean (Nov 20 2020 at 13:02):

So contrarily to what I said to you earlier @Assia Mahboubi , the norm is always real-valued on any numDomainType.

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 08:31):

Hi. Is there some result in the library that allows me to compare two functions knowing their derivative (and a common point). It seems that not that much has been proved in derive.v

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 09:16):

Nevermind, the mean value theorem will do the job.

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 09:37):

By the way, if I do a Check MVT, it prints continuous f instead of {within [a, b], continuous f}.

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 09:49):

Follow-up question: how can I prove {whithin [0, 1], continuous sin} from continuous sin?

view this post on Zulip Cyril Cohen (Jul 07 2022 at 12:24):

Pierre-Yves Strub said:

Follow-up question: how can I prove {whithin [0, 1], continuous sin} from continuous sin?

https://github.com/math-comp/analysis/blob/82667438ee3f6e9b030a9654bd62e18b23d31b88/theories/topology.v#L6012-L6013 ?

view this post on Zulip Cyril Cohen (Jul 07 2022 at 12:26):

Pierre-Yves Strub said:

By the way, if I do a Check MVT, it prints continuous f instead of {within [a, b], continuous f}.

Indeed, that's an issue... https://github.com/math-comp/analysis/blob/82667438ee3f6e9b030a9654bd62e18b23d31b88/theories/topology.v#L5972-L5973 should be parsing only and complemented with a printing only notation that fetches the domain from the type of the subspace in the implicit arguments of continuous. CC @Zachary Stone what do you think?

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 12:28):

Cyril Cohen said:

Pierre-Yves Strub said:

Follow-up question: how can I prove {whithin [0, 1], continuous sin} from continuous sin?

https://github.com/math-comp/analysis/blob/82667438ee3f6e9b030a9654bd62e18b23d31b88/theories/topology.v#L6012-L6013 ?

I finally understood that I had to Import numFieldNormedType.Exports to be able to apply this lemma.

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 12:28):

Isn't this module be exported by default?

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 12:44):

I have a function that is derivable over an interval, I want to prove that it is continuous over that interval. I cannot find a way to prove it directly

view this post on Zulip Cyril Cohen (Jul 07 2022 at 13:27):

Pierre-Yves Strub said:

Isn't this module be exported by default?

This module breaks forgetful inheritance, it should definitely be documented in the header of theories/normedtype.v as "Import only locally and at your own risks" or something.

view this post on Zulip Cyril Cohen (Jul 07 2022 at 13:28):

Pierre-Yves Strub said:

I have a function that is derivable over an interval, I want to prove that it is continuous over that interval. I cannot find a way to prove it directly

https://github.com/math-comp/analysis/blob/82667438ee3f6e9b030a9654bd62e18b23d31b88/theories/derive.v#L167-L168 ?

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 13:44):

I've seen this lemma, but never managed to apply it.

view this post on Zulip Pierre-Yves Strub (Jul 07 2022 at 13:44):

I'll give more context later

view this post on Zulip Zachary Stone (Jul 07 2022 at 17:58):

Regarding the the proof of continuous sin -> {within [0,1], continuous sin}, you should be able to combine continuous_subspaceT and continuous_subspace_in. It sounds like a making this a separate lemma would be useful.

Regarding the printing, I have been frustrated by this as well. You get goals like

continuous f -> continuous f

which is super misleading. I hacked around this with the pointwise vs. uniform convergence by introducing pointwise_fun and uniform_fun, but this solution is pretty poor. I'd love some help to improve the printing.

Lastly, regarding derivable on an interval implies continuous on an interval, I am not surprised that differentiable_continuous doesn't work for free if it's using the wrong topologies. To be more helpful, I'd need to know exactly how derivable on an interval is phrased in your setting.


Last updated: Mar 28 2024 at 10:01 UTC