mathlib documentation

analysis.complex.basic

Normed space structure on ℂ. #

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:

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.

source
@[protected, instance]
noncomputable def complex.has_norm  :
has_norm ℂ
Equations
source
@[simp]
theorem complex.norm_eq_abs (z : ℂ) :
‖z‖ = ⇑complex.abs z
source
@[protected, instance]
noncomputable def complex.normed_add_comm_group  :
normed_add_comm_group ℂ
Equations
source
@[protected, instance]
noncomputable def complex.normed_field  :
normed_field ℂ
Equations
source
@[protected, instance]
noncomputable def complex.densely_normed_field  :
densely_normed_field ℂ
Equations
source
@[protected, instance]
def complex.normed_algebra {R : Type u_1} [normed_field R] [normed_algebra R ℝ] :
normed_algebra R ℂ
Equations
source
@[protected, instance]
noncomputable def normed_space.complex_to_real {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] :
normed_space ℝ E

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

Equations
source
theorem complex.dist_eq (z w : ℂ) :
has_dist.dist z w = ⇑complex.abs (z - w)
source
theorem complex.dist_eq_re_im (z w : ℂ) :
has_dist.dist z w = real.sqrt ((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
source
@[simp]
theorem complex.dist_mk (x₁ y₁ x₂ y₂ : ℝ) :
has_dist.dist {re := x₁, im := y₁} {re := x₂, im := y₂} = real.sqrt ((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
source
theorem complex.dist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
has_dist.dist z w = has_dist.dist z.im w.im
source
theorem complex.nndist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
has_nndist.nndist z w = has_nndist.nndist z.im w.im
source
theorem complex.edist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
has_edist.edist z w = has_edist.edist z.im w.im
source
theorem complex.dist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
has_dist.dist z w = has_dist.dist z.re w.re
source
theorem complex.nndist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
has_nndist.nndist z w = has_nndist.nndist z.re w.re
source
theorem complex.edist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
has_edist.edist z w = has_edist.edist z.re w.re
source
theorem complex.dist_conj_self (z : ℂ) :
has_dist.dist (⇑(star_ring_end ℂ) z) z = 2 * |z.im|
source
theorem complex.nndist_conj_self (z : ℂ) :
has_nndist.nndist (⇑(star_ring_end ℂ) z) z = 2 * ⇑real.nnabs z.im
source
theorem complex.dist_self_conj (z : ℂ) :
has_dist.dist z (⇑(star_ring_end ℂ) z) = 2 * |z.im|
source
theorem complex.nndist_self_conj (z : ℂ) :
has_nndist.nndist z (⇑(star_ring_end ℂ) z) = 2 * ⇑real.nnabs z.im
source
@[simp]
theorem complex.comap_abs_nhds_zero  :
filter.comap ⇑complex.abs (nhds 0) = nhds 0
source
theorem complex.norm_real (r : ℝ) :
‖↑r‖ = ‖r‖
source
@[simp]
theorem complex.norm_rat (r : ℚ) :
‖↑r‖ = |↑r|
source
@[simp]
theorem complex.norm_nat (n : ℕ) :
‖↑n‖ = ↑n
source
@[simp]
theorem complex.norm_int {n : ℤ} :
‖↑n‖ = |↑n|
source
theorem complex.norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) :
‖↑n‖ = ↑n
source
@[continuity]
theorem complex.continuous_abs  :
continuous ⇑complex.abs
source
@[continuity]
theorem complex.continuous_norm_sq  :
continuous ⇑complex.norm_sq
source
@[simp, norm_cast]
theorem complex.nnnorm_real (r : ℝ) :
‖↑r‖₊ = ‖r‖₊
source
@[simp, norm_cast]
theorem complex.nnnorm_nat (n : ℕ) :
‖↑n‖₊ = ↑n
source
@[simp, norm_cast]
theorem complex.nnnorm_int (n : ℤ) :
‖↑n‖₊ = ‖n‖₊
source
theorem complex.nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :
‖ζ‖₊ = 1
source
theorem complex.norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :
‖ζ‖ = 1
source
theorem complex.tendsto_abs_cocompact_at_top  :
filter.tendsto ⇑complex.abs (filter.cocompact ℂ) filter.at_top

The abs function on ℂ is proper.

source
theorem complex.tendsto_norm_sq_cocompact_at_top  :
filter.tendsto ⇑complex.norm_sq (filter.cocompact ℂ) filter.at_top

The norm_sq function on ℂ is proper.

source
noncomputable def complex.re_clm  :
ℂ →L[ℝ] ℝ

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

Equations
source
@[continuity]
theorem complex.continuous_re  :
continuous complex.re
source
@[simp]
theorem complex.re_clm_coe  :
↑complex.re_clm = complex.re_lm
source
@[simp]
theorem complex.re_clm_apply (z : ℂ) :
⇑complex.re_clm z = z.re
source
@[simp]
theorem complex.re_clm_norm  :
‖complex.re_clm‖ = 1
source
@[simp]
theorem complex.re_clm_nnnorm  :
‖complex.re_clm‖₊ = 1
source
noncomputable def complex.im_clm  :
ℂ →L[ℝ] ℝ

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

Equations
source
@[continuity]
theorem complex.continuous_im  :
continuous complex.im
source
@[simp]
theorem complex.im_clm_coe  :
↑complex.im_clm = complex.im_lm
source
@[simp]
theorem complex.im_clm_apply (z : ℂ) :
⇑complex.im_clm z = z.im
source
@[simp]
theorem complex.im_clm_norm  :
‖complex.im_clm‖ = 1
source
@[simp]
theorem complex.im_clm_nnnorm  :
‖complex.im_clm‖₊ = 1
source
theorem complex.restrict_scalars_one_smul_right' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] (x : E) :
continuous_linear_map.restrict_scalars ℝ (1.smul_right x) = complex.re_clm.smul_right x + complex.I • complex.im_clm.smul_right x
source
theorem complex.restrict_scalars_one_smul_right (x : ℂ) :
continuous_linear_map.restrict_scalars ℝ (1.smul_right x) = x • 1
source
def complex.conj_lie  :
ℂ ≃ₗᵢ[ℝ] ℂ

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

Equations
source
@[simp]
theorem complex.conj_lie_apply (z : ℂ) :
⇑complex.conj_lie z = ⇑(star_ring_end ℂ) z
source
@[simp]
theorem complex.conj_lie_symm  :
complex.conj_lie.symm = complex.conj_lie
source
theorem complex.isometry_conj  :
isometry ⇑(star_ring_end ℂ)
source
@[simp]
theorem complex.dist_conj_conj (z w : ℂ) :
has_dist.dist (⇑(star_ring_end ℂ) z) (⇑(star_ring_end ℂ) w) = has_dist.dist z w
source
@[simp]
theorem complex.nndist_conj_conj (z w : ℂ) :
has_nndist.nndist (⇑(star_ring_end ℂ) z) (⇑(star_ring_end ℂ) w) = has_nndist.nndist z w
source
theorem complex.dist_conj_comm (z w : ℂ) :
has_dist.dist (⇑(star_ring_end ℂ) z) w = has_dist.dist z (⇑(star_ring_end ℂ) w)
source
theorem complex.nndist_conj_comm (z w : ℂ) :
has_nndist.nndist (⇑(star_ring_end ℂ) z) w = has_nndist.nndist z (⇑(star_ring_end ℂ) w)
source
@[simp]
theorem complex.det_conj_lie  :
⇑linear_map.det ↑(complex.conj_lie.to_linear_equiv) = -1

The determinant of conj_lie, as a linear map.

source
@[simp]
theorem complex.linear_equiv_det_conj_lie  :
⇑linear_equiv.det complex.conj_lie.to_linear_equiv = -1

The determinant of conj_lie, as a linear equiv.

source
@[protected, instance]
def complex.has_continuous_star  :
has_continuous_star ℂ
source
@[continuity]
theorem complex.continuous_conj  :
continuous ⇑(star_ring_end ℂ)
source
theorem complex.ring_hom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : continuous ⇑f) :
f = ring_hom.id ℂ ∨ f = star_ring_end ℂ

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

source
noncomputable def complex.conj_cle  :
ℂ ≃L[ℝ] ℂ

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

Equations
source
@[simp]
theorem complex.conj_cle_coe  :
complex.conj_cle.to_linear_equiv = complex.conj_ae.to_linear_equiv
source
@[simp]
theorem complex.conj_cle_apply (z : ℂ) :
⇑complex.conj_cle z = ⇑(star_ring_end ℂ) z
source
@[simp]
theorem complex.conj_cle_norm  :
‖↑complex.conj_cle‖ = 1
source
@[simp]
theorem complex.conj_cle_nnorm  :
‖↑complex.conj_cle‖₊ = 1
source
def complex.of_real_li  :
ℝ →ₗᵢ[ℝ] ℂ

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

Equations
source
theorem complex.isometry_of_real  :
isometry coe
source
@[continuity]
theorem complex.continuous_of_real  :
continuous coe
source
theorem complex.ring_hom_eq_of_real_of_continuous {f : ℝ →+* ℂ} (h : continuous ⇑f) :
f = complex.of_real

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

source
noncomputable def complex.of_real_clm  :
ℝ →L[ℝ] ℂ

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

Equations
source
@[simp]
theorem complex.of_real_clm_coe  :
↑complex.of_real_clm = complex.of_real_am.to_linear_map
source
@[simp]
theorem complex.of_real_clm_apply (x : ℝ) :
⇑complex.of_real_clm x = ↑x
source
@[simp]
theorem complex.of_real_clm_norm  :
‖complex.of_real_clm‖ = 1
source
@[simp]
theorem complex.of_real_clm_nnnorm  :
‖complex.of_real_clm‖₊ = 1
source
@[protected, instance]
noncomputable def complex.is_R_or_C  :
is_R_or_C ℂ
Equations
source
theorem is_R_or_C.re_eq_complex_re  :
⇑is_R_or_C.re = complex.re
source
theorem is_R_or_C.im_eq_complex_im  :
⇑is_R_or_C.im = complex.im
source
theorem complex.eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) :
z = ↑‖z‖
source
def complex.equiv_real_prod_add_hom  :
ℂ ≃+ ℝ × ℝ

The natural add_equiv from ℂ to ℝ × ℝ.

Equations
source
@[simp]
theorem complex.equiv_real_prod_add_hom_symm_apply_im (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prod_add_hom.symm) ᾰ).im = ᾰ.snd
source
@[simp]
theorem complex.equiv_real_prod_add_hom_symm_apply_re (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prod_add_hom.symm) ᾰ).re = ᾰ.fst
source
@[simp]
theorem complex.equiv_real_prod_add_hom_apply (ᾰ : ℂ) :
⇑complex.equiv_real_prod_add_hom ᾰ = (ᾰ.re, ᾰ.im)
source
def complex.equiv_real_prod_add_hom_lm  :
ℂ ≃ₗ[ℝ] ℝ × ℝ

