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:

continuous_linear_map.re
continuous_linear_map.im
continuous_linear_map.of_real

They are bundled versions of the real part, the imaginary part, and the embedding of ℝ in ℂ, as continuous ℝ-linear maps.

has_deriv_at_real_of_complex expresses that, if a function on ℂ is differentiable (over ℂ), then its restriction to ℝ is differentiable over ℝ, with derivative the real part of the complex derivative.

@[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 := _, neg := field.neg complex.field, add_left_neg := _, add_comm := _, mul := field.mul complex.field, mul_assoc := _, one := field.one complex.field, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := field.inv complex.field, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}, to_metric_space := complex.metric_space, 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_over_reals :

normed_algebra ℝ ℂ

Equations

complex.normed_algebra_over_reals = {to_algebra := {to_has_scalar := algebra.to_has_scalar complex.algebra_over_reals, to_ring_hom := algebra.to_ring_hom complex.algebra_over_reals, commutes' := complex.normed_algebra_over_reals._proof_1, smul_def' := complex.normed_algebra_over_reals._proof_2}, norm_algebra_map_eq := complex.abs_of_real}

@[simp]

theorem complex.norm_eq_abs (z : ℂ) :

∥z∥ = complex.abs z

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

@[instance]

def complex.finite_dimensional.proper (E : Type) [normed_group E] [normed_space ℂ E] [finite_dimensional ℂ E] :

Over the complex numbers, any finite-dimensional spaces is proper (and therefore complete). We can register this as an instance, as it will not cause problems in instance resolution since the properness of ℂ is already known and there is no metavariable.

@[instance]

def complex.normed_space.restrict_scalars_real (E : Type u_1) [normed_group E] [normed_space ℂ E] :

normed_space ℝ E

A complex normed vector space is also a real normed vector space.

Equations

complex.normed_space.restrict_scalars_real E = normed_space.restrict_scalars' ℝ ℂ E

@[instance]

def complex.continuous_linear_map.real_smul_complex (E : Type u_1) [normed_group E] [normed_space ℝ E] (F : Type u_2) [normed_group F] [normed_space ℂ F] :

normed_space ℂ (E →L[ℝ ] F)

The space of continuous linear maps over ℝ, from a real vector space to a complex vector space, is a normed vector space over ℂ.

Equations

complex.continuous_linear_map.real_smul_complex E F = continuous_linear_map.normed_space_extend_scalars

def complex.continuous_linear_map.re :

ℂ →L[ℝ ] ℝ

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

Equations

complex.continuous_linear_map.re = complex.linear_map.re.mk_continuous 1 complex.continuous_linear_map.re._proof_1

@[simp]

theorem complex.continuous_linear_map.re_coe :

↑complex.continuous_linear_map.re = complex.linear_map.re

@[simp]

theorem complex.continuous_linear_map.re_apply (z : ℂ) :

⇑complex.continuous_linear_map.re z = z.re

@[simp]

theorem complex.continuous_linear_map.re_norm :

∥complex.continuous_linear_map.re ∥ = 1

def complex.continuous_linear_map.im :

ℂ →L[ℝ ] ℝ

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

Equations

complex.continuous_linear_map.im = complex.linear_map.im.mk_continuous 1 complex.continuous_linear_map.im._proof_1

@[simp]

theorem complex.continuous_linear_map.im_coe :

↑complex.continuous_linear_map.im = complex.linear_map.im

@[simp]

theorem complex.continuous_linear_map.im_apply (z : ℂ) :

⇑complex.continuous_linear_map.im z = z.im

@[simp]

theorem complex.continuous_linear_map.im_norm :

∥complex.continuous_linear_map.im ∥ = 1

def complex.continuous_linear_map.of_real :

ℝ →L[ℝ ] ℂ

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

Equations

complex.continuous_linear_map.of_real = complex.linear_map.of_real.mk_continuous 1 complex.continuous_linear_map.of_real._proof_1

@[simp]

theorem complex.continuous_linear_map.of_real_coe :

↑complex.continuous_linear_map.of_real = complex.linear_map.of_real

@[simp]

theorem complex.continuous_linear_map.of_real_apply (x : ℝ) :

⇑complex.continuous_linear_map.of_real x = ↑x

@[simp]

theorem complex.continuous_linear_map.of_real_norm :

∥complex.continuous_linear_map.of_real ∥ = 1

theorem complex.continuous_linear_map.of_real_isometry :

isometry ⇑complex.continuous_linear_map.of_real

Differentiability of the restriction to `ℝ` of complex functions

theorem has_deriv_at_real_of_complex_aux {e : ℂ → ℂ} {e' : ℂ} {z : ℝ} (h : has_deriv_at e e' ↑z) :

has_deriv_at (⇑complex.continuous_linear_map.re ∘ λ {z : ℝ}, e (⇑complex.continuous_linear_map.of_real z)) (⇑((complex.continuous_linear_map.re.comp (continuous_linear_map.restrict_scalars ℝ (1.smul_right e'))).comp complex.continuous_linear_map.of_real) 1) z

A preliminary lemma for has_deriv_at_real_of_complex, which we only separate out to keep the maximum compile time per declaration low.

theorem has_deriv_at_real_of_complex {e : ℂ → ℂ} {e' : ℂ} {z : ℝ} (h : has_deriv_at e e' ↑z) :

has_deriv_at (λ (x : ℝ), (e ↑x).re) e'.re z

If a complex function is differentiable at a real point, then the induced real function is also differentiable at this point, with a derivative equal to the real part of the complex derivative.