Documentation

Mathlib.Analysis.Complex.Basic

Normed space structure on . #

This file gathers basic facts of analytic nature on the complex numbers.

Main results #

This file registers as a normed field, expresses basic properties of the norm, and gives tools on the real vector space structure of . Notably, it defines the following functions in the namespace Complex.

Name Type Description
equivRealProdCLM ℂ ≃L[ℝ] ℝ × ℝ The natural ContinuousLinearEquiv from to ℝ × ℝ
reCLM ℂ →L[ℝ] ℝ Real part function as a ContinuousLinearMap
imCLM ℂ →L[ℝ] ℝ Imaginary part function as a ContinuousLinearMap
ofRealCLM ℝ →L[ℝ] ℂ Embedding of the reals as a ContinuousLinearMap
ofRealLI ℝ →ₗᵢ[ℝ] ℂ Complex conjugation as a LinearIsometry
conjCLE ℂ ≃L[ℝ] ℂ Complex conjugation as a ContinuousLinearEquiv
conjLIE ℂ ≃ₗᵢ[ℝ] ℂ Complex conjugation as a LinearIsometryEquiv

We also register the fact that is an RCLike field.

Equations
@[simp]
theorem Complex.norm_eq_abs (z : ) :
z = Complex.abs z
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[instance 900]

The module structure from Module.complexToReal is a normed space.

Equations
@[instance 900]

The algebra structure from Algebra.complexToReal is a normed algebra.

