Documentation

Mathlib.Data.Complex.Norm

Norm on the complex numbers #

source
instance Complex.instNorm :
Norm ℂ
Equations
source
@[simp]
theorem Complex.norm_eq_abs (z : ℂ) :
‖z‖ = abs z
source
theorem Complex.norm_I :
‖I‖ = 1
source
instance Complex.instNormedAddCommGroup :
NormedAddCommGroup ℂ
Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem Complex.nnnorm_I :
‖I‖₊ = 1
source
theorem Complex.dist_eq (z w : ℂ) :
dist z w = abs (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
source
@[simp]
theorem Complex.norm_real (r : ℝ) :
‖↑r‖ = ‖r‖
source
@[simp]
theorem Complex.norm_natCast (n : ℕ) :
‖↑n‖ = ↑n
source
@[simp]
theorem Complex.norm_intCast (n : ℤ) :
‖↑n‖ = |↑n|
source
@[simp]
theorem Complex.norm_ratCast (q : ℚ) :
‖↑q‖ = |↑q|
source
@[simp]
theorem Complex.nnnorm_real (r : ℝ) :
‖↑r‖₊ = ‖r‖₊
source
@[simp]
theorem Complex.nnnorm_natCast (n : ℕ) :
‖↑n‖₊ = ↑n
source
@[simp]
theorem Complex.nnnorm_ratCast (q : ℚ) :
‖↑q‖₊ = ‖↑q‖₊
source
@[simp]
theorem Complex.norm_ofNat (n : ℕ) [n.AtLeastTwo] :
‖OfNat.ofNat n‖ = OfNat.ofNat n
source
@[simp]
theorem Complex.nnnorm_ofNat (n : ℕ) [n.AtLeastTwo] :
‖OfNat.ofNat n‖₊ = OfNat.ofNat n
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
@[simp]
theorem Complex.norm_nnratCast (q : ℚ≥0) :
‖↑q‖ = ↑q
source
@[simp]
theorem Complex.nnnorm_nnratCast (q : ℚ≥0) :
‖↑q‖₊ = ↑q
source
theorem Complex.norm_int_of_nonneg {n : ℤ} (hn : 0 ≤ n) :
‖↑n‖ = ↑n
source
theorem Complex.normSq_eq_norm_sq (z : ℂ) :
normSq z = ‖z‖ ^ 2