Marie Kerjean (Nov 19 2020 at 11:33): 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.
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).
(I guess the equality in the end should have been swapped though)
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.
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 ?
Cyril Cohen (Nov 19 2020 at 17:35):I guess that everything should indeed be generalized...
Assia Mahboubi (Nov 20 2020 at 10:55):What do you mean by "generalized"? to any numFieldType?
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.
Cyril Cohen (Nov 20 2020 at 11:25):I'm not sure I understand your remark
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 ?
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.
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
Pierre-Yves Strub (Jul 07 2022 at 09:16):Nevermind, the mean value theorem will do the job.
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}.
Pierre-Yves Strub (Jul 07 2022 at 09:49):Follow-up question: how can I prove {whithin [0, 1], continuous sin} from continuous sin?
Cyril Cohen (Jul 07 2022 at 12:24):Pierre-Yves Strub said:
Follow-up question: how can I prove
{whithin [0, 1], continuous sin}fromcontinuous sin?
Cyril Cohen (Jul 07 2022 at 12:26):Pierre-Yves Strub said:
By the way, if I do a
Check MVT, it printscontinuous finstead 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?
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}fromcontinuous sin?
I finally understood that I had to Import numFieldNormedType.Exports to be able to apply this lemma.
Pierre-Yves Strub (Jul 07 2022 at 12:28):Isn't this module be exported by default?
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
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.
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
Pierre-Yves Strub (Jul 07 2022 at 13:44):I've seen this lemma, but never managed to apply it.
Pierre-Yves Strub (Jul 07 2022 at 13:44):I'll give more context later
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: Oct 13 2024 at 01:02 UTC