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.

Estimated changes

added theorem CFC.mul_self_eq
added theorem CFC.nnrpow_add
added theorem CFC.nnrpow_def
added theorem CFC.nnrpow_eq_pow
added theorem CFC.nnrpow_eq_rpow
added theorem CFC.nnrpow_inv_eq
added theorem CFC.nnrpow_inv_nnrpow
added theorem CFC.nnrpow_nnrpow
added theorem CFC.nnrpow_nnrpow_inv
added theorem CFC.nnrpow_nonneg
added theorem CFC.nnrpow_one
added theorem CFC.nnrpow_sqrt
added theorem CFC.nnrpow_sqrt_two
added theorem CFC.nnrpow_three
added theorem CFC.nnrpow_two
added theorem CFC.nnrpow_zero
added theorem CFC.one_rpow
added theorem CFC.rpow_add
added theorem CFC.rpow_algebraMap
added theorem CFC.rpow_def
added theorem CFC.rpow_eq_pow
added theorem CFC.rpow_intCast
added theorem CFC.rpow_mul_rpow_neg
added theorem CFC.rpow_natCast
added theorem CFC.rpow_neg
added theorem CFC.rpow_neg_mul_rpow
added theorem CFC.rpow_nonneg
added theorem CFC.rpow_one
added theorem CFC.rpow_rpow
added theorem CFC.rpow_sqrt
added theorem CFC.rpow_sqrt_nnreal
added theorem CFC.rpow_zero
added theorem CFC.sq_sqrt
added theorem CFC.sqrt_algebraMap
added theorem CFC.sqrt_eq_cfc
added theorem CFC.sqrt_eq_iff
added theorem CFC.sqrt_eq_nnrpow
added theorem CFC.sqrt_eq_rpow
added theorem CFC.sqrt_mul_self
added theorem CFC.sqrt_mul_sqrt_self
added theorem CFC.sqrt_nnrpow
added theorem CFC.sqrt_nnrpow_two
added theorem CFC.sqrt_nonneg
added theorem CFC.sqrt_one
added theorem CFC.sqrt_rpow
added theorem CFC.sqrt_rpow_nnreal
added theorem CFC.sqrt_sq
added theorem CFC.sqrt_unique
added theorem CFC.sqrt_zero
added theorem CFC.zero_nnrpow
added theorem CFC.zero_rpow
added theorem NNReal.nnrpow_def