Complex.normSq_eq_abs
theorem Complex.normSq_eq_abs : ∀ (x : ℂ), Complex.normSq x = Complex.abs x ^ 2
This theorem states that for any complex number `x`, the square of its absolute value (denoted as `Complex.abs x ^ 2`) is equal to its squared norm (denoted as `Complex.normSq x`). In other words, it asserts the equivalence between the square of a complex number's absolute value and its norm squared. This is closely related to the Pythagorean theorem in the complex number realm, as the absolute value and squared norm are the counterparts of the length of the hypotenuse and the sum of the squares of the other two sides, respectively.
More concisely: For any complex number x, the square of its absolute value equals its squared norm (i.e., Complex.abs x ^ 2 = Complex.normSq x).
|
Complex.abs_of_nonneg
theorem Complex.abs_of_nonneg : ∀ {r : ℝ}, 0 ≤ r → Complex.abs ↑r = r
This theorem states that for any real number `r` that is greater than or equal to zero (non-negative), the complex absolute value of `r` is equal to `r` itself. The complex absolute value function is defined as the square root of the complex norm squared, and this theorem provides a specific property of this function when applied to non-negative real numbers. Essentially, it tells us that the magnitude of a non-negative real number in the complex plane is just the number itself.
More concisely: For any non-negative real number `r`, the complex absolute value of `r` equals `r`. In other words, `|r| = r` for all `r ≥ 0`.
|
Complex.sq_abs
theorem Complex.sq_abs : ∀ (z : ℂ), Complex.abs z ^ 2 = Complex.normSq z
The theorem `Complex.sq_abs` states that for any complex number `z`, the square of the absolute value of `z` is equal to the norm squared of `z`. In mathematical terms, if `z` is a complex number, then `|z|^2 = z.re^2 + z.im^2`, where `|z|` denotes the absolute value of `z`, `z.re` denotes the real part of `z`, and `z.im` denotes the imaginary part of `z`. The absolute value of a complex number is the square root of the norm squared, so squaring the absolute value gives us back the norm squared.
More concisely: The square of the absolute value of a complex number equals the sum of the squares of its real and imaginary parts. (i.e. |z|^2 = z.re^2 + z.im^2)
|
Complex.abs_im_le_abs
theorem Complex.abs_im_le_abs : ∀ (z : ℂ), |z.im| ≤ Complex.abs z
The theorem `Complex.abs_im_le_abs` states that for any complex number `z`, the absolute value of the imaginary part of `z`, denoted as `|z.im|`, is less than or equal to the absolute value of `z` itself. In mathematical terms, this is saying that for any complex number `z`, the modulus of its imaginary part is always less than or equal to the modulus of the complex number.
More concisely: For any complex number z, |z.im| ≤ |z|.
|
Complex.abs_re_le_abs
theorem Complex.abs_re_le_abs : ∀ (z : ℂ), |z.re| ≤ Complex.abs z
This theorem states that for any complex number `z`, the absolute value of the real part of `z`, denoted by `|z.re|`, is less than or equal to the absolute value of `z` itself, denoted by `Complex.abs z`. In other words, the magnitude of the real component of a complex number can never exceed the magnitude of the complex number itself.
More concisely: The absolute value of the real part of a complex number is less than or equal to its absolute value. |z.re| ≤ |z| for all complex numbers z.
|
Complex.abs_abs
theorem Complex.abs_abs : ∀ (z : ℂ), |Complex.abs z| = Complex.abs z
The theorem `Complex.abs_abs` states that for all complex numbers `z`, the absolute value of the absolute value of `z` is equal to the absolute value of `z`. This theorem essentially asserts the non-negativity of the complex absolute value, since taking the absolute value of a real number always yields a non-negative number.
More concisely: For all complex numbers z, ||z|| = |z|.
|
Complex.abs_ofReal
theorem Complex.abs_ofReal : ∀ (r : ℝ), Complex.abs ↑r = |r|
This theorem states that for any real number `r`, the absolute value of `r`, when treated as a complex number, is equal to the absolute value of `r` in the real number domain. In other words, when we interpret a real number as a complex number and calculate its complex absolute value, we get the same result as if we had just computed the normal absolute value of the real number.
More concisely: For any real number `r`, the absolute value of `r` as a complex number equals the absolute value of `r` in the real numbers. (abs(r) = abs(complex of r) in Lean 4)
|
Complex.isCauSeq_re
theorem Complex.isCauSeq_re : ∀ (f : CauSeq ℂ ⇑Complex.abs), IsCauSeq abs fun n => (↑f n).re
The theorem `Complex.isCauSeq_re` states that for any Cauchy sequence `f` of complex numbers, when we consider the sequence formed by taking the real part of each term in `f`, this new sequence is also a Cauchy sequence. In other words, if `f` is a Cauchy sequence in the complex numbers (with respect to the complex absolute value function), then the sequence of real parts of `f` is a Cauchy sequence (with respect to the absolute value function for real numbers).
More concisely: If `f` is a Cauchy sequence of complex numbers, then the sequence of real parts of `f` is a Cauchy sequence of real numbers.
|
Complex.abs_im_lt_abs
theorem Complex.abs_im_lt_abs : ∀ {z : ℂ}, |z.im| < Complex.abs z ↔ z.re ≠ 0
The theorem `Complex.abs_im_lt_abs` states that for all complex numbers `z`, the absolute value of the imaginary part of `z` is less than the absolute value of `z` if and only if the real part of `z` is not equal to zero. In mathematical terms, for all complex numbers `z`, |Im(z)| < |z| if and only if Re(z) ≠ 0.
More concisely: The absolute value of the imaginary part of a complex number is strictly less than the absolute value of the complex number if and only if its real part is non-zero.
|
Complex.abs_I
theorem Complex.abs_I : Complex.abs Complex.I = 1
This theorem states that the absolute value (the distance from the origin in the complex plane) of the imaginary unit `I` in the complex numbers is equal to 1. In mathematical terms, given the complex number `I` which is defined by real part 0 and imaginary part 1 (i.e., `I = 0 + 1i`), its absolute value is 1, as represented by `|I| = 1`.
More concisely: The absolute value of the complex number i, where i is the imaginary unit (0 + 1i), equals 1.
|
Complex.abs_conj
theorem Complex.abs_conj : ∀ (z : ℂ), Complex.abs ((starRingEnd ℂ) z) = Complex.abs z
The theorem `Complex.abs_conj` states that for every complex number `z`, the absolute value of the conjugate of `z` is equal to the absolute value of `z` itself. Here, `(starRingEnd ℂ) z` denotes the conjugate of `z`. Essentially, this theorem is asserting the mathematical fact that the absolute (or modulus) of a complex number and its conjugate are equal, i.e., if `z` is a complex number and `z*` is its conjugate, then `|z*| = |z|`.
More concisely: The absolute value of a complex number is equal to the absolute value of its conjugate.
|
Complex.abs_natCast
theorem Complex.abs_natCast : ∀ (n : ℕ), Complex.abs ↑n = ↑n
This theorem states that for every natural number `n`, the absolute value of the complex number obtained by casting `n` to a complex number is equal to the real number obtained by casting `n` to a real number. In other words, for any natural number, its absolute value remains the same whether it's considered as a complex number or a real number.
More concisely: For every natural number `n`, the absolute value of the complex number `fromNat n` is equal to the real number `fromNat n`.
|
Complex.abs_le_sqrt_two_mul_max
theorem Complex.abs_le_sqrt_two_mul_max : ∀ (z : ℂ), Complex.abs z ≤ √2 * max |z.re| |z.im|
This theorem states that for every complex number `z`, the absolute value of `z` is less than or equal to the square root of 2 multiplied by the maximum of the absolute values of the real and imaginary parts of `z`. In other words, the magnitude of a complex number is always less than or equal to the square root of 2 times the maximum of the magnitudes of its real and imaginary components.
More concisely: For every complex number z, |z| ≤ √2 max {|Re z|, |Im z|} where |z| denotes the absolute value of z and Re z and Im z represent the real and imaginary parts, respectively.
|