mathlib3 documentation

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

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

@[simp]

theorem complex.norm_eq_abs (z : ℂ) :

‖z‖ = ⇑complex.abs z

theorem complex.norm_exp_of_real_mul_I (t : ℝ) :

‖cexp (↑t * complex.I)‖ = 1

@[protected, instance]

noncomputable def complex.normed_add_comm_group :

normed_add_comm_group ℂ

Equations

complex.normed_add_comm_group = {to_fun := complex.abs.to_mul_hom.to_fun, map_zero' := complex.normed_add_comm_group._proof_1, add_le' := complex.normed_add_comm_group._proof_2, neg' := complex.normed_add_comm_group._proof_3, eq_zero_of_map_eq_zero' := complex.normed_add_comm_group._proof_4}.to_normed_add_comm_group

@[protected, instance]

noncomputable 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 := _, zsmul := field.zsmul complex.field, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := field.int_cast complex.field, nat_cast := field.nat_cast complex.field, one := field.one complex.field, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := field.mul complex.field, mul_assoc := _, 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 := _, zpow := field.zpow complex.field, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := field.rat_cast complex.field, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul complex.field, qsmul_eq_mul' := _}, to_metric_space := normed_add_comm_group.to_metric_space complex.normed_add_comm_group, dist_eq := complex.normed_field._proof_1, norm_mul' := complex.normed_field._proof_2}

@[protected, instance]

noncomputable def complex.densely_normed_field :

densely_normed_field ℂ

Equations

complex.densely_normed_field = {to_normed_field := complex.normed_field, lt_norm_lt := complex.densely_normed_field._proof_1}

@[protected, 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_smul_le := _}

@[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

normed_space.complex_to_real = normed_space.restrict_scalars ℝ ℂ E

theorem complex.dist_eq (z w : ℂ) :

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

theorem complex.dist_eq_re_im (z w : ℂ) :

has_dist.dist 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) :

has_dist.dist z w = has_dist.dist z.im w.im

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

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

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

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

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

theorem complex.dist_conj_self (z : ℂ) :

has_dist.dist (⇑(star_ring_end ℂ) z) z = 2 * |z.im |

theorem complex.nndist_conj_self (z : ℂ) :

has_nndist.nndist (⇑(star_ring_end ℂ) z) z = 2 * ⇑real.nnabs z.im

theorem complex.dist_self_conj (z : ℂ) :

has_dist.dist z (⇑(star_ring_end ℂ) z) = 2 * |z.im |

theorem complex.nndist_self_conj (z : ℂ) :

has_nndist.nndist z (⇑(star_ring_end ℂ) z) = 2 * ⇑real.nnabs z.im

@[simp]

theorem complex.comap_abs_nhds_zero :

filter.comap ⇑complex.abs (nhds 0) = nhds 0

theorem complex.norm_real (r : ℝ) :

‖↑r‖ = ‖r‖

@[simp]

theorem complex.norm_rat (r : ℚ) :

‖↑r‖ = |↑r|

@[simp]

theorem complex.norm_nat (n : ℕ) :

‖↑n‖ = ↑n

@[simp]

theorem complex.norm_int {n : ℤ} :

‖↑n‖ = |↑n|

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

‖↑n‖ = ↑n

@[continuity]

theorem complex.continuous_abs :

continuous ⇑complex.abs

@[continuity]

theorem complex.continuous_norm_sq :

continuous ⇑complex.norm_sq

@[simp, norm_cast]

theorem complex.nnnorm_real (r : ℝ) :

‖↑r‖₊ = ‖r‖₊

@[simp, norm_cast]

theorem complex.nnnorm_nat (n : ℕ) :

‖↑n‖₊ = ↑n

@[simp, norm_cast]

theorem complex.nnnorm_int (n : ℤ) :

‖↑n‖₊ = ‖n‖₊

theorem complex.nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :

‖ζ‖₊ = 1

theorem complex.norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :

theorem complex.equiv_real_prod_apply_le (z : ℂ) :

‖⇑complex.equiv_real_prod z‖ ≤ ⇑complex.abs z

theorem complex.equiv_real_prod_apply_le' (z : ℂ) :

‖⇑complex.equiv_real_prod z‖ ≤ 1 * ⇑complex.abs z

theorem complex.lipschitz_equiv_real_prod :

lipschitz_with 1 ⇑complex.equiv_real_prod

theorem complex.antilipschitz_equiv_real_prod :

antilipschitz_with (⇑nnreal.sqrt 2) ⇑complex.equiv_real_prod

