Absolute values of complex numbers

Absolute value

theorem Complex.AbsTheory.abs_conj (z : ℂ) : √(normSq ((starRingEnd ℂ) z)) = √(normSq z)

noncomputable def Complex.abs : AbsoluteValue ℂ ℝ

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.

theorem Complex.abs_def : ⇑abs = fun (z : ℂ) => √(normSq z)

theorem Complex.abs_apply {z : ℂ} : abs z = √(normSq z)

@[simp]

theorem Complex.abs_ofReal (r : ℝ) : abs ↑r = |r|

theorem Complex.abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : abs ↑r = r

@[simp]

theorem Complex.abs_natCast (n : ℕ) : abs ↑n = ↑n

@[simp]

theorem Complex.abs_ofNat (n : ℕ) [n.AtLeastTwo] : abs (OfNat.ofNat n) = OfNat.ofNat n

theorem Complex.mul_self_abs (z : ℂ) : abs z * abs z = normSq z

theorem Complex.sq_abs (z : ℂ) : abs z ^ 2 = normSq z

@[simp]

theorem Complex.sq_abs_sub_sq_re (z : ℂ) : abs z ^ 2 - z.re ^ 2 = z.im ^ 2

@[simp]

theorem Complex.sq_abs_sub_sq_im (z : ℂ) : abs z ^ 2 - z.im ^ 2 = z.re ^ 2

theorem Complex.abs_add_mul_I (x y : ℝ) : abs (↑x + ↑y * I) = √(x ^ 2 + y ^ 2)

theorem Complex.abs_eq_sqrt_sq_add_sq (z : ℂ) : abs z = √(z.re ^ 2 + z.im ^ 2)

@[simp]

theorem Complex.abs_I : abs I = 1

theorem Complex.abs_two : abs 2 = 2

@[simp]

theorem Complex.range_abs : Set.range ⇑abs = Set.Ici 0

@[simp]

theorem Complex.abs_conj (z : ℂ) : abs ((starRingEnd ℂ) z) = abs z

theorem Complex.abs_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) : abs (s.prod f) = ∏ I ∈ s, abs (f I)

theorem Complex.abs_pow (z : ℂ) (n : ℕ) : abs (z ^ n) = abs z ^ n

theorem Complex.abs_zpow (z : ℂ) (n : ℤ) : abs (z ^ n) = abs z ^ n

theorem Complex.abs_re_le_abs (z : ℂ) : |z.re| ≤ abs z

theorem Complex.abs_im_le_abs (z : ℂ) : |z.im| ≤ abs z

theorem Complex.re_le_abs (z : ℂ) : z.re ≤ abs z

theorem Complex.im_le_abs (z : ℂ) : z.im ≤ abs z

@[simp]

theorem Complex.abs_re_lt_abs {z : ℂ} : |z.re| < abs z ↔ z.im ≠ 0

@[simp]

theorem Complex.abs_im_lt_abs {z : ℂ} : |z.im| < abs z ↔ z.re ≠ 0

@[simp]

theorem Complex.abs_re_eq_abs {z : ℂ} : |z.re| = abs z ↔ z.im = 0

@[simp]

theorem Complex.abs_im_eq_abs {z : ℂ} : |z.im| = abs z ↔ z.re = 0

@[simp]

theorem Complex.abs_abs (z : ℂ) : |abs z| = abs z

theorem Complex.abs_le_abs_re_add_abs_im (z : ℂ) : abs z ≤ |z.re| + |z.im|

theorem Complex.abs_le_sqrt_two_mul_max (z : ℂ) : abs z ≤ √2 * (|z.re| ⊔ |z.im|)

theorem Complex.abs_re_div_abs_le_one (z : ℂ) : |z.re / abs z| ≤ 1

theorem Complex.abs_im_div_abs_le_one (z : ℂ) : |z.im / abs z| ≤ 1

@[simp]

theorem Complex.abs_intCast (n : ℤ) : abs ↑n = |↑n|

theorem Complex.normSq_eq_abs (x : ℂ) : normSq x = abs x ^ 2

@[simp]

theorem Complex.range_normSq : Set.range ⇑normSq = Set.Ici 0

Cauchy sequences

theorem Complex.isCauSeq_re (f : CauSeq ℂ ⇑abs) : IsCauSeq _root_.abs fun (n : ℕ) => (↑f n).re

theorem Complex.isCauSeq_im (f : CauSeq ℂ ⇑abs) : IsCauSeq _root_.abs fun (n : ℕ) => (↑f n).im

noncomputable def Complex.cauSeqRe (f : CauSeq ℂ ⇑abs) : CauSeq ℝ _root_.abs

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

Equations

• Complex.cauSeqRe f = ⟨fun (n : ℕ) => (↑f n).re, ⋯⟩

noncomputable def Complex.cauSeqIm (f : CauSeq ℂ ⇑abs) : CauSeq ℝ _root_.abs

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

Equations

• Complex.cauSeqIm f = ⟨fun (n : ℕ) => (↑f n).im, ⋯⟩

theorem Complex.isCauSeq_abs {f : ℕ → ℂ} (hf : IsCauSeq (⇑abs) f) : IsCauSeq _root_.abs (⇑abs ∘ f)

noncomputable def Complex.limAux (f : CauSeq ℂ ⇑abs) : ℂ

The limit of a Cauchy sequence of complex numbers.

Equations

• Complex.limAux f = { re := (Complex.cauSeqRe f).lim, im := (Complex.cauSeqIm f).lim }

theorem Complex.equiv_limAux (f : CauSeq ℂ ⇑abs) : f ≈ CauSeq.const (⇑abs) (limAux f)

instance Complex.instIsComplete : CauSeq.IsComplete ℂ ⇑abs

theorem Complex.lim_eq_lim_im_add_lim_re (f : CauSeq ℂ ⇑abs) : f.lim = ↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I

theorem Complex.lim_re (f : CauSeq ℂ ⇑abs) : (cauSeqRe f).lim = f.lim.re

theorem Complex.lim_im (f : CauSeq ℂ ⇑abs) : (cauSeqIm f).lim = f.lim.im

theorem Complex.isCauSeq_conj (f : CauSeq ℂ ⇑abs) : IsCauSeq ⇑abs fun (n : ℕ) => (starRingEnd ℂ) (↑f n)

noncomputable def Complex.cauSeqConj (f : CauSeq ℂ ⇑abs) : CauSeq ℂ ⇑abs

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

Equations

• Complex.cauSeqConj f = ⟨fun (n : ℕ) => (starRingEnd ℂ) (↑f n), ⋯⟩

theorem Complex.lim_conj (f : CauSeq ℂ ⇑abs) : (cauSeqConj f).lim = (starRingEnd ℂ) f.lim

noncomputable def Complex.cauSeqAbs (f : CauSeq ℂ ⇑abs) : CauSeq ℝ _root_.abs

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

Equations

• Complex.cauSeqAbs f = ⟨⇑Complex.abs ∘ ↑f, ⋯⟩

theorem Complex.lim_abs (f : CauSeq ℂ ⇑abs) : (cauSeqAbs f).lim = 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