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.recontinuous_linear_map.imcontinuous_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.
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}
Equations
- complex.nondiscrete_normed_field = {to_normed_field := complex.normed_field, non_trivial := complex.nondiscrete_normed_field._proof_1}
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}
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.
Equations
- _ = _
A complex normed vector space is also a real normed vector space.
The space of continuous linear maps over ℝ, from a real vector space to a complex vector
space, is a normed vector space over ℂ.
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
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
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
Differentiability of the restriction to ℝ of complex functions
A preliminary lemma for has_deriv_at_real_of_complex,
which we only separate out to keep the maximum compile time per declaration low.
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.