# Norm on the complex numbers #

source
instance Complex.instNorm :
Norm ℂ
Equations

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

source
theorem Complex.norm_def (z : ℂ) :
‖z‖ = √(normSq z)
source
theorem Complex.norm_mul_self_eq_normSq (z : ℂ) :
‖z‖ * ‖z‖ = normSq z
source
theorem Complex.abs_re_le_norm (z : ℂ) :
|z.re| ≤ ‖z‖
source
theorem Complex.re_le_norm (z : ℂ) :
z.re ≤ ‖z‖
source
instance Complex.instNormedAddCommGroup :
NormedAddCommGroup ℂ
Equations

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

source
@[simp]
theorem Complex.norm_mul (z w : ℂ) :
‖z * w‖ = ‖z‖ * ‖w‖
source
@[simp]
theorem Complex.norm_div (z w : ℂ) :
‖z / w‖ = ‖z‖ / ‖w‖
source
instance Complex.isAbsoluteValueNorm :
IsAbsoluteValue fun (x : ℂ) => ‖x‖
source
theorem Complex.norm_pow (z : ℂ) (n : ℕ) :
‖z ^ n‖ = ‖z‖ ^ n
source
theorem Complex.norm_zpow (z : ℂ) (n : ℤ) :
‖z ^ n‖ = ‖z‖ ^ n
source
theorem Complex.norm_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) :
‖s.prod f‖ = ∏ i ∈ s, ‖f i‖
source
theorem Complex.norm_conj (z : ℂ) :
‖(starRingEnd ℂ) z‖ = ‖z‖
source
@[simp]
theorem Complex.norm_I :
‖I‖ = 1
source
@[simp]
theorem Complex.nnnorm_I :
‖I‖₊ = 1
source
@[simp]
theorem Complex.norm_real (r : ℝ) :
‖↑r‖ = ‖r‖
source
theorem Complex.norm_of_nonneg {r : ℝ} (h : 0 ≤ r) :
‖↑r‖ = r
source
@[simp]
theorem Complex.nnnorm_real (r : ℝ) :
‖↑r‖₊ = ‖r‖₊
source
theorem Complex.norm_natCast (n : ℕ) :
‖↑n‖ = ↑n
source
@[simp]
theorem Complex.norm_ofNat (n : ℕ) [n.AtLeastTwo] :
‖OfNat.ofNat n‖ = OfNat.ofNat n
source
theorem Complex.norm_two :
‖2‖ = 2
source
@[simp]
theorem Complex.nnnorm_natCast (n : ℕ) :
‖↑n‖₊ = ↑n
source
@[simp]
theorem Complex.nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
‖OfNat.ofNat n‖₊ = OfNat.ofNat n
source
@[simp]
theorem Complex.norm_intCast (n : ℤ) :
‖↑n‖ = |↑n|
source
theorem Complex.norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) :
‖↑n‖ = ↑n
source
@[simp]
theorem Complex.norm_ratCast (q : ℚ) :
‖↑q‖ = |↑q|
source
@[simp]
theorem Complex.norm_nnratCast (q : ℚ≥0) :
‖↑q‖ = ↑q
source
@[simp]
theorem Complex.nnnorm_ratCast (q : ℚ) :
‖↑q‖₊ = ‖↑q‖₊
source
@[simp]
theorem Complex.nnnorm_nnratCast (q : ℚ≥0) :
‖↑q‖₊ = ↑q
source
theorem Complex.normSq_eq_norm_sq (z : ℂ) :
normSq z = ‖z‖ ^ 2
source
theorem Complex.sq_norm (z : ℂ) :
‖z‖ ^ 2 = normSq z
source
@[simp]
theorem Complex.sq_norm_sub_sq_re (z : ℂ) :
‖z‖ ^ 2 - z.re ^ 2 = z.im ^ 2
source
@[simp]
theorem Complex.sq_norm_sub_sq_im (z : ℂ) :
‖z‖ ^ 2 - z.im ^ 2 = z.re ^ 2
source
theorem Complex.norm_add_mul_I (x y : ℝ) :
‖↑x + ↑y * I‖ = √(x ^ 2 + y ^ 2)
source
theorem Complex.norm_eq_sqrt_sq_add_sq (z : ℂ) :
‖z‖ = √(z.re ^ 2 + z.im ^ 2)
source
@[simp]
theorem Complex.range_norm :
(Set.range fun (x : ℂ) => ‖x‖) = Set.Ici 0
source
@[simp]
theorem Complex.range_normSq :
Set.range ⇑normSq = Set.Ici 0
source
theorem Complex.norm_le_abs_re_add_abs_im (z : ℂ) :
‖z‖ ≤ |z.re| + |z.im|
source
theorem Complex.abs_im_le_norm (z : ℂ) :
|z.im| ≤ ‖z‖
source
theorem Complex.im_le_norm (z : ℂ) :
z.im ≤ ‖z‖
source
@[simp]
theorem Complex.abs_re_lt_norm {z : ℂ} :
|z.re| < ‖z‖ ↔ z.im ≠ 0
source
@[simp]
theorem Complex.abs_im_lt_norm {z : ℂ} :
|z.im| < ‖z‖ ↔ z.re ≠ 0
source
@[simp]
theorem Complex.abs_re_eq_norm {z : ℂ} :
|z.re| = ‖z‖ ↔ z.im = 0
source
@[simp]
theorem Complex.abs_im_eq_norm {z : ℂ} :
|z.im| = ‖z‖ ↔ z.re = 0
source
theorem Complex.norm_le_sqrt_two_mul_max (z : ℂ) :
‖z‖ ≤ √2 * max |z.re| |z.im|
source
theorem Complex.abs_re_div_norm_le_one (z : ℂ) :
|z.re / ‖z‖| ≤ 1
source
theorem Complex.abs_im_div_norm_le_one (z : ℂ) :
|z.im / ‖z‖| ≤ 1
source
theorem Complex.dist_eq (z w : ℂ) :
dist z w = ‖z - w‖
source
theorem Complex.dist_eq_re_im (z w : ℂ) :
dist z w = √((z.re - w.re) ^ 2 + (z.im - w.im) ^ 2)
source
@[simp]
theorem Complex.dist_mk (x₁ y₁ x₂ y₂ : ℝ) :
dist { re := x₁, im := y₁ } { re := x₂, im := y₂ } = √((x₁ - x₂) ^ 2 + (y₁ - y₂) ^ 2)
source
theorem Complex.dist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
dist z w = dist z.im w.im
source
theorem Complex.nndist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
nndist z w = nndist z.im w.im
source
theorem Complex.edist_of_re_eq {z w : ℂ} (h : z.re = w.re) :
edist z w = edist z.im w.im
source
theorem Complex.dist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
dist z w = dist z.re w.re
source
theorem Complex.nndist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
nndist z w = nndist z.re w.re
source
theorem Complex.edist_of_im_eq {z w : ℂ} (h : z.im = w.im) :
edist z w = edist z.re w.re
source
theorem Complex.dist_conj_self (z : ℂ) :
dist ((starRingEnd ℂ) z) z = 2 * |z.im|
source
theorem Complex.nndist_conj_self (z : ℂ) :
nndist ((starRingEnd ℂ) z) z = 2 * Real.nnabs z.im
source
theorem Complex.dist_self_conj (z : ℂ) :
dist z ((starRingEnd ℂ) z) = 2 * |z.im|
source
theorem Complex.nndist_self_conj (z : ℂ) :
nndist z ((starRingEnd ℂ) z) = 2 * Real.nnabs z.im

