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?

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

?

Fixed, thanks :)

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

?

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

Yes indeed

hmm, is this related to mathcomp-analysis?

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

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

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