# Absolute values of complex numbers #

### Absolute value #

theorem Complex.AbsTheory.abs_conj (z : ) :
(Complex.normSq (() z)) = (Complex.normSq z)
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 : ) => (Complex.normSq z)
theorem Complex.abs_apply {z : } :
Complex.abs z = (Complex.normSq z)
@[simp]
theorem Complex.abs_ofReal (r : ) :
Complex.abs r = |r|
theorem Complex.abs_of_nonneg {r : } (h : 0 r) :
Complex.abs r = r
@[simp]
theorem Complex.abs_natCast (n : ) :
Complex.abs n = n
@[simp]
theorem Complex.abs_ofNat (n : ) [n.AtLeastTwo] :
Complex.abs () =
theorem Complex.mul_self_abs (z : ) :
Complex.abs z * Complex.abs z = Complex.normSq z
theorem Complex.sq_abs (z : ) :
Complex.abs z ^ 2 = Complex.normSq z
@[simp]
theorem Complex.sq_abs_sub_sq_re (z : ) :
Complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2
@[simp]
theorem Complex.sq_abs_sub_sq_im (z : ) :
Complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2
theorem Complex.abs_add_mul_I (x : ) (y : ) :
Complex.abs (x + ) = (x ^ 2 + y ^ 2)
theorem Complex.abs_eq_sqrt_sq_add_sq (z : ) :
Complex.abs z = (z.re ^ 2 + z.im ^ 2)
@[simp]
theorem Complex.abs_I :
Complex.abs Complex.I = 1
theorem Complex.abs_two :
Complex.abs 2 = 2
@[simp]
@[simp]
theorem Complex.abs_conj (z : ) :
Complex.abs (() z) = Complex.abs z
theorem Complex.abs_prod {ι : Type u_1} (s : ) (f : ι) :
Complex.abs (s.prod f) = Is, Complex.abs (f I)
theorem Complex.abs_pow (z : ) (n : ) :
Complex.abs (z ^ n) = Complex.abs z ^ n
theorem Complex.abs_zpow (z : ) (n : ) :
Complex.abs (z ^ n) = Complex.abs z ^ n
theorem Complex.abs_re_le_abs (z : ) :
|z.re| Complex.abs z
theorem Complex.abs_im_le_abs (z : ) :
|z.im| Complex.abs z
theorem Complex.re_le_abs (z : ) :
z.re Complex.abs z
theorem Complex.im_le_abs (z : ) :
z.im Complex.abs z
@[simp]
theorem Complex.abs_re_lt_abs {z : } :
|z.re| < Complex.abs z z.im 0
@[simp]
theorem Complex.abs_im_lt_abs {z : } :
|z.im| < Complex.abs z z.re 0
@[simp]
theorem Complex.abs_re_eq_abs {z : } :
|z.re| = Complex.abs z z.im = 0
@[simp]
theorem Complex.abs_im_eq_abs {z : } :
|z.im| = Complex.abs z z.re = 0
@[simp]
theorem Complex.abs_abs (z : ) :
|Complex.abs z| = Complex.abs z
theorem Complex.abs_le_abs_re_add_abs_im (z : ) :
Complex.abs z |z.re| + |z.im|
theorem Complex.abs_le_sqrt_two_mul_max (z : ) :
Complex.abs z 2 * max |z.re| |z.im|
theorem Complex.abs_re_div_abs_le_one (z : ) :
|z.re / Complex.abs z| 1
theorem Complex.abs_im_div_abs_le_one (z : ) :
|z.im / Complex.abs z| 1
@[simp]
theorem Complex.abs_intCast (n : ) :
Complex.abs n = |n|
@[deprecated]
theorem Complex.int_cast_abs (n : ) :
|n| = Complex.abs n
theorem Complex.normSq_eq_abs (x : ) :
Complex.normSq x = Complex.abs x ^ 2
@[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
• = 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
• = 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 := ().lim, im := ().lim }
Instances For
theorem Complex.equiv_limAux (f : ) :
f
Equations
theorem Complex.lim_eq_lim_im_add_lim_re (f : ) :
f.lim = ().lim + ().lim * Complex.I
theorem Complex.lim_re (f : ) :
().lim = f.lim.re
theorem Complex.lim_im (f : ) :
().lim = f.lim.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
• = fun (n : ) => () (f n),
Instances For
theorem Complex.lim_conj (f : ) :
.lim = () f.lim
noncomputable def Complex.cauSeqAbs (f : ) :

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

Equations
• = f,
Instances For
theorem Complex.lim_abs (f : ) :
.lim = Complex.abs f.lim
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