### Cauchy sequences #

source
theorem Complex.isCauSeq_re (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
IsCauSeq abs fun (n : ℕ) => (↑f n).re
source
theorem Complex.isCauSeq_im (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
IsCauSeq abs fun (n : ℕ) => (↑f n).im
source
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, ⋯⟩

Instances For

source
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, ⋯⟩

Instances For

source
theorem Complex.isCauSeq_norm {f : ℕ → ℂ} (hf : IsCauSeq (fun (x : ℂ) => ‖x‖) f) :
IsCauSeq abs ((fun (x : ℂ) => ‖x‖) ∘ f)
source
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 }

Instances For

source
theorem Complex.equiv_limAux (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
f ≈ CauSeq.const (fun (x : ℂ) => ‖x‖) (limAux f)
source
instance Complex.instIsComplete :
CauSeq.IsComplete ℂ fun (x : ℂ) => ‖x‖
source
theorem Complex.lim_eq_lim_im_add_lim_re (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
f.lim = ↑(cauSeqRe f).lim + ↑(cauSeqIm f).lim * I
source
theorem Complex.lim_re (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
(cauSeqRe f).lim = f.lim.re
source
theorem Complex.lim_im (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
(cauSeqIm f).lim = f.lim.im
source
theorem Complex.isCauSeq_conj (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
IsCauSeq (fun (x : ℂ) => ‖x‖) fun (n : ℕ) => (starRingEnd ℂ) (↑f n)
source
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), ⋯⟩

Instances For

source
theorem Complex.lim_conj (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
(cauSeqConj f).lim = (starRingEnd ℂ) f.lim
source
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, ⋯⟩

Instances For

source
theorem Complex.lim_norm (f : CauSeq ℂ fun (x : ℂ) => ‖x‖) :
(cauSeqNorm f).lim = ‖f.lim‖
source
theorem Complex.ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) :
s ≠ 0
source
theorem Complex.ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) :
s ≠ 0
source
theorem Complex.re_neg_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) :
(-s).re ≠ 0
source
theorem Complex.re_neg_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) :
(-s).re ≠ 0
source
theorem Complex.norm_sub_one_sq_eq_of_norm_eq_one {z : ℂ} (hz : ‖z‖ = 1) :
‖z - 1‖ ^ 2 = 2 * (1 - z.re)
source
@[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`.

source
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)
source
theorem Complex.normSq_ofReal_add_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) :
normSq (↑x + I * ↑√(1 - x ^ 2)) = 1
source
theorem Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub {x : ℝ} (hx : ‖x‖ ≤ 1) :
normSq (↑x - I * ↑√(1 - x ^ 2)) = 1