Norm on the complex numbers

instance Complex.instNorm : Norm ℂ

Equations

• Complex.instNorm = { norm := fun (z : ℂ) => √(Complex.normSq z) }

theorem Complex.norm_def (z : ℂ) : ‖z‖ = √(normSq z)

theorem Complex.norm_mul_self_eq_normSq (z : ℂ) : ‖z‖ * ‖z‖ = normSq z

@[deprecated Complex.norm_mul_self_eq_normSq (since := "2025-02-16")]

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

Alias of Complex.norm_mul_self_eq_normSq.

theorem Complex.abs_re_le_norm (z : ℂ) : |z.re| ≤ ‖z‖

theorem Complex.re_le_norm (z : ℂ) : z.re ≤ ‖z‖

@[deprecated Complex.abs_re_le_norm (since := "2025-02-16")]

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

Alias of Complex.abs_re_le_norm.

@[deprecated Complex.re_le_norm (since := "2025-02-16")]

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

Alias of Complex.re_le_norm.

instance Complex.instNormedAddCommGroup : NormedAddCommGroup ℂ

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline, deprecated "use the norm instead" (since := "2025-02-16")]

noncomputable abbrev Complex.abs (z : ℂ) : ℝ

The complex absolute value function, defined as the Complex norm.

Equations

• z.abs = ‖z‖

@[deprecated Complex.norm_def (since := "2025-02-16")]

theorem Complex.abs_apply (z : ℂ) : ‖z‖ = √(normSq z)

Alias of Complex.norm_def.

@[simp]

theorem Complex.norm_mul (z w : ℂ) : ‖z * w‖ = ‖z‖ * ‖w‖

@[simp]

theorem Complex.norm_div (z w : ℂ) : ‖z / w‖ = ‖z‖ / ‖w‖

instance Complex.isAbsoluteValueNorm : IsAbsoluteValue fun (x : ℂ) => ‖x‖

theorem Complex.norm_pow (z : ℂ) (n : ℕ) : ‖z ^ n‖ = ‖z‖ ^ n

theorem Complex.norm_zpow (z : ℂ) (n : ℤ) : ‖z ^ n‖ = ‖z‖ ^ n

theorem Complex.norm_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) : ‖s.prod f‖ = ∏ i ∈ s, ‖f i‖

theorem Complex.norm_conj (z : ℂ) : ‖(starRingEnd ℂ) z‖ = ‖z‖

@[deprecated Complex.norm_pow (since := "2025-02-16")]

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

Alias of Complex.norm_pow.

@[deprecated Complex.norm_zpow (since := "2025-02-16")]

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

Alias of Complex.norm_zpow.

@[deprecated Complex.norm_prod (since := "2025-02-16")]

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

Alias of Complex.norm_prod.

@[deprecated Complex.norm_conj (since := "2025-02-16")]

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

Alias of Complex.norm_conj.

@[deprecated abs_norm (since := "2025-02-16")]

theorem Complex.abs_abs {E : Type u_5} [SeminormedAddGroup E] (z : E) : |‖z‖| = ‖z‖

Alias of abs_norm.

@[simp]

theorem Complex.norm_I : ‖I‖ = 1

@[deprecated Complex.norm_I (since := "2025-02-16")]

theorem Complex.abs_I : ‖I‖ = 1

Alias of Complex.norm_I.

@[simp]

theorem Complex.nnnorm_I : ‖I‖₊ = 1

@[simp]

theorem Complex.norm_real (r : ℝ) : ‖↑r‖ = ‖r‖

theorem Complex.norm_of_nonneg {r : ℝ} (h : 0 ≤ r) : ‖↑r‖ = r

@[deprecated Complex.norm_real (since := "2025-02-16")]

theorem Complex.abs_ofReal (r : ℝ) : ‖↑r‖ = ‖r‖

Alias of Complex.norm_real.

@[deprecated Complex.norm_of_nonneg (since := "2025-02-16")]

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

Alias of Complex.norm_of_nonneg.

@[simp]

theorem Complex.nnnorm_real (r : ℝ) : ‖↑r‖₊ = ‖r‖₊

@[simp]

theorem Complex.norm_natCast (n : ℕ) : ‖↑n‖ = ↑n

@[simp]

theorem Complex.norm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖ = OfNat.ofNat n

theorem Complex.norm_two : ‖2‖ = 2

@[simp]

theorem Complex.nnnorm_natCast (n : ℕ) : ‖↑n‖₊ = ↑n

@[simp]

theorem Complex.nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] : ‖OfNat.ofNat n‖₊ = OfNat.ofNat n

@[deprecated Complex.norm_natCast (since := "2025-02-16")]

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

Alias of Complex.norm_natCast.

@[deprecated Complex.norm_ofNat (since := "2025-02-16")]

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

Alias of Complex.norm_ofNat.

@[deprecated Complex.norm_two (since := "2025-02-16")]