theorem complex.uniform_embedding_equiv_real_prod :

uniform_embedding ⇑complex.equiv_real_prod

@[protected, instance]

def complex.complete_space :

complete_space ℂ

@[simp]

theorem complex.equiv_real_prod_clm_symm_apply_re (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_clm.symm) ᾰ).re = ᾰ.fst

noncomputable def complex.equiv_real_prod_clm :

ℂ ≃L[ℝ ] ℝ × ℝ

The natural continuous_linear_equiv from ℂ to ℝ × ℝ.

Equations

complex.equiv_real_prod_clm = complex.equiv_real_prod_lm.to_continuous_linear_equiv_of_bounds 1 (√ 2) complex.equiv_real_prod_apply_le' complex.equiv_real_prod_clm._proof_1

@[simp]

theorem complex.equiv_real_prod_clm_symm_apply_im (ᾰ : ℝ × ℝ) :

(⇑(complex.equiv_real_prod_clm.symm) ᾰ).im = ᾰ.snd

@[simp]

theorem complex.equiv_real_prod_clm_apply (ᾰ : ℂ) :

⇑complex.equiv_real_prod_clm ᾰ = (ᾰ.re, ᾰ.im)

@[protected, instance]

def complex.proper_space :

proper_space ℂ

theorem complex.tendsto_abs_cocompact_at_top :

filter.tendsto ⇑complex.abs (filter.cocompact ℂ) filter.at_top

The abs function on ℂ is proper.

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.

noncomputable 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

@[continuity]

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

noncomputable 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

@[continuity]

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

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

theorem complex.restrict_scalars_one_smul_right (x : ℂ) :

continuous_linear_map.restrict_scalars ℝ (1.smul_right x) = x • 1

def complex.conj_lie :

ℂ ≃ₗᵢ[ℝ ] ℂ

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

Equations

complex.conj_lie = {to_linear_equiv := complex.conj_ae.to_linear_equiv, norm_map' := complex.abs_conj}

@[simp]

theorem complex.conj_lie_apply (z : ℂ) :

⇑complex.conj_lie z = ⇑(star_ring_end ℂ) z

@[simp]

theorem complex.conj_lie_symm :

complex.conj_lie.symm = complex.conj_lie

theorem complex.isometry_conj :

isometry ⇑(star_ring_end ℂ)

@[simp]

theorem complex.dist_conj_conj (z w : ℂ) :

has_dist.dist (⇑(star_ring_end ℂ) z) (⇑(star_ring_end ℂ) w) = has_dist.dist z w

@[simp]

theorem complex.nndist_conj_conj (z w : ℂ) :

has_nndist.nndist (⇑(star_ring_end ℂ) z) (⇑(star_ring_end ℂ) w) = has_nndist.nndist z w

theorem complex.dist_conj_comm (z w : ℂ) :

has_dist.dist (⇑(star_ring_end ℂ) z) w = has_dist.dist z (⇑(star_ring_end ℂ) w)

theorem complex.nndist_conj_comm (z w : ℂ) :

has_nndist.nndist (⇑(star_ring_end ℂ) z) w = has_nndist.nndist z (⇑(star_ring_end ℂ) w)

@[protected, instance]

def complex.has_continuous_star :

has_continuous_star ℂ

@[continuity]

theorem complex.continuous_conj :

continuous ⇑(star_ring_end ℂ)

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.

noncomputable def complex.conj_cle :

ℂ ≃L[ℝ ] ℂ

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

Equations

complex.conj_cle = ↑complex.conj_lie

@[simp]

theorem complex.conj_cle_coe :

complex.conj_cle.to_linear_equiv = complex.conj_ae.to_linear_equiv

@[simp]

theorem complex.conj_cle_apply (z : ℂ) :

⇑complex.conj_cle z = ⇑(star_ring_end ℂ) z

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_am.to_linear_map, norm_map' := complex.norm_real}

theorem complex.isometry_of_real :

@[continuity]

theorem complex.continuous_of_real :

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.

noncomputable 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

@[simp]

theorem complex.of_real_clm_coe :

↑complex.of_real_clm = complex.of_real_am.to_linear_map

@[simp]

theorem complex.of_real_clm_apply (x : ℝ) :

⇑complex.of_real_clm x = ↑x

@[protected, instance]

noncomputable def complex.is_R_or_C :

Equations

complex.is_R_or_C = {to_densely_normed_field := complex.densely_normed_field, to_star_ring := complex.star_ring, to_normed_algebra := complex.normed_algebra (normed_algebra.id ℝ), to_complete_space := complex.complete_space, 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}, I := complex.I, I_re_ax := complex.is_R_or_C._proof_1, I_mul_I_ax := complex.is_R_or_C._proof_2, re_add_im_ax := complex.is_R_or_C._proof_3, of_real_re_ax := complex.is_R_or_C._proof_4, of_real_im_ax := complex.is_R_or_C._proof_5, mul_re_ax := complex.is_R_or_C._proof_6, mul_im_ax := complex.is_R_or_C._proof_7, conj_re_ax := complex.is_R_or_C._proof_8, conj_im_ax := complex.is_R_or_C._proof_9, conj_I_ax := complex.is_R_or_C._proof_10, norm_sq_eq_def_ax := complex.is_R_or_C._proof_11, mul_im_I_ax := complex.is_R_or_C._proof_12}

