Commit 2022-04-21 12:09 ba455ea6

View on Github →

feat(special_functions/pow): continuity of real to complex power (#13244) Some lemmas excised from my Gamma-function project. The main result is that for a complex s with re s > 0, the function (λ x, x ^ s : ℝ → ℂ) is continuous on all of ℝ.

Estimated changes

Modified src/analysis/special_functions/pow.lean

added theorem complex.continuous_at_cpow_const_of_re_pos

added theorem complex.continuous_at_cpow_of_re_pos

added theorem complex.continuous_of_real_cpow_const

added theorem complex.of_real_cpow_of_nonpos

Modified src/data/complex/basic.lean

added theorem complex.not_lt_iff

added theorem complex.not_lt_zero_iff