The natural linear_equiv from ℂ to ℝ × ℝ.

Equations
source
@[simp]
theorem complex.equiv_real_prod_add_hom_lm_apply (ᾰ : ℂ) :
⇑complex.equiv_real_prod_add_hom_lm ᾰ = (ᾰ.re, ᾰ.im)
source
@[simp]
theorem complex.equiv_real_prod_add_hom_lm_symm_apply_im (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prod_add_hom_lm.symm) ᾰ).im = ᾰ.snd
source
@[simp]
theorem complex.equiv_real_prod_add_hom_lm_symm_apply_re (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prod_add_hom_lm.symm) ᾰ).re = ᾰ.fst
source
noncomputable def complex.equiv_real_prodₗ  :
ℂ ≃L[ℝ] ℝ × ℝ

The natural continuous_linear_equiv from ℂ to ℝ × ℝ.

Equations
source
@[simp]
theorem complex.equiv_real_prodₗ_symm_apply_im (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prodₗ.symm) ᾰ).im = ᾰ.snd
source
@[simp]
theorem complex.equiv_real_prodₗ_symm_apply_re (ᾰ : ℝ × ℝ) :
(⇑(complex.equiv_real_prodₗ.symm) ᾰ).re = ᾰ.fst
source
@[simp]
theorem complex.equiv_real_prodₗ_apply (ᾰ : ℂ) :
⇑complex.equiv_real_prodₗ ᾰ = (ᾰ.re, ᾰ.im)
source
theorem complex.has_sum_iff {α : Type u_1} (f : α → ℂ) (c : ℂ) :
has_sum f c ↔ has_sum (λ (x : α), (f x).re) c.re ∧ has_sum (λ (x : α), (f x).im) c.im
source
@[simp]
theorem is_R_or_C.re_to_complex {x : ℂ} :
⇑is_R_or_C.re x = x.re
source
@[simp]
theorem is_R_or_C.im_to_complex {x : ℂ} :
⇑is_R_or_C.im x = x.im
source
@[simp]
theorem is_R_or_C.I_to_complex  :
is_R_or_C.I = complex.I
source
@[simp]
theorem is_R_or_C.norm_sq_to_complex {x : ℂ} :
⇑is_R_or_C.norm_sq x = ⇑complex.norm_sq x
source
@[simp]
theorem is_R_or_C.abs_to_complex {x : ℂ} :
is_R_or_C.abs x = ⇑complex.abs x