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: Apr 17 2024 at 20:02 UTC