Commit 2024-08-16 14:45 d03203d6
View on Github →feat: define rpow
and sqrt
based on the continuous functional calculus (#15377)
This PR defines CFC.nnrpow
, CFC.sqrt
and CFC.rpow
based on the continuous functional calculus. We define two separate versions CFC.nnrpow
(based on the non-unital calculus) and CFC.rpow
(unital) due to what happens at 0. Since NNReal.rpow 0 0 = 1
, this means that this function does not map zero to zero when the exponent
is zero, and hence CFC.nnrpow a 0 = 0
whereas CFC.rpow a 0 = 1
.