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

@[simp]

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

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]

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

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

Equations

Continuous linear map version of the canonical embedding of in .

Equations

Differentiability of the restriction to of complex functions

theorem has_deriv_at_real_of_complex {e : } {e' : } {z : } :
has_deriv_at e 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.