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

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

source

theorem Complex.abs_re_le_norm (z : ℂ) :

|z.re| ≤ ‖z‖

source

theorem Complex.re_le_norm (z : ℂ) :

z.re ≤ ‖z‖

source

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

source

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

theorem Complex.re_le_abs (z : ℂ) :

z.re ≤ ‖z‖

Alias of Complex.re_le_norm.

source

instance Complex.instNormedAddCommGroup :

NormedAddCommGroup ℂ

Equations

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

source

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

Instances For

source

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

theorem Complex.abs_apply (z : ℂ) :

‖z‖ = √(normSq z)

Alias of Complex.norm_def.

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

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

theorem Complex.abs_pow (z : ℂ) (n : ℕ) :

‖z ^ n‖ = ‖z‖ ^ n

Alias of Complex.norm_pow.

source

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

theorem Complex.abs_zpow (z : ℂ) (n : ℤ) :

‖z ^ n‖ = ‖z‖ ^ n

Alias of Complex.norm_zpow.

source

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

source

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

theorem Complex.abs_conj (z : ℂ) :

‖(starRingEnd ℂ) z‖ = ‖z‖

Alias of Complex.norm_conj.

source

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

source

@[simp]

theorem Complex.norm_I :

‖I ‖ = 1

source

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

theorem Complex.abs_I :

‖I ‖ = 1

Alias of Complex.norm_I.

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

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

theorem Complex.abs_ofReal (r : ℝ) :

‖↑r‖ = ‖r‖

Alias of Complex.norm_real.

source

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

source

@[simp]

theorem Complex.nnnorm_real (r : ℝ) :

‖↑r‖₊ = ‖r‖₊

source

@[simp]

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

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

theorem Complex.abs_natCast (n : ℕ) :

‖↑n‖ = ↑n

Alias of Complex.norm_natCast.

source

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

source

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

theorem Complex.abs_two :

‖2‖ = 2

Alias of Complex.norm_two.

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

@[deprecated Complex.norm_natCast (since := "2024-08-25")]

theorem Complex.norm_nat (n : ℕ) :

‖↑n‖ = ↑n

Alias of Complex.norm_natCast.

source

@[deprecated Complex.norm_intCast (since := "2024-08-25")]

theorem Complex.norm_int (n : ℤ) :

‖↑n‖ = |↑n|

Alias of Complex.norm_intCast.

source

@[deprecated Complex.norm_ratCast (since := "2024-08-25")]

theorem Complex.norm_rat (q : ℚ) :

‖↑q‖ = |↑q|

Alias of Complex.norm_ratCast.

source

@[deprecated Complex.nnnorm_natCast (since := "2024-08-25")]

theorem Complex.nnnorm_nat (n : ℕ) :

‖↑n‖₊ = ↑n

Alias of Complex.nnnorm_natCast.

source

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

theorem Complex.abs_intCast (n : ℤ) :

‖↑n‖ = |↑n|

Alias of Complex.norm_intCast.

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

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

source

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

theorem Complex.sq_abs (z : ℂ) :

‖z‖ ^ 2 = normSq z

Alias of Complex.sq_norm.

source

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

source

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

source

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

source

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

source

@[simp]

theorem Complex.range_norm :

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

source

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

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

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

source

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

source

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

theorem Complex.im_le_abs (z : ℂ) :

z.im ≤ ‖z‖

Alias of Complex.im_le_norm.

source

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

source

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

source

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

source

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

source

theorem Complex.norm_le_sqrt_two_mul_max (z : ℂ) :

‖z‖ ≤ √2 * (|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

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

source

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

source

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

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

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

source

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

Instances For

source

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

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

Documentation

Mathlib.Data.Complex.Norm

Norm on the complex numbers #

Cauchy sequences #