Mathlib.Analysis.Complex.Circle._auxLemma.1
theorem Mathlib.Analysis.Complex.Circle._auxLemma.1 : ∀ {z : ℂ}, (z ∈ circle) = (Complex.abs z = 1)
This theorem states that for every complex number `z`, `z` belongs to the unit circle (in the complex numbers) if and only if the absolute value of `z` is equal to 1. This is essentially stating that the unit circle in the complex plane is the set of all complex numbers with an absolute value of 1.
More concisely: A complex number `z` lies on the unit circle if and only if |z| = 1. (The unit circle in the complex plane is the set of all complex numbers with absolute value equal to 1.)
|
abs_coe_circle
theorem abs_coe_circle : ∀ (z : ↥circle), Complex.abs ↑z = 1
This theorem states that for any complex number `z` that is a member of the unit circle in the complex plane (also known as `circle`), the absolute value of `z` is equal to 1. In other words, the absolute value of any point on the unit circle in the complex plane is always 1. In mathematical terms, if `z` is a complex number such that it belongs to the unit circle, i.e., |z| = 1, then the theorem `abs_coe_circle` asserts this fact.
More concisely: The theorem asserts that the absolute value of any complex number in the unit circle is equal to 1.
|
expMapCircle_zero
theorem expMapCircle_zero : expMapCircle 0 = 1
This theorem states that when the function `expMapCircle`, which maps real numbers to the unit circle in the complex plane by exponentiating the product of the real number and the imaginary unit, is applied to the number zero, it returns one. In mathematical terms, this is essentially stating that $e^{0i} = 1$ in the context of complex numbers, which aligns with the well-known principle that any number raised to the power of zero is one.
More concisely: The theorem asserts that expMapCircle 0 = 1 in the complex plane.
|
expMapCircle_add
theorem expMapCircle_add : ∀ (x y : ℝ), expMapCircle (x + y) = expMapCircle x * expMapCircle y
This theorem states that for all real numbers `x` and `y`, the value of the function `expMapCircle` at the point `x + y` is equal to the product of `expMapCircle` evaluated at `x` and `expMapCircle` evaluated at `y`. In other words, the function `expMapCircle`, which maps real numbers to the unit circle in the complex plane using the exponential function, satisfies the property that the image of the sum of two real numbers is the product of their individual images. This property parallels the familiar one from trigonometry that the sum of two angles corresponds to the product of their complex exponentials.
More concisely: For all real numbers x and y, expMapCircle (x + y) = expMapCircle x * expMapCircle y.
|
mem_circle_iff_abs
theorem mem_circle_iff_abs : ∀ {z : ℂ}, z ∈ circle ↔ Complex.abs z = 1
The theorem `mem_circle_iff_abs` states that for every complex number `z`, `z` is a member of the unit circle in the complex plane if and only if the absolute value (or modulus) of `z` is equal to 1. This is essentially a formal statement in Lean 4 that reflects the geometric interpretation that points on the unit circle in the complex plane are precisely those complex numbers with an absolute value (or modulus) of 1.
More concisely: A complex number `z` lies on the unit circle if and only if the absolute value of `z` equals 1.
|
expMapCircle_apply
theorem expMapCircle_apply : ∀ (t : ℝ), ↑(expMapCircle t) = (↑t * Complex.I).exp
The theorem `expMapCircle_apply` states that for any real number `t`, the application of the function `expMapCircle` to `t` is equivalent to the complex exponential of `t` multiplied by the imaginary unit. In mathematical terms, it's stating that for all `t` in real numbers, the complex exponential of `t * i` (where `i` is the imaginary unit) maps to a point on the unit circle in the complex plane, as described by the function `expMapCircle`.
More concisely: For all real numbers `t`, `expMapCircle t = (exp (i * t))`.
|