Complex.log_one
theorem Complex.log_one : Complex.log 1 = 0
This theorem states that the complex logarithm of 1 equals 0. In other words, if you take the logarithm of 1 in the complex number system, the result is 0. This is consistent with the mathematical fact that the logarithm of 1 (for any base) is always 0, extended to the complex number domain.
More concisely: The complex logarithm of 1 is equal to 0.
|
Complex.log_im
theorem Complex.log_im : ∀ (x : ℂ), x.log.im = x.arg
The theorem `Complex.log_im` states that for all complex numbers `x`, the imaginary part of the natural logarithm of `x` is equal to the argument of `x`. This means that when you take the natural logarithm of a complex number and then obtain the imaginary part of the result, it is the same as getting the argument of the original complex number. The "argument" of a complex number is the angle it makes with the positive real axis when represented in polar coordinates.
More concisely: The theorem `Complex.log_im` asserts that for all complex numbers x, Im (log x) = Arg x, where log is the natural logarithm, Im denotes the imaginary part, and Arg represents the argument.
|
Complex.range_exp
theorem Complex.range_exp : Set.range Complex.exp = {0}ᶜ
The theorem `Complex.range_exp` states that the range of the complex exponential function, defined as `Complex.exp`, is the set of all complex numbers excluding zero. In other words, every complex number except zero can be obtained as the exponential of some complex number, and zero cannot be obtained this way. In mathematical notation, this can be written as $\mathrm{range}(\exp) = \mathbb{C} \setminus \{0\}$.
More concisely: The complex exponential function, `Complex.exp`, maps complex numbers to all non-zero complex numbers.
|
Complex.ofReal_log
theorem Complex.ofReal_log : ∀ {x : ℝ}, 0 ≤ x → ↑x.log = (↑x).log
This theorem states that for any real number `x` that is greater than or equal to zero, the real logarithm of `x` when converted to a complex number equals the complex logarithm of `x` when it is treated as a complex number. This theorem links the real logarithm and the complex logarithm functions, asserting that they align for non-negative real numbers.
More concisely: For any non-negative real number x, the real logarithm of x is equal to the complex logarithm of x treated as a complex number.
|
Complex.log_exp
theorem Complex.log_exp : ∀ {x : ℂ}, -Real.pi < x.im → x.im ≤ Real.pi → x.exp.log = x
The theorem `Complex.log_exp` states that for any complex number `x`, if the imaginary part of `x` is strictly greater than negative pi and less than or equal to pi, then the logarithm of the exponential of `x` is equal to `x` itself. This captures an important property of the logarithmic and exponential functions in the complex domain, namely that the logarithm and exponential functions are inverses of each other within these bounds on the imaginary part.
More concisely: For complex numbers x with imag(x) ≤ pi and imag(x) > -π, log (exp x) = x.
|
Set.Countable.preimage_cexp
theorem Set.Countable.preimage_cexp : ∀ {s : Set ℂ}, s.Countable → (Complex.exp ⁻¹' s).Countable
This theorem, known as `Set.Countable.preimage_cexp`, states that for any countable set `s` of complex numbers, the preimage of `s` under the complex exponential function is also countable. In simpler terms, it says that if we have a countable set of complex numbers, and we consider all the complex numbers such that their exponential is in our original set, then this new set is also countable.
More concisely: If `s` is a countable set of complex numbers, then the preimage of `s` under the complex exponential function is also countable.
|
Complex.log_re
theorem Complex.log_re : ∀ (x : ℂ), x.log.re = (Complex.abs x).log
The theorem `Complex.log_re` states that for any complex number `x`, the real part of the natural logarithm of `x` (as computed by the `Complex.log` function) is equal to the natural logarithm of the absolute value of `x` (computed by the `Real.log` function after obtaining the absolute value using `Complex.abs`). This essentially connects the concepts of logarithms and absolute values in the realms of both real and complex numbers.
More concisely: The real part of the complex logarithm `Complex.log x` equals the natural logarithm of the absolute value `Real.log (Complex.abs x)` for any complex number `x`.
|
Complex.log_mul
theorem Complex.log_mul :
∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → (x * y).log = x.log + y.log
This theorem, called `Complex.log_mul`, states that for any two non-zero complex numbers `x` and `y`, if the sum of their arguments belongs to the left-open right-closed interval from `-π` to `π` (where `π` is the mathematical constant Pi), then the natural logarithm of their product equals the sum of their individual natural logarithms.
More concisely: If the arguments of two non-zero complex numbers fall within the interval `(-π, pi]`, then `log (x * y) = log x + log y`.
|
Complex.exp_log
theorem Complex.exp_log : ∀ {x : ℂ}, x ≠ 0 → x.log.exp = x
This theorem states that, for any non-zero complex number `x`, the exponential of the logarithm of `x` equals `x` itself. In other words, the functions `Complex.exp` and `Complex.log` are inverses of each other when the domain is the set of non-zero complex numbers. This mirrors the standard property of exponential and logarithm functions in real number mathematics.
More concisely: For any non-zero complex number `x`, `Complex.exp (Complex.log x) = x` holds. (The functions `Complex.exp` and `Complex.log` are inverses on the non-zero complex numbers.)
|