Complex.hasSum_taylorSeries_neg_log
theorem Complex.hasSum_taylorSeries_neg_log : ∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => z ^ n / ↑n) (-(1 - z).log) := by
sorry
This theorem states that for any complex number `z` with its norm less than 1 (i.e., `z` is within the open unit disk), the series formed by the terms `z^n/n` (where `n` ranges over all natural numbers) converges to the negative logarithm of `(1-z)`. In mathematical terms, it's equivalent to saying that the series `∑ z^n/n` is equal to `-log (1-z)` for `z` in the open unit disk.
More concisely: For complex numbers `z` with norm less than 1, the series `∑ (1/n * z^n)` converges to `-log(1-z)`.
|
Complex.norm_log_one_sub_inv_add_logTaylor_neg_le
theorem Complex.norm_log_one_sub_inv_add_logTaylor_neg_le :
∀ (n : ℕ) {z : ℂ},
‖z‖ < 1 → ‖(1 - z)⁻¹.log + Complex.logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
The theorem states that for any natural number `n` and any complex number `z` with norm less than 1, the norm of the difference between the logarithm of the inverse of `(1 - z)` and the `(n+1)`st Taylor polynomial of `log` at `-z` can be bounded above. Specifically, the upper bound is given by the `(n + 1)`st power of the norm of `z` times the reciprocal of `(1 - ‖z‖)`, all divided by `(n + 1)`.
More concisely: For any natural number `n` and complex number `z` with norm less than 1, the norm of the difference between the logarithm of the inverse of `(1 - z)` and the `(n+1)`st Taylor polynomial of `log` at `-z` is bounded above by `|z|^{n+1}/(1-|z|)`.
|
Complex.log_inv_eq_integral
theorem Complex.log_inv_eq_integral :
∀ {z : ℂ}, 1 - z ∈ Complex.slitPlane → (1 - z)⁻¹.log = z * ∫ (t : ℝ) in 0 ..1, (1 - t • z)⁻¹
This theorem states that for any complex number `z`, if `1 - z` belongs to the slit plane (i.e., the complex plane with the closed negative real axis removed), then the natural logarithm of the inverse of `1 - z` can be expressed as `z` times the integral from 0 to 1 of the inverse of `(1 - t * z)`, where `t` is a real number.
More concisely: For complex numbers `z`, if `1 - z` lies in the slit complex plane, then `ln(1 / (1 - z)) = ∫(0,1) dt / (1 - t * z)`.
|
Complex.norm_log_sub_logTaylor_le
theorem Complex.norm_log_sub_logTaylor_le :
∀ (n : ℕ) {z : ℂ}, ‖z‖ < 1 → ‖(1 + z).log - Complex.logTaylor (n + 1) z‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
The theorem `Complex.norm_log_sub_logTaylor_le` states that for any natural number `n` and any complex number `z` with the norm of `z` less than 1, the difference between the complex logarithm of `1 + z` and the `(n+1)`-th Taylor polynomial of the complex logarithm at `z` is bounded by the `(n + 1)`-th power of the norm of `z` times the inverse of `1 - ‖z‖`, all divided by `n + 1`. This gives an estimate of the error when approximating the complex logarithm by its Taylor polynomial.
More concisely: For any complex number `z` with norm less than 1 and natural number `n`, the difference between the complex logarithm of `1 + z` and the `(n+1)`-th Taylor polynomial of the complex logarithm at `z` is bounded by `‖z‖^(n+1) / (n+1) (1 - ‖z‖)`.
|
Complex.norm_log_one_add_sub_self_le
theorem Complex.norm_log_one_add_sub_self_le : ∀ {z : ℂ}, ‖z‖ < 1 → ‖(1 + z).log - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 := by
sorry
The theorem `Complex.norm_log_one_add_sub_self_le` states that for any complex number `z` with norm less than 1, the norm of the difference between the logarithm of `1 + z` and `z` itself is less than or equal to half the square of the norm of `z` divided by `(1 - norm of z)`. Essentially, this provides an upper bound for the difference between the logarithm of `1 + z` and `z` in terms of the norm of `z`.
More concisely: For any complex number `z` with norm less than 1, the norm of the logarithm of `(1 + z)` minus `z` is less than or equal to `0.5 * norm(z) ^ 2 / (1 - norm(z))`.
|
Complex.log_eq_integral
theorem Complex.log_eq_integral :
∀ {z : ℂ}, 1 + z ∈ Complex.slitPlane → (1 + z).log = z * ∫ (t : ℝ) in 0 ..1, (1 + t • z)⁻¹
The theorem `Complex.log_eq_integral` expresses that, for every complex number `z`, if `1 + z` belongs to the slit plane (that is, the real part of `1 + z` is greater than zero or the imaginary part of `1 + z` is not zero), then the logarithm of `1 + z` can be represented as an integral from 0 to 1 of the inverse of `1 + t • z`, where `t` is a real number and '•' denotes scalar multiplication. Essentially, this theorem provides an integral representation for the complex logarithm of `1 + z` in the context of complex numbers that fall within the slit plane.
More concisely: If complex number `1 + z` lies in the slit plane, then the logarithm of `1 + z` equals the integral from 0 to 1 of the inverse of `1 + t • z` with respect to `dt`.
|
Complex.hasSum_taylorSeries_log
theorem Complex.hasSum_taylorSeries_log :
∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (1 + z).log
The theorem `Complex.hasSum_taylorSeries_log` states that for any complex number `z` with its norm less than 1, the Taylor series of the complex logarithm at `1` converges to the logarithm of `(1 + z)`. The Taylor series is given by the expression `(-1) ^ (n + 1) * z ^ n / ↑n`, where `n` ranges over natural numbers.
More concisely: For complex numbers `z` with norm less than 1, the Taylor series of the complex logarithm centered at 1, given by `(-1) ^ (n + 1) * z ^ n / ↑n`, converges to the complex logarithm of `(1 + z)`.
|
Complex.norm_one_add_mul_inv_le
theorem Complex.norm_one_add_mul_inv_le :
∀ {t : ℝ}, t ∈ Set.Icc 0 1 → ∀ {z : ℂ}, ‖z‖ < 1 → ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
This theorem provides a bound on the norm of the complex function `(1 + t * z)⁻¹`, where `t` is a real number between 0 and 1 (inclusive), and `z` is a complex number with a norm less than 1. Specifically, it states that for these conditions, the norm of `(1 + t * z)⁻¹` is less than or equal to `(1 - ‖z‖)⁻¹`.
More concisely: For complex numbers `z` with norm less than 1 and real numbers `t` between 0 and 1, the norm of `(1 + t * z)⁻¹` is bounded by `(1 - ‖z‖)⁻¹`.
|
Complex.norm_log_one_sub_inv_sub_self_le
theorem Complex.norm_log_one_sub_inv_sub_self_le :
∀ {z : ℂ}, ‖z‖ < 1 → ‖(1 - z)⁻¹.log - z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2
This theorem states that for any complex number `z` with a norm less than one (`‖z‖ < 1`), the norm of the difference between the log of the reciprocal of `1-z` and `z` itself (‖(1 - z)⁻¹.log - z‖) is less than or equal to the square of the norm of `z` divided by twice the difference between 1 and the norm of `z` (`‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2`). In mathematical notation, this is:
‖(1 - z)⁻¹.log - z‖ ≤ ‖z‖^2/(2*(1-‖z‖)) for all complex `z` with ‖z‖ < 1.
More concisely: For any complex number `z` with norm less than one, the norm of the difference between the log of its reciprocal and `z` is bounded above by the square of the norm of `z` divided by twice the difference between 1 and the norm of `z`.
|