theorem Complex.abs_two : ‖2‖ = 2

Alias of Complex.norm_two.

@[simp]

theorem Complex.norm_intCast (n : ℤ) : ‖↑n‖ = |↑n|

theorem Complex.norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) : ‖↑n‖ = ↑n

@[simp]

theorem Complex.norm_ratCast (q : ℚ) : ‖↑q‖ = |↑q|

@[simp]

theorem Complex.norm_nnratCast (q : ℚ≥0) : ‖↑q‖ = ↑q

@[simp]

theorem Complex.nnnorm_ratCast (q : ℚ) : ‖↑q‖₊ = ‖↑q‖₊

@[simp]

theorem Complex.nnnorm_nnratCast (q : ℚ≥0) : ‖↑q‖₊ = ↑q

@[deprecated Complex.norm_intCast (since := "2025-02-16")]

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

Alias of Complex.norm_intCast.

theorem Complex.normSq_eq_norm_sq (z : ℂ) : normSq z = ‖z‖ ^ 2

theorem Complex.sq_norm (z : ℂ) : ‖z‖ ^ 2 = normSq z

@[simp]

theorem Complex.sq_norm_sub_sq_re (z : ℂ) : ‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2

@[simp]

theorem Complex.sq_norm_sub_sq_im (z : ℂ) : ‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2

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

theorem Complex.norm_eq_sqrt_sq_add_sq (z : ℂ) : ‖z‖ = √(z.re ^ 2 + z.im ^ 2)

@[deprecated Complex.normSq_eq_norm_sq (since := "2025-02-16")]

theorem Complex.normSq_eq_abs (z : ℂ) : normSq z = ‖z‖ ^ 2

Alias of Complex.normSq_eq_norm_sq.

@[deprecated Complex.sq_norm (since := "2025-02-16")]

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

Alias of Complex.sq_norm.

@[deprecated Complex.sq_norm_sub_sq_re (since := "2025-02-16")]

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

Alias of Complex.sq_norm_sub_sq_re.

@[deprecated Complex.sq_norm_sub_sq_im (since := "2025-02-16")]

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

Alias of Complex.sq_norm_sub_sq_im.

@[deprecated Complex.norm_add_mul_I (since := "2025-02-16")]

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

Alias of Complex.norm_add_mul_I.

@[deprecated Complex.norm_eq_sqrt_sq_add_sq (since := "2025-02-16")]

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

Alias of Complex.norm_eq_sqrt_sq_add_sq.

@[simp]

theorem Complex.range_norm : (Set.range fun (x : ℂ) => ‖x‖) = Set.Ici 0

@[deprecated Complex.range_norm (since := "2025-02-16")]

theorem Complex.range_abs : (Set.range fun (x : ℂ) => ‖x‖) = Set.Ici 0

Alias of Complex.range_norm.

@[simp]

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

theorem Complex.norm_le_abs_re_add_abs_im (z : ℂ) : ‖z‖ ≤ |z.re| + |z.im|

theorem Complex.abs_im_le_norm (z : ℂ) : |z.im| ≤ ‖z‖

theorem Complex.im_le_norm (z : ℂ) : z.im ≤ ‖z‖

@[simp]

theorem Complex.abs_re_lt_norm {z : ℂ} : |z.re| < ‖z‖ ↔ z.im ≠ 0

@[simp]

theorem Complex.abs_im_lt_norm {z : ℂ} : |z.im| < ‖z‖ ↔ z.re ≠ 0

@[simp]

theorem Complex.abs_re_eq_norm {z : ℂ} : |z.re| = ‖z‖ ↔ z.im = 0

@[simp]

theorem Complex.abs_im_eq_norm {z : ℂ} : |z.im| = ‖z‖ ↔ z.re = 0

@[deprecated Complex.norm_le_abs_re_add_abs_im (since := "2025-02-16")]

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

Alias of Complex.norm_le_abs_re_add_abs_im.

@[deprecated Complex.abs_im_le_norm (since := "2025-02-16")]

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

Alias of Complex.abs_im_le_norm.

@[deprecated Complex.im_le_norm (since := "2025-02-16")]

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

Alias of Complex.im_le_norm.

@[deprecated Complex.abs_re_lt_norm (since := "2025-02-16")]

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

Alias of Complex.abs_re_lt_norm.

@[deprecated Complex.abs_im_lt_norm (since := "2025-02-16")]

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

Alias of Complex.abs_im_lt_norm.

@[deprecated Complex.abs_re_eq_norm (since := "2025-02-16")]

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

Alias of Complex.abs_re_eq_norm.

@[deprecated Complex.abs_im_eq_norm (since := "2025-02-16")]

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

Alias of Complex.abs_im_eq_norm.

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

theorem Complex.abs_re_div_norm_le_one (z : ℂ) : |z.re / ‖z‖| ≤ 1

