Is there a lemma in `derive.v`

stating the uniqueness of the differential of a differentiable function ? I can't find it.

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

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.

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 ?

I guess that everything should indeed be generalized...

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

?

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

I'm not sure I understand your remark

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 ?

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

.

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

Nevermind, the mean value theorem will do the job.

By the way, if I do a `Check MVT`

, it prints `continuous f`

instead of `{within [a, b], continuous f}`

.

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

from `continuous sin`

?

Pierre-Yves Strub said:

Follow-up question: how can I prove

`{whithin [0, 1], continuous sin}`

from`continuous sin`

?

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?

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.

Isn't this module be exported by default?

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 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.

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

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

I'll give more context later

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