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:

re_clm
im_clm
of_real_clm
conj_clm

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_li.

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

@[instance]

def complex.has_norm :

Equations

complex.has_norm = {norm := complex.abs}

@[instance]

def complex.normed_group :

normed_group ℂ

Equations

complex.normed_group = normed_group.of_core ℂ complex.normed_group._proof_1

@[instance]

def complex.normed_field :

normed_field ℂ

Equations

complex.normed_field = {to_has_norm := {norm := complex.abs}, to_field := {add := field.add complex.field, add_assoc := _, zero := field.zero complex.field, zero_add := _, add_zero := _, nsmul := field.nsmul complex.field, nsmul_zero' := _, nsmul_succ' := _, neg := field.neg complex.field, sub := field.sub complex.field, sub_eq_add_neg := _, gsmul := field.gsmul complex.field, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := field.mul complex.field, mul_assoc := _, one := field.one complex.field, one_mul := _, mul_one := _, npow := field.npow complex.field, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv complex.field, div := field.div complex.field, div_eq_mul_inv := _, gpow := field.gpow complex.field, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}, to_metric_space := normed_group.to_metric_space complex.normed_group, dist_eq := complex.normed_field._proof_1, norm_mul' := complex.abs_mul}

@[instance]

def complex.nondiscrete_normed_field :

nondiscrete_normed_field ℂ

Equations

complex.nondiscrete_normed_field = {to_normed_field := complex.normed_field, non_trivial := complex.nondiscrete_normed_field._proof_1}

@[instance]

def complex.normed_algebra {R : Type u_1} [normed_field R] [normed_algebra R ℝ] :

normed_algebra R ℂ

Equations

complex.normed_algebra = {to_algebra := complex.algebra normed_algebra.to_algebra, norm_algebra_map_eq := _}

@[simp]

theorem complex.norm_eq_abs (z : ℂ) :

∥z∥ = complex.abs z

theorem complex.dist_eq (z w : ℂ) :

dist z w = complex.abs (z - w)

@[simp]

theorem complex.norm_real (r : ℝ) :

∥↑r∥ = ∥r∥

@[simp]

theorem complex.norm_rat (r : ℚ) :

∥↑r∥ = abs ↑r

@[simp]

theorem complex.norm_nat (n : ℕ) :

∥↑n∥ = ↑n

@[simp]

theorem complex.norm_int {n : ℤ} :

∥↑n∥ = abs ↑n

theorem complex.norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) :

∥↑n∥ = ↑n

def complex.re_clm :

ℂ →L[ℝ ] ℝ

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

Equations

complex.re_clm = complex.re_lm.mk_continuous 1 complex.re_clm._proof_1

theorem complex.continuous_re :

continuous complex.re

@[simp]

theorem complex.re_clm_coe :

↑complex.re_clm = complex.re_lm

@[simp]

theorem complex.re_clm_apply (z : ℂ) :

⇑complex.re_clm z = z.re

@[simp]

theorem complex.re_clm_norm :

∥complex.re_clm ∥ = 1

def complex.im_clm :

ℂ →L[ℝ ] ℝ

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

Equations

complex.im_clm = complex.im_lm.mk_continuous 1 complex.im_clm._proof_1

theorem complex.continuous_im :

continuous complex.im

@[simp]

theorem complex.im_clm_coe :

↑complex.im_clm = complex.im_lm

@[simp]

theorem complex.im_clm_apply (z : ℂ) :

⇑complex.im_clm z = z.im

@[simp]

theorem complex.im_clm_norm :

∥complex.im_clm ∥ = 1

def complex.conj_li :

ℂ →ₗᵢ[ℝ ] ℂ

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

Equations

complex.conj_li = {to_linear_map := complex.conj_lm, norm_map' := complex.conj_li._proof_1}

@[simp]

theorem complex.conj_li_apply (z : ℂ) :

⇑complex.conj_li z = ⇑complex.conj_lm z

def complex.conj_clm :

ℂ →L[ℝ ] ℂ

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

Equations

complex.conj_clm = complex.conj_li.to_continuous_linear_map

theorem complex.isometry_conj :

isometry ⇑complex.conj

theorem complex.continuous_conj :

continuous ⇑complex.conj

@[simp]

theorem complex.conj_clm_coe :

↑complex.conj_clm = complex.conj_lm

@[simp]

theorem complex.conj_clm_apply (z : ℂ) :

⇑complex.conj_clm z = ⇑complex.conj z

@[simp]

theorem complex.conj_clm_norm :

∥complex.conj_clm ∥ = 1

def complex.of_real_li :

ℝ →ₗᵢ[ℝ ] ℂ

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

Equations

complex.of_real_li = {to_linear_map := complex.of_real_lm, norm_map' := complex.of_real_li._proof_1}

def complex.of_real_clm :

ℝ →L[ℝ ] ℂ

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

Equations

complex.of_real_clm = complex.of_real_li.to_continuous_linear_map

theorem complex.isometry_of_real :

theorem complex.continuous_of_real :

@[simp]

theorem complex.of_real_clm_coe :

↑complex.of_real_clm = complex.of_real_lm

@[simp]

theorem complex.of_real_clm_apply (x : ℝ) :

⇑complex.of_real_clm x = ↑x

@[simp]

theorem complex.of_real_clm_norm :

∥complex.of_real_clm ∥ = 1

@[instance]

def complex.is_R_or_C :

Equations

complex.is_R_or_C = {to_nondiscrete_normed_field := complex.nondiscrete_normed_field, to_normed_algebra := complex.normed_algebra (normed_algebra.id ℝ), to_complete_space := complex.is_R_or_C._proof_1, re := {to_fun := complex.re, map_zero' := complex.zero_re, map_add' := complex.add_re}, im := {to_fun := complex.im, map_zero' := complex.zero_im, map_add' := complex.add_im}, conj := complex.conj, I := complex.I, I_re_ax := complex.is_R_or_C._proof_2, I_mul_I_ax := complex.is_R_or_C._proof_3, re_add_im_ax := complex.is_R_or_C._proof_4, of_real_re_ax := complex.is_R_or_C._proof_5, of_real_im_ax := complex.is_R_or_C._proof_6, mul_re_ax := complex.is_R_or_C._proof_7, mul_im_ax := complex.is_R_or_C._proof_8, conj_re_ax := complex.is_R_or_C._proof_9, conj_im_ax := complex.is_R_or_C._proof_10, conj_I_ax := complex.is_R_or_C._proof_11, norm_sq_eq_def_ax := complex.is_R_or_C._proof_12, mul_im_I_ax := complex.is_R_or_C._proof_13, inv_def_ax := complex.is_R_or_C._proof_14, div_I_ax := complex.div_I}

@[simp]

theorem is_R_or_C.re_to_complex {x : ℂ} :

⇑is_R_or_C.re x = x.re

@[simp]

theorem is_R_or_C.im_to_complex {x : ℂ} :

⇑is_R_or_C.im x = x.im

@[simp]

theorem is_R_or_C.conj_to_complex {x : ℂ} :

⇑is_R_or_C.conj x = ⇑complex.conj x

@[simp]

theorem is_R_or_C.I_to_complex :

is_R_or_C.I = complex.I

@[simp]

theorem is_R_or_C.norm_sq_to_complex {x : ℂ} :

⇑is_R_or_C.norm_sq x = ⇑complex.norm_sq x

@[simp]

theorem is_R_or_C.abs_to_complex {x : ℂ} :

is_R_or_C.abs x = complex.abs x