# mathlibdocumentation

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]

Equations
@[instance]

Equations
@[instance]

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

@[simp]
theorem complex.norm_real (r : ) :

@[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 : } :
0 nn = n

@[instance]
def complex.finite_dimensional.proper (E : Type) [normed_group E] [ 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]

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

Equations
@[instance]
def complex.continuous_linear_map.real_smul_complex (E : Type u_1) [normed_group E] [ E] (F : Type u_2) [normed_group F] [ F] :
(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

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

Equations
@[simp]

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

Equations
@[simp]

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

Equations
@[simp]

@[simp]

### Differentiability of the restriction to ℝ of complex functions

theorem has_deriv_at_real_of_complex_aux {e : } {e' : } {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 : } :
e' zhas_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.