Complex.arg_real_mul
theorem Complex.arg_real_mul : ∀ (x : ℂ) {r : ℝ}, 0 < r → (↑r * x).arg = x.arg
The theorem `Complex.arg_real_mul` states that for any complex number `x` and any real number `r` greater than zero, the argument of the product of `x` and `r` (when `r` is considered as a complex number with zero imaginary part) is the same as the argument of `x`. In other words, multiplying a complex number by a positive real number doesn't change its argument. Here, the argument of a complex number is a real number in the range (-π, π] satisfying certain trigonometric conditions.
More concisely: For any complex number x and positive real number r, the argument of x \* r equals the argument of x.
|
Complex.arg_zero
theorem Complex.arg_zero : Complex.arg 0 = 0
The theorem `Complex.arg_zero` states that the argument of the complex number 0 is 0. This is derived from the definition of the argument of a complex number, which defaults to 0 when the complex number is 0.
More concisely: The argument of the complex number 0 is 0.
|
Complex.mem_slitPlane_iff_arg
theorem Complex.mem_slitPlane_iff_arg : ∀ {z : ℂ}, z ∈ Complex.slitPlane ↔ z.arg ≠ Real.pi ∧ z ≠ 0
This theorem provides an alternative characterization of the slit plane in complex analysis. Specifically, it states that a complex number `z` belongs to the slit plane if and only if its argument is not equal to π and `z` is not equal to zero. In other words, the slit plane consists of all nonzero complex numbers that do not lie on the line formed by rotating the positive real axis by an angle of π radians (or 180 degrees), which corresponds to the negative real axis.
More concisely: A complex number belongs to the slit plane if and only if its argument is neither 0 nor π.
|
Complex.arg_neg_eq_arg_sub_pi_of_im_pos
theorem Complex.arg_neg_eq_arg_sub_pi_of_im_pos : ∀ {x : ℂ}, 0 < x.im → (-x).arg = x.arg - Real.pi
This theorem states that for any complex number `x`, if the imaginary part of `x` is positive (i.e., `0 < x.im`), then the argument of the negation of `x` (i.e., `Complex.arg (-x)`) is equal to the argument of `x` subtracted by pi (i.e., `Complex.arg x - Real.pi`). In simpler terms, if we have a complex number with a positive imaginary part, the angle that its negative makes with the positive real axis is the angle made by the original number minus pi. This is based on the polar form representation of complex numbers.
More concisely: For any complex number `x` with positive imaginary part, `Complex.arg (-x) = Complex.arg x - Real.pi`.
|
Complex.arg_of_re_neg_of_im_nonneg
theorem Complex.arg_of_re_neg_of_im_nonneg :
∀ {x : ℂ}, x.re < 0 → 0 ≤ x.im → x.arg = ((-x).im / Complex.abs x).arcsin + Real.pi
This theorem states that for any complex number `x`, if the real part of `x` is negative and its imaginary part is non-negative, then the argument of `x` equals to the arcsine of the negative of the imaginary part of `x` divided by the absolute value of `x`, plus π. The argument of a complex number, often denoted as `arg(x)`, represents the angle that a line from the origin to the point representing the complex number makes with the positive real axis. The arcsin function, symbolized as `arcsin`, returns the inverse of the sine of a number. The absolute value of a complex number, `abs(x)`, is its distance from the origin in the complex plane.
More concisely: If the real part of a complex number `x` is negative and its imaginary part is non-negative, then the argument of `x` is equal to `π + arcsin(neg (Im x) / abs x)`.
|
Complex.sin_arg
theorem Complex.sin_arg : ∀ (x : ℂ), x.arg.sin = x.im / Complex.abs x
The theorem `Complex.sin_arg` states that for every complex number `x`, the sine of the argument of `x` is equal to the imaginary part of `x` divided by the absolute value of `x`. In mathematical terms, this could be written as $\sin(\arg(x)) = \frac{Im(x)}{|x|}$ for all complex numbers `x`. This relationship is fundamental in the polar form representation of complex numbers.
More concisely: The sine of the argument of a complex number equals the imaginary part divided by its absolute value: $\sin(\arg(x)) = \frac{Im(x)}{|x|}$.
|
Complex.arg_coe_angle_toReal_eq_arg
theorem Complex.arg_coe_angle_toReal_eq_arg : ∀ (z : ℂ), (↑z.arg).toReal = z.arg
This theorem states that for any complex number `z`, when you take the argument of `z` (denoted as `Complex.arg z`), convert it to a `Real.Angle` and then convert it back to a real number using `Real.Angle.toReal`, you will get the original argument of `z`. In other words, the operations of converting from the argument of a complex number to a `Real.Angle` and then back to a real number is lossless, returning the initial argument of the complex number.
More concisely: The theorem asserts that for any complex number `z`, the conversion `Real.Angle.toReal (Complex.arg z)` equals `Complex.arg z`.
|
Complex.arg_neg_eq_arg_add_pi_of_im_neg
theorem Complex.arg_neg_eq_arg_add_pi_of_im_neg : ∀ {x : ℂ}, x.im < 0 → (-x).arg = x.arg + Real.pi
The theorem `Complex.arg_neg_eq_arg_add_pi_of_im_neg` states that for any complex number `x` with a negative imaginary part, the argument of the negation of `x` (i.e., `-x`) is equal to the argument of `x` plus π. This is a property that relates the argument of a complex number and its negation, specific to the case where the imaginary part of the original complex number is negative.
More concisely: For complex numbers `x` with negative imaginary part, the argument of `-x` equals the argument of `x` + π.
|
Complex.arg_of_im_neg
theorem Complex.arg_of_im_neg : ∀ {z : ℂ}, z.im < 0 → z.arg = -(z.re / Complex.abs z).arccos
The theorem `Complex.arg_of_im_neg` states that for any complex number `z`, if the imaginary part of `z` is less than 0, then the argument of `z` (the angle in polar coordinates) is equal to the negative of the arccosine of the ratio of the real part of `z` to the absolute value of `z`. Here, the arccosine function returns values in the range [0, π], and the argument of a complex number is defined to be in the range (-π, π].
More concisely: If the imaginary part of a complex number `z` is negative, then the argument of `z` equals the negative of the arccosine of the real part of `z` divided by the absolute value of `z`. (Arguments are in the range [-π, π]).
|
Complex.arg_of_re_nonneg
theorem Complex.arg_of_re_nonneg : ∀ {x : ℂ}, 0 ≤ x.re → x.arg = (x.im / Complex.abs x).arcsin
This theorem states that for any complex number `x`, if the real part of `x` is nonnegative, then the argument of `x` is equal to the arcsine of the quotient of the imaginary part of `x` and the absolute value of `x`. In mathematical terms, if `Re(x) ≥ 0`, then `arg(x) = arcsin(Im(x) / |x|)`. Here, `Re(x)` and `Im(x)` refer to the real and imaginary parts of `x` respectively, `arg(x)` is the argument of `x`, `arcsin` is the inverse sine function, and `|x|` is the absolute value of `x`.
More concisely: If a complex number `x` has nonnegative real part, then its argument equals the arcsine of its imaginary part divided by its absolute value: `arg(x) = arcsin(Im(x) / |x|)`.
|
Complex.arg_of_im_pos
theorem Complex.arg_of_im_pos : ∀ {z : ℂ}, 0 < z.im → z.arg = (z.re / Complex.abs z).arccos
The theorem `Complex.arg_of_im_pos` states that for any complex number `z` with a positive imaginary part, the argument of `z` (denoted as `Complex.arg z`) is equal to the arccosine of the ratio of the real part of `z` to the absolute value of `z` (denoted as `Real.arccos (z.re / Complex.abs z)`). The "argument" of a complex number is the angle it makes with the positive real axis, the "arccosine" function is the inverse of the cosine function restricted to [0, π], and the "absolute value" of a complex number is the square root of the sum of the squares of its real and imaginary parts.
More concisely: For complex numbers `z` with a positive imaginary part, `Complex.arg z` equals the arccosine of the real part divided by the absolute value of `z`. That is, `Complex.arg z = Real.arccos (z.re / Complex.abs z)`.
|
Complex.arg_mul
theorem Complex.arg_mul :
∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → x.arg + y.arg ∈ Set.Ioc (-Real.pi) Real.pi → (x * y).arg = x.arg + y.arg
This theorem, `Complex.arg_mul`, is a statement about the argument function in complex number theory. Specifically, it says that for any two complex numbers `x` and `y` that are not zero, if the sum of their arguments falls within the interval from `-π` to `π` (where `π` is included and `-π` is excluded), then the argument of the product of `x` and `y` is equal to the sum of their arguments.
In mathematical terms, if `arg(x)` and `arg(y)` denote the arguments of `x` and `y` respectively, the theorem states that if `-π < arg(x) + arg(y) ≤ π`, then `arg(x*y) = arg(x) + arg(y)`.
More concisely: If the arguments of two non-zero complex numbers fall within the interval `(-π, π]`, then the argument of their product is equal to the sum of their arguments.
|
Complex.abs_mul_exp_arg_mul_I
theorem Complex.abs_mul_exp_arg_mul_I : ∀ (x : ℂ), ↑(Complex.abs x) * (↑x.arg * Complex.I).exp = x
The theorem `Complex.abs_mul_exp_arg_mul_I` states that for any complex number `x`, the product of the absolute value of `x` and the complex exponential of the imaginary unit `Complex.I` multiplied by the argument of `x` is equal to `x` itself. In mathematical terms, for any complex number `x`, `|x| * e^(arg(x) * i) = x`. This theorem essentially provides a polar form representation of a complex number, where `|x|` is the magnitude (or absolute value) and `arg(x)` is the angle (or argument) in the complex plane.
More concisely: For any complex number x, the product of its absolute value and the complex exponential of its argument times the imaginary unit is equal to x. |x| * exp(arg(x) * I) = x.
|
Complex.ext_abs_arg
theorem Complex.ext_abs_arg : ∀ {x y : ℂ}, Complex.abs x = Complex.abs y → x.arg = y.arg → x = y
The theorem `Complex.ext_abs_arg` states that for any two complex numbers 'x' and 'y', if the absolute values (or magnitudes) of 'x' and 'y' are equal and their arguments (the angles they make with the positive real axis in the complex plane) are also equal, then 'x' and 'y' are the same complex number. This theorem essentially asserts that two complex numbers are equal if and only if they have the same magnitude and the same argument, which is a fundamental property in the study of complex numbers.
More concisely: Given complex numbers x and y, if |x| = |y| and arg(x) = arg(y), then x = y.
|
Complex.arg_neg_one
theorem Complex.arg_neg_one : (-1).arg = Real.pi
The theorem `Complex.arg_neg_one` states that the argument of the complex number -1 is equal to the mathematical constant pi. This can be interpreted in the complex plane as the angle formed by -1 and the positive real axis being pi radians (or 180 degrees). In other words, using the `Complex.arg` function, which returns the principal value of the argument of a complex number (in the range (-π, π]), if we input -1 (which falls in the left half of the complex plane), we get out pi.
More concisely: The argument of the complex number -1 is equal to the mathematical constant pi.
|
Complex.arg_mul_cos_add_sin_mul_I
theorem Complex.arg_mul_cos_add_sin_mul_I :
∀ {r : ℝ}, 0 < r → ∀ {θ : ℝ}, θ ∈ Set.Ioc (-Real.pi) Real.pi → (↑r * ((↑θ).cos + (↑θ).sin * Complex.I)).arg = θ
This theorem states that for any real number `r` that is greater than zero and any real number `θ` that lies in the open-closed interval from `-π` to `π`, the argument of the complex number obtained by multiplying `r` with the sum of `cos(θ)` and `sin(θ)` times the imaginary unit `I` is equal to `θ`. In other words, it proves that the formula for converting from polar to rectangular coordinates in complex number theory holds true.
More concisely: For any real number `r > 0` and `θ` in `(-π, π]`, the argument of `r * (cos(θ) + sin(θ) * I)` equals `θ` in complex numbers.
|
Complex.arg_of_re_neg_of_im_neg
theorem Complex.arg_of_re_neg_of_im_neg :
∀ {x : ℂ}, x.re < 0 → x.im < 0 → x.arg = ((-x).im / Complex.abs x).arcsin - Real.pi
This theorem states that for any complex number `x`, if both the real part (`x.re`) and the imaginary part (`x.im`) of `x` are less than zero, then the argument of `x` (the angle in polar coordinates) is equal to the arcsine of the negative of the imaginary part of `x` divided by the absolute value of `x`, minus pi (`π`). This essentially gives a rule for determining the angle of a complex number in the lower-left quadrant of the complex plane (where both real and imaginary parts are negative).
More concisely: For complex numbers `x` with negative real and imaginary parts, the argument is given by `Arg(x) = Arcsin(neg (x.im) / abs x) - π`.
|
Complex.cos_arg
theorem Complex.cos_arg : ∀ {x : ℂ}, x ≠ 0 → x.arg.cos = x.re / Complex.abs x
This theorem states that for any non-zero complex number `x`, the real part of `x` divided by the absolute value of `x` is equal to the real cosine of the argument of `x`. In mathematical terms, this means that for all complex numbers `x ≠ 0`, we have $\cos(\arg(x)) = \frac{x_{\text{re}}}{|x|}$, where $\arg(x)$ is the argument of `x`, $x_{\text{re}}$ is the real part of `x`, and $|x|$ is the absolute value of `x`.
More concisely: For any non-zero complex number x, the real part x\_{re} is equal to the absolute value of x times the cosine of its argument, i.e., x\_{re} = |x| * cos(arg(x)).
|
Complex.abs_mul_cos_add_sin_mul_I
theorem Complex.abs_mul_cos_add_sin_mul_I :
∀ (x : ℂ), ↑(Complex.abs x) * ((↑x.arg).cos + (↑x.arg).sin * Complex.I) = x
This theorem states that for every complex number `x`, the product of the absolute value of `x` and the complex number formed by adding the cosine of the argument of `x` and the product of the sine of the argument of `x` and the imaginary unit `I`, is equal to `x` itself. In other words, it expresses a complex number in terms of its polar form. In mathematical terms, given a complex number `x`, this theorem verifies the well-known formula `x = r(cos θ + i*sin θ)`, where `r` is the absolute value of the complex number (distance from origin) and `θ` is the argument of the complex number (angle made with the real axis).
More concisely: For every complex number x, x equals the product of its absolute value and the complex number formed by the cosine and sine of its argument and the imaginary unit i.
|
Complex.arg_mul_coe_angle
theorem Complex.arg_mul_coe_angle : ∀ {x y : ℂ}, x ≠ 0 → y ≠ 0 → ↑(x * y).arg = ↑x.arg + ↑y.arg
This theorem states that for any two non-zero complex numbers `x` and `y`, the argument of the product of `x` and `y` (denoted as `Complex.arg (x * y)`) is equal to the sum of the arguments of `x` and `y` (denoted as `Complex.arg x` and `Complex.arg y`, respectively). In other words, if `x` and `y` are complex numbers and neither of them is zero, then the argument (the angle in polar representation) of the product of `x` and `y` is equal to the sum of the arguments of `x` and `y`. This matches the property of angles in the multiplication of complex numbers in polar form.
More concisely: For complex numbers `x` and `y` with `x * y` non-zero, `Complex.arg (x * y) = Complex.arg x + Complex.arg y`.
|
Complex.arg_conj
theorem Complex.arg_conj : ∀ (x : ℂ), ((starRingEnd ℂ) x).arg = if x.arg = Real.pi then Real.pi else -x.arg
This theorem states that for any complex number `x`, the argument of the complex conjugate of `x` (denoted by `(starRingEnd ℂ) x`) is equal to the negation of the argument of `x`, except when the argument of `x` is equal to π (`Real.pi`). In that specific case, the argument of the complex conjugate of `x` is also π. Here, `Complex.arg` refers to the function that calculates the argument (phase) of a complex number, `starRingEnd` is a function that computes the complex conjugate of a given complex number, and `Real.pi` refers to the mathematical constant π.
More concisely: The argument of the complex conjugate of a complex number is the negation of its argument, except when the argument is π, in which case it is π again.
|
Complex.arg_mem_Ioc
theorem Complex.arg_mem_Ioc : ∀ (z : ℂ), z.arg ∈ Set.Ioc (-Real.pi) Real.pi
This theorem states that for every complex number `z`, the argument of `z` (denoted as `Complex.arg z`) belongs to the left-open right-closed interval from `-π` to `π`. In other words, the value of the argument function on any complex number lies between `-π` and `π`, with `-π` being excluded and `π` being included.
More concisely: The argument of every complex number lies in the interval (-π, pi].
|
Complex.arg_le_pi_div_two_iff
theorem Complex.arg_le_pi_div_two_iff : ∀ {z : ℂ}, z.arg ≤ Real.pi / 2 ↔ 0 ≤ z.re ∨ z.im < 0
The theorem `Complex.arg_le_pi_div_two_iff` states that for any complex number `z`, the argument of `z` (as defined by `Complex.arg`) is less than or equal to pi divided by 2 if and only if the real part of `z` is non-negative or the imaginary part of `z` is negative. In other words, it provides a characterization of the complex numbers whose argument is less than or equal to $\frac{\pi}{2}$ in terms of the signs of their real and imaginary parts.
More concisely: The complex argument is less than or equal to pi/2 if and only if the real part is non-negative or the imaginary part is negative.
|
Complex.arg_ofReal_of_nonneg
theorem Complex.arg_ofReal_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → (↑x).arg = 0
The theorem `Complex.arg_ofReal_of_nonneg` states that for every real number `x` that is equal to or greater than zero, the argument function (`arg`) of the complex number created from `x` (denoted as `↑x`) is equal to zero. The argument function of a complex number is a way to measure the angle that the complex number forms with the positive real axis when it is represented in the plane. In this specific case, the theorem says that any non-negative real number forms an angle of zero degrees with the positive real axis when it is seen as a complex number.
More concisely: For every non-negative real number x, the argument of the complex number ↑x is equal to 0.
|
Complex.neg_pi_lt_arg
theorem Complex.neg_pi_lt_arg : ∀ (x : ℂ), -Real.pi < x.arg
This theorem states that for every complex number `x`, the argument of `x` (denoted as `Complex.arg x` in Lean) is strictly greater than negative pi (`-Real.pi`). In other words, the angle made by the line connecting the origin and the point representing the complex number on the complex plane with the positive real axis, measured in radians, is always more than `-π` radians. The measurement of this angle is done in a counter-clockwise direction and revolves between `-π` and `π`.
More concisely: For every complex number `x`, the argument of `x` is strictly greater than `-π` radians.
|
Complex.arg_eq_pi_iff
theorem Complex.arg_eq_pi_iff : ∀ {z : ℂ}, z.arg = Real.pi ↔ z.re < 0 ∧ z.im = 0
This theorem, `Complex.arg_eq_pi_iff`, states that for any complex number `z`, the argument of `z` is equal to the mathematical constant `π` if and only if the real part of `z` is less than `0` and the imaginary part of `z` is exactly `0`. In other words, a complex number lies on the negative real axis (where the polar angle is `π`) if and only if its real component is negative and its imaginary component is zero.
More concisely: The complex number `z` has argument equal to `π` if and only if the real part of `z` is less than 0 and the imaginary part is 0.
|
Complex.arg_ofReal_of_neg
theorem Complex.arg_ofReal_of_neg : ∀ {x : ℝ}, x < 0 → (↑x).arg = Real.pi
This theorem provides a relationship between a negative real number and the argument of a complex number. Specifically, it states that for any real number `x` that is less than zero, the argument of the complex number formed by casting `x` to a complex number is equal to π (pi). In mathematical terms, if `x` is a real number with `x < 0`, then the argument of the complex number `x` equals π.
More concisely: For any real number `x` with `x < 0`, the argument of the complex number `x + i*0` equals `π`. (Here, `i` is the imaginary unit, `i*0` is the zero complex number.)
|
Complex.arg_le_pi
theorem Complex.arg_le_pi : ∀ (x : ℂ), x.arg ≤ Real.pi
The theorem `Complex.arg_le_pi` states that for every complex number `x`, the argument of `x`, given by the function `Complex.arg x`, is less than or equal to `Real.pi`, the mathematical constant π, approximately 3.14159265. The argument of a complex number is defined such that if the real part of `x` is non-negative, it is the arcsine of the imaginary part divided by the absolute value of `x`; otherwise, if the imaginary part is non-negative, it is the arcsine of the negative `x`'s imaginary part divided by the absolute value of `x` plus π, and if the imaginary part is negative, it is the arcsine of the negative `x`'s imaginary part divided by the absolute value of `x` minus π. The mathematical constant π is defined as twice the real number for which cosine equals zero in the interval [1,2].
More concisely: For all complex numbers x, the argument of x, as defined, is less than or equal to the mathematical constant π.
|
Complex.abs_mul_cos_arg
theorem Complex.abs_mul_cos_arg : ∀ (x : ℂ), Complex.abs x * x.arg.cos = x.re
The theorem `Complex.abs_mul_cos_arg` states that for any complex number `x`, the product of the absolute value of `x` and the cosine of the argument of `x` is equal to the real part of `x`. In mathematical terms, this means that for any complex number `x`, we have |x| * cos(arg(x)) = Re(x), where |x| denotes the absolute value of `x`, arg(x) refers to its argument, and Re(x) is its real part. This relationship is a key part of the polar representation of complex numbers.
More concisely: For any complex number x, |x| * cos(arg x) = Re(x).
|