# mathlib3documentation

analysis.complex.basic

# Normed space structure on ℂ. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file gathers basic facts on complex numbers of an analytic nature.

## Main results #

This file registers ℂ as a normed field, expresses basic properties of the norm, and gives tools on the real vector space structure of ℂ. Notably, in the namespace complex, it defines functions:

• re_clm
• im_clm
• of_real_clm
• conj_cle

They are bundled versions of the real part, the imaginary part, the embedding of ℝ in ℂ, and the complex conjugate as continuous ℝ-linear maps. The last two are also bundled as linear isometries in of_real_li and conj_lie.

We also register the fact that ℂ is an is_R_or_C field.

@[protected, instance]
noncomputable def complex.has_norm  :
Equations
@[simp]
theorem complex.norm_eq_abs (z : ) :
@[protected, instance]
Equations
@[protected, instance]
noncomputable def complex.normed_field  :
Equations
@[protected, instance]
noncomputable def complex.densely_normed_field  :
Equations
@[protected, instance]
def complex.normed_algebra {R : Type u_1} [normed_field R] [ ] :
Equations
@[protected, instance]
noncomputable def normed_space.complex_to_real {E : Type u_1} [ E] :

The module structure from module.complex_to_real is a normed space.

Equations
theorem complex.dist_eq (z w : ) :
theorem complex.dist_eq_re_im (z w : ) :
= ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
@[simp]
theorem complex.dist_mk (x₁ y₁ x₂ y₂ : ) :
has_dist.dist {re := x₁, im := y₁} {re := x₂, im := y₂} = ((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
theorem complex.dist_of_re_eq {z w : } (h : z.re = w.re) :
= w.im
theorem complex.nndist_of_re_eq {z w : } (h : z.re = w.re) :
=
theorem complex.edist_of_re_eq {z w : } (h : z.re = w.re) :
= w.im
theorem complex.dist_of_im_eq {z w : } (h : z.im = w.im) :
= w.re
theorem complex.nndist_of_im_eq {z w : } (h : z.im = w.im) :
=
theorem complex.edist_of_im_eq {z w : } (h : z.im = w.im) :
= w.re
theorem complex.dist_conj_self (z : ) :
theorem complex.nndist_conj_self (z : ) :
z = 2 *
theorem complex.dist_self_conj (z : ) :
( z) = 2 * |z.im|
theorem complex.nndist_self_conj (z : ) :
( z) = 2 *
@[simp]
@[simp]
theorem complex.norm_rat (r : ) :
@[simp]
theorem complex.norm_nat (n : ) :
@[simp]
theorem complex.norm_int {n : } :
theorem complex.norm_int_of_nonneg {n : } (hn : 0 n) :
@[continuity]
@[continuity]
@[simp, norm_cast]
@[simp, norm_cast]
theorem complex.nnnorm_nat (n : ) :
@[simp, norm_cast]
theorem complex.nnnorm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
theorem complex.norm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
ζ = 1
@[protected, instance]
noncomputable def complex.equiv_real_prod_clm  :

The natural continuous_linear_equiv from ℂ to ℝ × ℝ.

Equations
@[simp]
theorem complex.equiv_real_prod_clm_apply (ᾰ : ) :
= (ᾰ.re, ᾰ.im)
@[protected, instance]

The abs function on ℂ is proper.

The norm_sq function on ℂ is proper.

noncomputable def complex.re_clm  :

Continuous linear map version of the real part function, from ℂ to ℝ.

Equations
@[continuity]
@[simp]
@[simp]
theorem complex.re_clm_apply (z : ) :
noncomputable def complex.im_clm  :

Continuous linear map version of the real part function, from ℂ to ℝ.

Equations
@[continuity]
@[simp]
@[simp]
theorem complex.im_clm_apply (z : ) :
theorem complex.restrict_scalars_one_smul_right' {E : Type u_1} [ E] (x : E) :

The complex-conjugation function from ℂ to itself is an isometric linear equivalence.

Equations
@[simp]
theorem complex.conj_lie_apply (z : ) :
@[simp]
@[simp]
theorem complex.dist_conj_conj (z w : ) :
@[simp]
theorem complex.nndist_conj_conj (z w : ) :
( w) =
theorem complex.dist_conj_comm (z w : ) :
theorem complex.nndist_conj_comm (z w : ) :
w = ( w)
@[protected, instance]
@[continuity]

The only continuous ring homomorphisms from ℂ to ℂ are the identity and the complex conjugation.

noncomputable def complex.conj_cle  :

Continuous linear equiv version of the conj function, from ℂ to ℂ.

Equations
@[simp]
@[simp]
theorem complex.conj_cle_apply (z : ) :

Linear isometry version of the canonical embedding of ℝ in ℂ.

Equations
@[continuity]

The only continuous ring homomorphism from ℝ to ℂ is the identity.

noncomputable def complex.of_real_clm  :

Continuous linear map version of the canonical embedding of ℝ in ℂ.

Equations
@[simp]
@[simp]
theorem complex.of_real_clm_apply (x : ) :
@[protected, instance]
noncomputable def complex.is_R_or_C  :
Equations
theorem complex.eq_coe_norm_of_nonneg {z : } (hz : 0 z) :
@[simp]
theorem is_R_or_C.re_to_complex {x : } :
= x.re
@[simp]
theorem is_R_or_C.im_to_complex {x : } :
= x.im
@[simp]
@[simp]
@[simp]
theorem is_R_or_C.has_sum_conj {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} {x : 𝕜} :
has_sum (λ (x : α), (f x)) x ( x)
theorem is_R_or_C.has_sum_conj' {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} {x : 𝕜} :
has_sum (λ (x : α), (f x)) ( x) x
@[simp]
theorem is_R_or_C.summable_conj {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} :
summable (λ (x : α), (f x))
theorem is_R_or_C.conj_tsum {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] (f : α 𝕜) :
(∑' (a : α), f a) = ∑' (a : α), (f a)
@[simp, norm_cast]
theorem is_R_or_C.has_sum_of_real {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α } {x : } :
has_sum (λ (x : α), (f x)) x x
@[simp, norm_cast]
theorem is_R_or_C.summable_of_real {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α } :
summable (λ (x : α), (f x))
@[norm_cast]
theorem is_R_or_C.of_real_tsum {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] (f : α ) :
∑' (a : α), f a = ∑' (a : α), (f a)
theorem is_R_or_C.has_sum_re {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} {x : 𝕜} (h : x) :
has_sum (λ (x : α), is_R_or_C.re (f x))
theorem is_R_or_C.has_sum_im {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} {x : 𝕜} (h : x) :
has_sum (λ (x : α), is_R_or_C.im (f x))
theorem is_R_or_C.re_tsum {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} (h : summable f) :
is_R_or_C.re (∑' (a : α), f a) = ∑' (a : α), is_R_or_C.re (f a)
theorem is_R_or_C.im_tsum {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α 𝕜} (h : summable f) :
is_R_or_C.im (∑' (a : α), f a) = ∑' (a : α), is_R_or_C.im (f a)
theorem is_R_or_C.has_sum_iff {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] (f : α 𝕜) (c : 𝕜) :
c has_sum (λ (x : α), is_R_or_C.re (f x)) has_sum (λ (x : α), is_R_or_C.im (f x))

We have to repeat the lemmas about is_R_or_C.re and is_R_or_C.im as they are not syntactic matches for complex.re and complex.im.

We do not have this problem with of_real and conj, although we repeat them anyway for discoverability and to avoid the need to unify 𝕜.

@[simp]
theorem complex.has_sum_conj {α : Type u_1} {f : α } {x : } :
has_sum (λ (x : α), (f x)) x ( x)
theorem complex.has_sum_conj' {α : Type u_1} {f : α } {x : } :
has_sum (λ (x : α), (f x)) ( x) x
@[simp]
theorem complex.summable_conj {α : Type u_1} {f : α } :
summable (λ (x : α), (f x))
theorem complex.conj_tsum {α : Type u_1} (f : α ) :
(∑' (a : α), f a) = ∑' (a : α), (f a)
@[simp, norm_cast]
theorem complex.has_sum_of_real {α : Type u_1} {f : α } {x : } :
has_sum (λ (x : α), (f x)) x x
@[simp, norm_cast]
theorem complex.summable_of_real {α : Type u_1} {f : α } :
summable (λ (x : α), (f x))
@[norm_cast]
theorem complex.of_real_tsum {α : Type u_1} (f : α ) :
∑' (a : α), f a = ∑' (a : α), (f a)
theorem complex.has_sum_re {α : Type u_1} {f : α } {x : } (h : x) :
has_sum (λ (x : α), (f x).re) x.re
theorem complex.has_sum_im {α : Type u_1} {f : α } {x : } (h : x) :
has_sum (λ (x : α), (f x).im) x.im
theorem complex.re_tsum {α : Type u_1} {f : α } (h : summable f) :
(∑' (a : α), f a).re = ∑' (a : α), (f a).re
theorem complex.im_tsum {α : Type u_1} {f : α } (h : summable f) :
(∑' (a : α), f a).im = ∑' (a : α), (f a).im
theorem complex.has_sum_iff {α : Type u_1} (f : α ) (c : ) :
c has_sum (λ (x : α), (f x).re) c.re has_sum (λ (x : α), (f x).im) c.im