theorem Complex.abs_im_div_norm_le_one (z : ℂ) : |z.im / ‖z‖| ≤ 1

@[deprecated Complex.norm_le_sqrt_two_mul_max (since := "2025-02-16")]

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

Alias of Complex.norm_le_sqrt_two_mul_max.

@[deprecated Complex.abs_re_div_norm_le_one (since := "2025-02-16")]

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

Alias of Complex.abs_re_div_norm_le_one.

@[deprecated Complex.abs_im_div_norm_le_one (since := "2025-02-16")]

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

Alias of Complex.abs_im_div_norm_le_one.

theorem Complex.dist_eq (z w : ℂ) : dist z w = ‖z - w‖

theorem Complex.dist_eq_re_im (z w : ℂ) : dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)

@[simp]

theorem Complex.dist_mk (x₁ y₁ x₂ y₂ : ℝ) : dist { re := x₁, im := y₁ } { re := x₂, im := y₂ } = √((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)

theorem Complex.dist_of_re_eq {z w : ℂ} (h : z.re = w.re) : dist z w = dist z.im w.im

theorem Complex.nndist_of_re_eq {z w : ℂ} (h : z.re = w.re) : nndist z w = nndist z.im w.im

theorem Complex.edist_of_re_eq {z w : ℂ} (h : z.re = w.re) : edist z w = edist z.im w.im

theorem Complex.dist_of_im_eq {z w : ℂ} (h : z.im = w.im) : dist z w = dist z.re w.re

theorem Complex.nndist_of_im_eq {z w : ℂ} (h : z.im = w.im) : nndist z w = nndist z.re w.re

theorem Complex.edist_of_im_eq {z w : ℂ} (h : z.im = w.im) : edist z w = edist z.re w.re

theorem Complex.dist_conj_self (z : ℂ) : dist ((starRingEnd ℂ) z) z = 2 * |z.im|

theorem Complex.nndist_conj_self (z : ℂ) : nndist ((starRingEnd ℂ) z) z = 2 * Real.nnabs z.im

theorem Complex.dist_self_conj (z : ℂ) : dist z ((starRingEnd ℂ) z) = 2 * |z.im|

theorem Complex.nndist_self_conj (z : ℂ) : nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im

Cauchy sequences

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

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

noncomputable def Complex.cauSeqRe (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : CauSeq ℝ 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 ℂ fun (x : ℂ) => ‖x‖) : CauSeq ℝ 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_norm {f : ℕ → ℂ} (hf : IsCauSeq (fun (x : ℂ) => ‖x‖) f) : IsCauSeq abs ((fun (x : ℂ) => ‖x‖) ∘ f)

noncomputable def Complex.limAux (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : ℂ

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 ℂ fun (x : ℂ) => ‖x‖) : f ≈ CauSeq.const (fun (x : ℂ) => ‖x‖) (limAux f)

instance Complex.instIsComplete : CauSeq.IsComplete ℂ fun (x : ℂ) => ‖x‖

theorem Complex.lim_eq_lim_im_add_lim_re (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : f.lim = ↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I

theorem Complex.lim_re (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : (cauSeqRe f).lim = f.lim.re

theorem Complex.lim_im (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : (cauSeqIm f).lim = f.lim.im

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

noncomputable def Complex.cauSeqConj (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : CauSeq ℂ fun (x : ℂ) => ‖x‖

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 ℂ fun (x : ℂ) => ‖x‖) : (cauSeqConj f).lim = (starRingEnd ℂ) f.lim

noncomputable def Complex.cauSeqNorm (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : CauSeq ℝ abs

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

Equations

• Complex.cauSeqNorm f = ⟨(fun (x : ℂ) => ‖x‖) ∘ ↑f, ⋯⟩

theorem Complex.lim_norm (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : (cauSeqNorm f).lim = ‖f.lim‖

@[deprecated Complex.isCauSeq_norm (since := "2025-02-16")]

theorem Complex.isCauSeq_abs {f : ℕ → ℂ} (hf : IsCauSeq (fun (x : ℂ) => ‖x‖) f) : IsCauSeq abs ((fun (x : ℂ) => ‖x‖) ∘ f)

Alias of Complex.isCauSeq_norm.

@[deprecated Complex.cauSeqNorm (since := "2025-02-16")]

def Complex.cauSeqAbs (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : CauSeq ℝ abs

Alias of Complex.cauSeqNorm.

---

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

Equations

• Complex.cauSeqAbs = Complex.cauSeqNorm

@[deprecated Complex.lim_norm (since := "2025-02-16")]

theorem Complex.lim_abs (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) : (cauSeqNorm f).lim = ‖f.lim‖

Alias of Complex.lim_norm.

theorem Complex.ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : s ≠ 0

theorem Complex.ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : s ≠ 0

theorem Complex.re_neg_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : (-s).re ≠ 0

theorem Complex.re_neg_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : (-s).re ≠ 0