Documentation

Mathlib.Data.Complex.Norm

Norm on the complex numbers #

source
instance Complex.instNorm :
Norm ℂ
Equations
    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
      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
        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_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 * 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
          @[deprecated Complex.norm_le_sqrt_two_mul_max (since := "2025-02-16")]
          theorem Complex.abs_le_sqrt_two_mul_max (z : ℂ) :
          ‖z‖ ≤ √2 * max |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
            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
                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
                    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
                        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
                            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
                                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