Equations
theorem Complex.dist_eq (z : ) (w : ) :
dist z w = Complex.abs (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
@[simp]
theorem Complex.norm_rat (r : ) :
r = |r|
@[simp]
theorem Complex.norm_nat (n : ) :
n = n
@[simp]
theorem Complex.norm_int {n : } :
n = |n|
theorem Complex.norm_int_of_nonneg {n : } (hn : 0 n) :
n = n
theorem Complex.normSq_eq_norm_sq (z : ) :
Complex.normSq z = z ^ 2
@[simp]
@[simp]
theorem Complex.nnnorm_nat (n : ) :
n‖₊ = n
@[simp]
theorem Complex.nnnorm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
theorem Complex.norm_eq_one_of_pow_eq_one {ζ : } {n : } (h : ζ ^ n = 1) (hn : n 0) :
ζ = 1
theorem Complex.le_of_eq_sum_of_eq_sum_norm {ι : Type u_2} {a : } {b : } (f : ι) (s : Finset ι) (ha₀ : 0 a) (ha : a = is, f i) (hb : b = is, f i) :
a b
theorem Complex.equivRealProd_apply_le (z : ) :
Complex.equivRealProd z Complex.abs z
theorem Complex.equivRealProd_apply_le' (z : ) :
Complex.equivRealProd z 1 * Complex.abs z
@[simp]
theorem Complex.equivRealProdCLM_apply :
∀ (a : ), Complex.equivRealProdCLM a = (a.re, a.im)

The abs function on is proper.

The normSq function on is proper.

Continuous linear map version of the real part function, from to .

Equations
Instances For
    @[simp]
    theorem Complex.reCLM_apply (z : ) :
    Complex.reCLM z = z.re

    Continuous linear map version of the imaginary part function, from to .

    Equations
    Instances For
      @[simp]
      theorem Complex.imCLM_apply (z : ) :
      Complex.imCLM z = z.im

      The complex-conjugation function from to itself is an isometric linear equivalence.

      Equations
      Instances For
        @[simp]
        theorem Complex.conjLIE_apply (z : ) :
        Complex.conjLIE z = (starRingEnd ) z
        @[simp]
        theorem Complex.dist_conj_conj (z : ) (w : ) :
        @[simp]

        The only continuous ring homomorphisms from to are the identity and the complex conjugation.

        Continuous linear equiv version of the conj function, from to .

        Equations
        Instances For
          @[simp]
          theorem Complex.conjCLE_coe :
          Complex.conjCLE.toLinearEquiv = Complex.conjAe.toLinearEquiv
          @[simp]
          theorem Complex.conjCLE_apply (z : ) :
          Complex.conjCLE z = (starRingEnd ) z

          Linear isometry version of the canonical embedding of in .

          Equations
          Instances For
            theorem Filter.Tendsto.ofReal {α : Type u_2} {l : Filter α} {f : α} {x : } (hf : Filter.Tendsto f l (nhds x)) :
            Filter.Tendsto (fun (x : α) => (f x)) l (nhds x)

            The only continuous ring homomorphism from to is the identity.

            Continuous linear map version of the canonical embedding of in .

            Equations
            Instances For
              @[simp]
              theorem Complex.ofRealCLM_apply (x : ) :
              Complex.ofRealCLM x = x
              noncomputable instance Complex.instRCLike :
              Equations
              • One or more equations did not get rendered due to their size.
              theorem Complex.mul_conj' (z : ) :
              z * (starRingEnd ) z = z ^ 2
              theorem Complex.conj_mul' (z : ) :
              (starRingEnd ) z * z = z ^ 2
              theorem Complex.inv_eq_conj {z : } (hz : z = 1) :
              theorem Complex.exists_norm_eq_mul_self (z : ) :
              ∃ (c : ), c = 1 z = c * z
              theorem Complex.exists_norm_mul_eq_self (z : ) :
              ∃ (c : ), c = 1 c * z = z
              @[simp]
              theorem RCLike.complexRingEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (x : 𝕜) :
              (RCLike.complexRingEquiv h) x = (RCLike.re x) + (RCLike.im x) * Complex.I
              @[simp]
              theorem RCLike.complexRingEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) (x : ) :
              (RCLike.complexRingEquiv h).symm x = x.re + x.im * RCLike.I
              def RCLike.complexRingEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :
              𝕜 ≃+*

              The natural isomorphism between 𝕜 satisfying RCLike 𝕜 and when RCLike.im RCLike.I = 1.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem RCLike.complexLinearIsometryEquiv_invFun {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :
                ∀ (a : ), (RCLike.complexLinearIsometryEquiv h).invFun a = (RCLike.complexRingEquiv h).invFun a
                @[simp]
                theorem RCLike.complexLinearIsometryEquiv_toFun {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :
                @[simp]
                theorem RCLike.complexLinearIsometryEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :
                @[simp]
                theorem RCLike.complexLinearIsometryEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :
                def RCLike.complexLinearIsometryEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : RCLike.im RCLike.I = 1) :

                The natural -linear isometry equivalence between 𝕜 satisfying RCLike 𝕜 and when RCLike.im RCLike.I = 1.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Complex.eq_coe_norm_of_nonneg {z : } (hz : 0 z) :
                  z = z

                  We show that the partial order and the topology on are compatible. We turn this into an instance scoped to ComplexOrder.

                  @[simp]
                  theorem RCLike.re_to_complex {x : } :
                  RCLike.re x = x.re
                  @[simp]
                  theorem RCLike.im_to_complex {x : } :
                  RCLike.im x = x.im
                  @[simp]
                  theorem RCLike.I_to_complex :
                  RCLike.I = Complex.I
                  @[simp]
                  theorem RCLike.normSq_to_complex {x : } :
                  RCLike.normSq x = Complex.normSq x
                  @[simp]
                  theorem RCLike.hasSum_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} {x : 𝕜} :
                  HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) x HasSum f ((starRingEnd 𝕜) x)
                  theorem RCLike.hasSum_conj' {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} {x : 𝕜} :
                  HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) ((starRingEnd 𝕜) x) HasSum f x
                  @[simp]
                  theorem RCLike.summable_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} :
                  (Summable fun (x : α) => (starRingEnd 𝕜) (f x)) Summable f
                  theorem RCLike.conj_tsum {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (f : α𝕜) :
                  (starRingEnd 𝕜) (∑' (a : α), f a) = ∑' (a : α), (starRingEnd 𝕜) (f a)
                  @[simp]
                  theorem RCLike.hasSum_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α} {x : } :
                  HasSum (fun (x : α) => (f x)) x HasSum f x
                  @[simp]
                  theorem RCLike.summable_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α} :
                  (Summable fun (x : α) => (f x)) Summable f
                  theorem RCLike.ofReal_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] (f : α) :
                  (∑' (a : α), f a) = ∑' (a : α), (f a)
                  theorem RCLike.hasSum_re {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} {x : 𝕜} (h : HasSum f x) :
                  HasSum (fun (x : α) => RCLike.re (f x)) (RCLike.re x)
                  theorem RCLike.hasSum_im {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} {x : 𝕜} (h : HasSum f x) :
                  HasSum (fun (x : α) => RCLike.im (f x)) (RCLike.im x)
                  theorem RCLike.re_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} (h : Summable f) :
                  RCLike.re (∑' (a : α), f a) = ∑' (a : α), RCLike.re (f a)
                  theorem RCLike.im_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {f : α𝕜} (h : Summable f) :
                  RCLike.im (∑' (a : α), f a) = ∑' (a : α), RCLike.im (f a)
                  theorem RCLike.hasSum_iff {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] (f : α𝕜) (c : 𝕜) :
                  HasSum f c HasSum (fun (x : α) => RCLike.re (f x)) (RCLike.re c) HasSum (fun (x : α) => RCLike.im (f x)) (RCLike.im c)

                  We have to repeat the lemmas about RCLike.re and RCLike.im as they are not syntactic matches for Complex.re and Complex.im.

                  We do not have this problem with ofReal and conj, although we repeat them anyway for discoverability and to avoid the need to unify 𝕜.

                  theorem Complex.hasSum_conj {α : Type u_1} {f : α} {x : } :
                  HasSum (fun (x : α) => (starRingEnd ) (f x)) x HasSum f ((starRingEnd ) x)
                  theorem Complex.hasSum_conj' {α : Type u_1} {f : α} {x : } :
                  HasSum (fun (x : α) => (starRingEnd ) (f x)) ((starRingEnd ) x) HasSum f x
                  theorem Complex.summable_conj {α : Type u_1} {f : α} :
                  (Summable fun (x : α) => (starRingEnd ) (f x)) Summable f
                  theorem Complex.conj_tsum {α : Type u_1} (f : α) :
                  (starRingEnd ) (∑' (a : α), f a) = ∑' (a : α), (starRingEnd ) (f a)
                  @[simp]
                  theorem Complex.hasSum_ofReal {α : Type u_1} {f : α} {x : } :
                  HasSum (fun (x : α) => (f x)) x HasSum f x
                  @[simp]
                  theorem Complex.summable_ofReal {α : Type u_1} {f : α} :
                  (Summable fun (x : α) => (f x)) Summable f
                  theorem Complex.ofReal_tsum {α : Type u_1} (f : α) :
                  (∑' (a : α), f a) = ∑' (a : α), (f a)
                  theorem Complex.hasSum_re {α : Type u_1} {f : α} {x : } (h : HasSum f x) :
                  HasSum (fun (x : α) => (f x).re) x.re
                  theorem Complex.hasSum_im {α : Type u_1} {f : α} {x : } (h : HasSum f x) :
                  HasSum (fun (x : α) => (f x).im) x.im
                  theorem Complex.re_tsum {α : Type u_1} {f : α} (h : Summable f) :
                  (∑' (a : α), f a).re = ∑' (a : α), (f a).re
                  theorem Complex.im_tsum {α : Type u_1} {f : α} (h : Summable f) :
                  (∑' (a : α), f a).im = ∑' (a : α), (f a).im
                  theorem Complex.hasSum_iff {α : Type u_1} (f : α) (c : ) :
                  HasSum f c HasSum (fun (x : α) => (f x).re) c.re HasSum (fun (x : α) => (f x).im) c.im

                  Define the "slit plane" ℂ ∖ ℝ≤0 and provide some API #

                  The slit plane is the complex plane with the closed negative real axis removed.

                  Equations
                  Instances For
                    theorem Complex.slitPlane_eq_union :
                    Complex.slitPlane = {z : | 0 < z.re} {z : | z.im 0}
                    @[deprecated Complex.natCast_mem_slitPlane]

                    Alias of Complex.natCast_mem_slitPlane.

                    The slit plane includes the open unit ball of radius 1 around 1.

                    The slit plane includes the open unit ball of radius 1 around 1.