Complex.dist_of_re_eq
theorem Complex.dist_of_re_eq : ∀ {z w : ℂ}, z.re = w.re → dist z w = dist z.im w.im
This theorem states that for any two complex numbers `z` and `w`, if the real parts of `z` and `w` are equal, then the distance between `z` and `w` is equal to the distance between the imaginary part of `z` and the imaginary part of `w`. Here, `dist` denotes the distance function, `z.re` and `w.re` represent the real parts of `z` and `w` respectively, and `z.im` and `w.im` represent their imaginary parts.
More concisely: For complex numbers `z` and `w`, if `z.re = w.re` then `dist (z : ℂ) (w : ℂ) = dist z.im w.im`.
|
Complex.ringHom_eq_ofReal_of_continuous
theorem Complex.ringHom_eq_ofReal_of_continuous : ∀ {f : ℝ →+* ℂ}, Continuous ⇑f → f = Complex.ofReal
This theorem states that for any continuous ring homomorphism `f: ℝ → ℂ`, the only possible homomorphism is the identity function, which is represented by `Complex.ofReal`. In other words, the identity function, which maps every real number to the corresponding complex number (with a zero imaginary part), is the only continuous function from the real numbers to the complex numbers that also preserves the ring structure (i.e., addition and multiplication).
More concisely: The only continuous ring homomorphism from the real numbers to the complex numbers is the identity function.
|
Complex.tendsto_normSq_cocompact_atTop
theorem Complex.tendsto_normSq_cocompact_atTop : Filter.Tendsto (⇑Complex.normSq) (Filter.cocompact ℂ) Filter.atTop
The theorem `Complex.tendsto_normSq_cocompact_atTop` states that the square of the complex norm function, `normSq`, tends to infinity (`Filter.atTop`) when applied to the complements of compact sets (`Filter.cocompact`) in the complex numbers (`ℂ`). In other words, for any neighborhood of infinity in the real numbers, there exists a complement of a compact set in the complex numbers such that the squared norm of any complex number in this set is in the aforementioned neighborhood of infinity. This implies that the `normSq` function grows unbounded on the complements of compact sets in the complex plane.
More concisely: For any neighborhood of infinity in the real numbers, there exists a complement of a compact set in the complex numbers where the complex norm is unbounded.
|
Complex.ball_one_subset_slitPlane
theorem Complex.ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ Complex.slitPlane
This theorem states that the open unit ball of radius `1` centered at `1` in the complex plane is a subset of the slit plane. In mathematical terms, if we take all points in the complex plane that are less than distance `1` from the complex number `1`, all such points will either have a positive real part or a non-zero imaginary part, thus falling in the definition of the slit plane, which is the complex plane with the closed negative real axis excluded.
More concisely: The open unit ball centered at 1 in the complex plane is contained in the slit plane, where the slit plane is the complex plane with the closed negative real axis excluded. Points in the open unit ball have a positive real part or non-zero imaginary part.
|
Complex.ringHom_eq_id_or_conj_of_continuous
theorem Complex.ringHom_eq_id_or_conj_of_continuous :
∀ {f : ℂ →+* ℂ}, Continuous ⇑f → f = RingHom.id ℂ ∨ f = starRingEnd ℂ
This theorem states that for any continuous ring homomorphism `f` from the complex numbers `ℂ` to itself, `f` must either be the identity function or the complex conjugation function. In other words, the only continuous functions that preserve the ring structure of the complex numbers are the identity function and complex conjugation.
More concisely: Every continuous ring homomorphism from the complex numbers to themselves is either the identity function or complex conjugation.
|
Complex.restrictScalars_one_smulRight
theorem Complex.restrictScalars_one_smulRight :
∀ (x : ℂ), ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = x • 1
This theorem states that for every complex number `x`, when we restrict the scalars from complex to real numbers in the continuous linear map that multiplies `x` on the right by 1 (represented as `ContinuousLinearMap.smulRight 1 x`), the result is equivalent to `x` being scaled by 1 (`x • 1`). The `ContinuousLinearMap.restrictScalars ℝ` part ensures that the computation only involves real numbers.
More concisely: For every complex number x, the restriction of the continuous linear map that multiplies x on the right by 1 to real scalars is equivalent to scaling x by 1.
|
Complex.ofReal_tsum
theorem Complex.ofReal_tsum : ∀ {α : Type u_1} (f : α → ℝ), ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)
This theorem states that for any function `f` from a generic type `α` to the real numbers `ℝ`, the sum of the real part of the complex number representations of the function's outputs over all `α` is equal to the complex number representation of the sum of the function's outputs over all `α`. In other words, when we compute the sum (using tsum) of the real part of the complex numbers obtained from `f`, it's the same as first summing up the real numbers obtained from `f` and then converting to a complex number.
More concisely: For any function `f` from type `α` to `ℝ`, the complex number sum of the real parts of `f α` for all `α` equals the complex number representation of the real sum of `f α` for all `α`.
|
Complex.norm_real
theorem Complex.norm_real : ∀ (r : ℝ), ‖↑r‖ = ‖r‖
This theorem states that for all real numbers `r`, the norm of `r` when it is considered as a complex number (denoted by `↑r`) is equal to the norm of `r` as a real number. In other words, the magnitude of a real number remains the same whether it is considered in the real number space or the complex number space.
More concisely: For all real numbers r, the norm of the complex number ↑r equals the absolute value of r.
|
Complex.tendsto_abs_cocompact_atTop
theorem Complex.tendsto_abs_cocompact_atTop : Filter.Tendsto (⇑Complex.abs) (Filter.cocompact ℂ) Filter.atTop := by
sorry
This theorem states that the absolute value function on complex numbers (`ℂ`) is "proper". In this context, "proper" signifies that the function tends to infinity (`Filter.atTop`) when applied to a sequence of complex numbers that moves further and further away from all compact sets (`Filter.cocompact ℂ`). In other words, as the input complex numbers get larger and larger in magnitude (moving further away from any compact subset of the complex plane), the real-valued absolute values of these complex numbers also tend to infinity.
More concisely: The absolute value function on complex numbers is a proper function, meaning it approaches infinity on sequences of complex numbers that move arbitrarily far from any compact subset.
|
Complex.ofReal_mem_slitPlane
theorem Complex.ofReal_mem_slitPlane : ∀ {x : ℝ}, ↑x ∈ Complex.slitPlane ↔ 0 < x
This theorem states that for any real number `x`, `x` belongs to the slit complex plane (defined as the set of complex numbers whose real part is greater than zero or whose imaginary part is not equal to zero) if and only if `x` is greater than zero. Here, we're considering `x` as a complex number with zero imaginary part, denoted by `↑x` in Lean's notation.
More concisely: A real number `x` belongs to the slit complex plane if and only if `x` is a positive real number.
|
Complex.slitPlane_ne_zero
theorem Complex.slitPlane_ne_zero : ∀ {z : ℂ}, z ∈ Complex.slitPlane → z ≠ 0
This theorem states that for any complex number `z`, if `z` belongs to the slit plane (which is defined as the complex plane with the closed negative real axis removed, i.e., all complex numbers whose real part is greater than 0 or whose imaginary part is not equal to 0), then `z` cannot be equal to 0. In other words, the origin (0,0) is not included in the slit plane.
More concisely: The complex number `0` is not an element of the slit complex plane.
|
Complex.continuous_abs
theorem Complex.continuous_abs : Continuous ⇑Complex.abs
This theorem states that the absolute value function on complex numbers is continuous. In mathematical terms, this means for any complex number, small changes in the input to the absolute value function result in small changes in the output. In other words, if we have a sequence of complex numbers that converges to a certain value, the sequence of their absolute values will also converge to the absolute value of that value. This is an important property in complex analysis and topology that helps us understand the behavior of functions on complex numbers.
More concisely: The absolute value function on complex numbers is a continuous function.
|
Complex.mem_slitPlane_of_norm_lt_one
theorem Complex.mem_slitPlane_of_norm_lt_one : ∀ {z : ℂ}, ‖z‖ < 1 → 1 + z ∈ Complex.slitPlane
This theorem states that for any complex number `z`, if the norm (or magnitude) of `z` is less than one, then the complex number `1 + z` belongs to the slit plane. The slit plane, in this context, is defined as the set of all complex numbers that either have a positive real part or a non-zero imaginary part.
More concisely: If the norm of a complex number `z` is less than 1, then `1 + z` is in the slit complex plane.
|
Complex.continuous_re
theorem Complex.continuous_re : Continuous Complex.re
This theorem states that the real part of a complex number is a continuous function. In other words, for every sequence of complex numbers that converges to a certain complex number, the sequence of their real parts also converges to the real part of the limit. This is a basic property in the field of complex analysis.
More concisely: The real part function is continuous on the complex numbers.
|
Complex.norm_eq_abs
theorem Complex.norm_eq_abs : ∀ (z : ℂ), ‖z‖ = Complex.abs z
The theorem `Complex.norm_eq_abs` states that for any complex number `z`, the norm of `z` is equal to the absolute value of `z`. In mathematical terms, this theorem can be written as `‖z‖ = |z|` for all `z` in the set of complex numbers ℂ. This theorem establishes a direct relationship between the norm (a measure of the "length" or "size" of `z`) and the absolute value (which provides the magnitude of `z`) for complex numbers.
More concisely: The theorem `Complex.norm_eq_abs` asserts that the norm and absolute value of a complex number are equal.
|
Mathlib.Analysis.Complex.Basic._auxLemma.11
theorem Mathlib.Analysis.Complex.Basic._auxLemma.11 :
∀ {α : Type u_1} {f : α → ℝ} {x : ℝ}, HasSum (fun x => ↑(f x)) ↑x = HasSum f x
This theorem, `Mathlib.Analysis.Complex.Basic._auxLemma.11`, states that for any type `α`, any function `f` from `α` to the real numbers `ℝ`, and any real number `x`, the condition that the series sum of the complexified function values equals the complex number `x` is equivalent to the condition that the series sum of the function values equals the real number `x`. In other words, the sum of the complexified function `f` converges to the complexified limit if and only if the sum of the function `f` converges to the real limit.
More concisely: The complexification of a real-valued function `f : α → ℝ` converges to a complex number `x ∈ ℝ + iℝ` if and only if `f` converges to the real part of `x`.
|
Complex.continuous_ofReal
theorem Complex.continuous_ofReal : Continuous Complex.ofReal'
The theorem `Complex.continuous_ofReal` states that the function `Complex.ofReal'`, which maps real numbers to complex numbers, is continuous. In other words, the function that takes a real number and returns a complex number with that real number as the real part and zero as the imaginary part, is a continuous function with respect to the topology of real numbers and complex numbers.
More concisely: The real-valued function `Complex.ofReal'` mapping reals to complex numbers with real part equal to the input and imaginary part equal to zero is continuous.
|
Complex.continuous_im
theorem Complex.continuous_im : Continuous Complex.im
This theorem states that the imaginary part of a complex number is a continuous function. In other words, for every complex number, the function that extracts its imaginary part (denoted as `Complex.im` in Lean 4) doesn't have any jumps or disruptions and changes in a way that you can draw it without lifting your pen from the paper. This is expressed in Lean 4 as `Continuous Complex.im`.
More concisely: The imaginary part function of complex numbers is a continuous function.
|
Complex.dist_eq_re_im
theorem Complex.dist_eq_re_im : ∀ (z w : ℂ), dist z w = ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2).sqrt
This theorem states that for any two complex numbers `z` and `w`, the distance between them is equal to the square root of the sum of the squares of their real and imaginary part differences. In other words, if you represent the complex numbers `z` and `w` in the complex plane, the geometric distance between them is calculated using Pythagoras' theorem: the square root of ((real part of z - real part of w) squared + (imaginary part of z - imaginary part of w) squared). This is the complex number version of the Euclidean distance formula.
More concisely: The theorem asserts that the magnitude of the complex difference between two complex numbers z and w is equal to the square root of the sum of the squares of the real and imaginary part differences: |z - w| = sqrt((Re(z) - Re(w))^2 + (Im(z) - Im(w))^2).
|
Complex.mem_slitPlane_iff
theorem Complex.mem_slitPlane_iff : ∀ {z : ℂ}, z ∈ Complex.slitPlane ↔ 0 < z.re ∨ z.im ≠ 0
This theorem states that a complex number `z` belongs to the slit plane if and only if its real part is positive or its imaginary part is not equal to zero. In other words, the slit plane consists of all complex numbers whose real component is greater than zero or whose imaginary component is different from zero.
More concisely: A complex number `z` lies in the slit complex plane if and only if its real part is positive or its imaginary part is non-zero.
|
Complex.restrictScalars_one_smulRight'
theorem Complex.restrictScalars_one_smulRight' :
∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (x : E),
ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) =
Complex.reCLM.smulRight x + Complex.I • Complex.imCLM.smulRight x
This theorem states that for any element `x` of a certain type `E` (where `E` is a seminormed additive commutative group and a complex normed space), the restriction of scalars from the complex numbers to the real numbers on the continuous linear map defined by right-multiplication by `x` is equal to the sum of two terms: the continuous linear map defined by right-multiplication by the real part of `x`, and the imaginary unit times the continuous linear map defined by right-multiplication by the imaginary part of `x`. In other words, this theorem encapsulates how a complex linear transformation relates to its real and imaginary parts when viewed as real linear transformations.
More concisely: For any complex number `x` and seminormed additive commutative group `E` being a complex normed space, the restriction of scalars from complex numbers to real numbers on the right-multiplication-by-`x` linear map equals the sum of right-multiplication-by-the-real-part-of-`x` and the imaginary unit times right-multiplication-by-the-imaginary-part-of-`x` linear maps.
|