Stream: math-comp analysis

Topic: Square root on ereals


view this post on Zulip Alessandro Bruni (Feb 10 2023 at 12:55):

Hi, I'm trying to express use Num.sqrt on extended reals, but failing. Currently the PR on lebesgue-stieltjes has the following function which I was using:

Definition funEFin {R : numDomainType} (f : R -> R) : \bar R -> \bar R :=
  fun x => if x is r%:E then (f r)%:E else x.

But using it is problematic because it maps -oo to -oo, while Num.sqrt requires that the number be non-negative. Do you have a recommendation for how to proceed?

view this post on Zulip Reynald Affeldt (Feb 10 2023 at 13:14):

It is not a real answer but can't you use, say, fun x => (Num.sqrt (fine x))%:E ?

view this post on Zulip Alessandro Bruni (Feb 10 2023 at 13:26):

Fixed, thanks :)

view this post on Zulip Reynald Affeldt (Feb 10 2023 at 13:28):

or fun x => if x is +oo then +oo else (sqrtr (fine x)%:R ?

view this post on Zulip Reynald Affeldt (Feb 10 2023 at 13:31):

(in any case it looks like you maybe need to develop a small theory.)

view this post on Zulip Alessandro Bruni (Feb 10 2023 at 13:44):

Yes indeed

view this post on Zulip Karl Palmskog (Feb 10 2023 at 14:32):

hmm, is this related to mathcomp-analysis?

view this post on Zulip Karl Palmskog (Feb 10 2023 at 14:33):

I ask because we try to collect topics in the right stream, which may be #math-comp analysis here?

view this post on Zulip Pierre Roux (Feb 10 2023 at 14:37):

Indeed you're right, ereal.v currently lives in MC Analysis

view this post on Zulip Notification Bot (Feb 10 2023 at 14:40):

This topic was moved here from #math-comp users > Square root on ereals by Karl Palmskog.


Last updated: Jun 25 2024 at 18:02 UTC