Norm on the complex numbers

@[implicit_reducible]

noncomputable instance Complex.instNorm : Norm ℂ

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

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

theorem Complex.norm_nonneg (z : ℂ) : 0 ≤ ‖z‖

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

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

theorem Complex.norm_add_le' (z w : ℂ) : ‖z + w‖ ≤ ‖z‖ + ‖w‖

theorem Complex.norm_eq_zero_iff {z : ℂ} : ‖z‖ = 0 ↔ z = 0

theorem Complex.norm_map_zero' : ‖0‖ = 0

theorem Complex.norm_neg' (z : ℂ) : ‖-z‖ = ‖z‖

@[implicit_reducible]

noncomputable instance Complex.instNormedAddCommGroup : NormedAddCommGroup ℂ

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

@[simp]

theorem Complex.norm_I : ‖I‖ = 1

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

@[simp]

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

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

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

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

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

theorem Complex.one_lt_normSq_iff {x : ℂ} : 1 < normSq x ↔ 1 < ‖x‖

theorem Complex.one_le_normSq_iff {x : ℂ} : 1 ≤ normSq x ↔ 1 ≤ ‖x‖

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

@[simp]

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

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

theorem Complex.norm_le_sqrt_two_mul_max (z : ℂ) : ‖z‖ ≤ √2 * max |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

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.

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

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

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.

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.

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.

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

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

theorem Complex.norm_sub_one_sq_eq_of_norm_eq_one {z : ℂ} (hz : ‖z‖ = 1) : ‖z - 1‖ ^ 2 = 2 * (1 - z.re)

@[deprecated Complex.norm_sub_one_sq_eq_of_norm_eq_one (since := "2025-11-15")]

theorem Complex.norm_sub_one_sq_eq_of_norm_one {z : ℂ} (hz : ‖z‖ = 1) : ‖z - 1‖ ^ 2 = 2 * (1 - z.re)

Alias of Complex.norm_sub_one_sq_eq_of_norm_eq_one.

theorem Complex.norm_sub_one_sq_eqOn_sphere : Set.EqOn (fun (x : ℂ) => ‖x - 1‖ ^ 2) (fun (z : ℂ) => 2 * (1 - z.re)) (Metric.sphere 0 1)

theorem Complex.normSq_ofReal_add_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) : normSq (↑x + I * ↑√(1 - x ^ 2)) = 1

theorem Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) : normSq (↑x - I * ↑√(1 - x ^ 2)) = 1