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.

@[instance]

Equations
@[simp]

theorem complex.dist_eq (z w : ) :
dist z w = complex.abs (z - w)

@[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 : } (hn : 0 n) :

@[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 : } (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.

theorem times_cont_diff_at.real_of_complex {e : } {z : } {n : with_top } (h : times_cont_diff_at n e z) :
times_cont_diff_at n (λ (x : ), (e x).re) z

theorem times_cont_diff.real_of_complex {e : } {n : with_top } (h : times_cont_diff n e) :
times_cont_diff n (λ (x : ), (e x).re)