# Documentation

Mathlib.Data.Complex.Abs

# Absolute values of complex numbers #

### Absolute value #

noncomputable def Complex.abs :

The complex absolute value function, defined as the square root of the norm squared.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Complex.abs_def :
= fun (z : ) =>
@[simp]
theorem Complex.abs_ofReal (r : ) :
= |r|
theorem Complex.abs_of_nonneg {r : } (h : 0 r) :
= r
@[simp]
theorem Complex.abs_natCast (n : ) :
= n
@[simp]
theorem Complex.abs_ofNat (n : ) [] :
theorem Complex.sq_abs (z : ) :
^ 2 =
@[simp]
theorem Complex.sq_abs_sub_sq_re (z : ) :
^ 2 - z.re ^ 2 = z.im ^ 2
@[simp]
theorem Complex.sq_abs_sub_sq_im (z : ) :
^ 2 - z.im ^ 2 = z.re ^ 2
@[simp]
theorem Complex.abs_I :
@[simp]
@[simp]
theorem Complex.abs_conj (z : ) :
Complex.abs (() z) =
theorem Complex.abs_prod {ι : Type u_1} (s : ) (f : ι) :
Complex.abs () = Finset.prod s fun (I : ι) => Complex.abs (f I)
theorem Complex.abs_pow (z : ) (n : ) :
Complex.abs (z ^ n) = ^ n
theorem Complex.abs_zpow (z : ) (n : ) :
Complex.abs (z ^ n) = ^ n
theorem Complex.abs_re_le_abs (z : ) :
|z.re|
theorem Complex.abs_im_le_abs (z : ) :
|z.im|
theorem Complex.re_le_abs (z : ) :
z.re
theorem Complex.im_le_abs (z : ) :
z.im
@[simp]
theorem Complex.abs_re_lt_abs {z : } :
|z.re| < z.im 0
@[simp]
theorem Complex.abs_im_lt_abs {z : } :
|z.im| < z.re 0
@[simp]
theorem Complex.abs_re_eq_abs {z : } :
|z.re| = z.im = 0
@[simp]
theorem Complex.abs_im_eq_abs {z : } :
|z.im| = z.re = 0
@[simp]
theorem Complex.abs_abs (z : ) :
|| =
theorem Complex.abs_le_abs_re_add_abs_im (z : ) :
|z.re| + |z.im|
theorem Complex.abs_le_sqrt_two_mul_max (z : ) :
* max |z.re| |z.im|
theorem Complex.abs_re_div_abs_le_one (z : ) :
|z.re / | 1
theorem Complex.abs_im_div_abs_le_one (z : ) :
|z.im / | 1
@[simp]
theorem Complex.int_cast_abs (n : ) :
|n| =
@[simp]

### Cauchy sequences #

theorem Complex.isCauSeq_re (f : ) :
IsCauSeq abs fun (n : ) => (f n).re
theorem Complex.isCauSeq_im (f : ) :
IsCauSeq abs fun (n : ) => (f n).im
noncomputable def Complex.cauSeqRe (f : ) :

The real part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
• = { val := fun (n : ) => (f n).re, property := (_ : IsCauSeq abs fun (n : ) => (f n).re) }
Instances For
noncomputable def Complex.cauSeqIm (f : ) :

The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
• = { val := fun (n : ) => (f n).im, property := (_ : IsCauSeq abs fun (n : ) => (f n).im) }
Instances For
theorem Complex.isCauSeq_abs {f : } (hf : ) :
IsCauSeq abs ()
noncomputable def Complex.limAux (f : ) :

The limit of a Cauchy sequence of complex numbers.

Equations
• = { re := , im := }
Instances For
theorem Complex.equiv_limAux (f : ) :
f
Equations
theorem Complex.lim_re (f : ) :
= ().re
theorem Complex.lim_im (f : ) :
= ().im
theorem Complex.isCauSeq_conj (f : ) :
IsCauSeq fun (n : ) => () (f n)
noncomputable def Complex.cauSeqConj (f : ) :

The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.

Equations
• = { val := fun (n : ) => () (f n), property := (_ : IsCauSeq fun (n : ) => () (f n)) }
Instances For
theorem Complex.lim_conj (f : ) :
= () ()
noncomputable def Complex.cauSeqAbs (f : ) :

The absolute value of a complex Cauchy sequence, as a real Cauchy sequence.

Equations
Instances For
theorem Complex.lim_abs (f : ) :
theorem Complex.ne_zero_of_one_lt_re {s : } (hs : 1 < s.re) :
s 0
theorem Complex.re_neg_ne_zero_of_one_lt_re {s : } (hs : 1 < s.re) :
(-s).re 0