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 : 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 : ⇑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)

@[simp]

theorem Complex.abs_I : Complex.abs Complex.I = 1

theorem Complex.abs_two : Complex.abs 2 = 2

@[simp]

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

@[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|

instance Complex.instNeZeroRealInstZeroRealOfNatToOfNat1InstOneReal : NeZero 1

Equations

• Complex.instNeZeroRealInstZeroRealOfNatToOfNat1InstOneReal = (_ : NeZero 1)

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.int_cast_abs (n : ℤ) : |↑n| = Complex.abs ↑n

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

@[simp]

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

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) : CauSeq ℝ abs

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

Equations

• Complex.cauSeqRe f = { val := fun (n : ℕ) => (↑f n).re, property := (_ : IsCauSeq abs fun (n : ℕ) => (↑f n).re) }

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

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

Equations

• Complex.cauSeqIm f = { val := fun (n : ℕ) => (↑f n).im, property := (_ : IsCauSeq abs fun (n : ℕ) => (↑f n).im) }

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

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

The limit of a Cauchy sequence of complex numbers.

Equations

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

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

instance Complex.instIsComplete : CauSeq.IsComplete ℂ ⇑Complex.abs

Equations

• Complex.instIsComplete = (_ : CauSeq.IsComplete ℂ ⇑Complex.abs)

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

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

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

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

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

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

Equations

• Complex.cauSeqConj f = { val := fun (n : ℕ) => (starRingEnd ℂ) (↑f n), property := (_ : IsCauSeq ⇑Complex.abs fun (n : ℕ) => (starRingEnd ℂ) (↑f n)) }

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

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

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

Equations

• Complex.cauSeqAbs f = { val := ⇑Complex.abs ∘ ↑f, property := (_ : IsCauSeq abs (⇑Complex.abs ∘ ↑f)) }

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