theorem is_R_or_C.re_eq_complex_re :

⇑is_R_or_C.re = complex.re

theorem is_R_or_C.im_eq_complex_im :

⇑is_R_or_C.im = complex.im

theorem complex.eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) :

@[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.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.has_sum_conj {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α → 𝕜} {x : 𝕜} :

has_sum (λ (x : α), ⇑(star_ring_end 𝕜) (f x)) x ↔ has_sum f (⇑(star_ring_end 𝕜) x)

theorem is_R_or_C.has_sum_conj' {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α → 𝕜} {x : 𝕜} :

has_sum (λ (x : α), ⇑(star_ring_end 𝕜) (f x)) (⇑(star_ring_end 𝕜) x) ↔ has_sum f x

@[simp]

theorem is_R_or_C.summable_conj {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α → 𝕜} :

summable (λ (x : α), ⇑(star_ring_end 𝕜) (f x)) ↔ summable f

theorem is_R_or_C.conj_tsum {α : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] (f : α → 𝕜) :

⇑(star_ring_end 𝕜) (∑' (a : α), f a) = ∑' (a : α), ⇑(star_ring_end 𝕜) (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 ↔ has_sum f 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)) ↔ summable f

@[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 : has_sum f x) :

has_sum (λ (x : α), ⇑is_R_or_C.re (f x)) (⇑is_R_or_C.re x)

theorem is_R_or_C.has_sum_im {α : Type u_1} (𝕜 : Type u_2) [is_R_or_C 𝕜] {f : α → 𝕜} {x : 𝕜} (h : has_sum f x) :

has_sum (λ (x : α), ⇑is_R_or_C.im (f x)) (⇑is_R_or_C.im 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 : 𝕜) :

has_sum f c ↔ has_sum (λ (x : α), ⇑is_R_or_C.re (f x)) (⇑is_R_or_C.re c) ∧ has_sum (λ (x : α), ⇑is_R_or_C.im (f x)) (⇑is_R_or_C.im c)

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 : α), ⇑(star_ring_end ℂ) (f x)) x ↔ has_sum f (⇑(star_ring_end ℂ) x)

theorem complex.has_sum_conj' {α : Type u_1} {f : α → ℂ} {x : ℂ} :

has_sum (λ (x : α), ⇑(star_ring_end ℂ) (f x)) (⇑(star_ring_end ℂ) x) ↔ has_sum f x

@[simp]

theorem complex.summable_conj {α : Type u_1} {f : α → ℂ} :

summable (λ (x : α), ⇑(star_ring_end ℂ) (f x)) ↔ summable f

theorem complex.conj_tsum {α : Type u_1} (f : α → ℂ) :

⇑(star_ring_end ℂ) (∑' (a : α), f a) = ∑' (a : α), ⇑(star_ring_end ℂ) (f a)

@[simp, norm_cast]

theorem complex.has_sum_of_real {α : Type u_1} {f : α → ℝ} {x : ℝ} :

has_sum (λ (x : α), ↑(f x)) ↑x ↔ has_sum f x

@[simp, norm_cast]

theorem complex.summable_of_real {α : Type u_1} {f : α → ℝ} :

summable (λ (x : α), ↑(f x)) ↔ summable f

@[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 : has_sum f x) :

has_sum (λ (x : α), (f x).re) x.re

theorem complex.has_sum_im {α : Type u_1} {f : α → ℂ} {x : ℂ} (h : has_sum f 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 : ℂ) :

has_sum f c ↔ has_sum (λ (x : α), (f x).re) c.re ∧ has_sum (λ (x : α), (f x).im) c.im