## Stream: math-comp analysis

### Topic: derive

#### 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).
``````

#### Cyril Cohen (Nov 19 2020 at 11:55):

(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 `W`needs 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}` from `continuous sin`?

#### 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?

#### 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`?

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: Jun 22 2024 at 16:02 UTC