Documentation

Mathlib.Data.Complex.Abs

Absolute values of complex numbers #

Absolute value #

theorem Complex.AbsTheory.abs_conj (z : ) :
Real.sqrt (Complex.normSq ((starRingEnd ) z)) = Real.sqrt (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 :
    Complex.abs = fun (z : ) => Real.sqrt (Complex.normSq z)
    theorem Complex.abs_apply {z : } :
    Complex.abs z = Real.sqrt (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 : ) [Nat.AtLeastTwo n] :
    Complex.abs (OfNat.ofNat n) = OfNat.ofNat n
    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 + y * Complex.I) = Real.sqrt (x ^ 2 + y ^ 2)
    theorem Complex.abs_eq_sqrt_sq_add_sq (z : ) :
    Complex.abs z = Real.sqrt (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]
    theorem Complex.abs_conj (z : ) :
    Complex.abs ((starRingEnd ) z) = Complex.abs z
    theorem Complex.abs_prod {ι : Type u_1} (s : Finset ι) (f : ι) :
    Complex.abs (Finset.prod s f) = Finset.prod s fun (I : ι) => 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 Real.sqrt 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

    Cauchy sequences #

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

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

    Equations
    Instances For
      noncomputable def Complex.cauSeqIm (f : CauSeq Complex.abs) :

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

      Equations
      Instances For
        theorem Complex.isCauSeq_abs {f : } (hf : IsCauSeq (Complex.abs) f) :
        noncomputable def Complex.limAux (f : CauSeq Complex.abs) :

        The limit of a Cauchy sequence of complex numbers.

        Equations
        Instances For

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

          Equations
          Instances For
            noncomputable def Complex.cauSeqAbs (f : CauSeq Complex.abs) :

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

            Equations
            Instances For
              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