Documentation

Mathlib.Analysis.Complex.Basic

Normed space structure on . #

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

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, in the namespace Complex, it defines functions:

They are bundled versions of the real part, the imaginary part, the embedding of in , and the complex conjugate as continuous -linear maps. The last two are also bundled as linear isometries in ofRealLi and conjLie.

We also register the fact that is an IsROrC field.

@[simp]

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

theorem Complex.dist_eq (z : ) (w : ) :
dist z w = Complex.abs (z - w)
theorem Complex.dist_eq_re_im (z : ) (w : ) :
dist z w = Real.sqrt ((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₂ } = Real.sqrt ((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.dist_self_conj (z : ) :
dist z (↑(starRingEnd ) z) = 2 * |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
@[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
@[simp]
theorem Complex.equivRealProdClm_apply :
∀ (a : ), Complex.equivRealProdClm a = (a.re, a.im)

The natural ContinuousLinearEquiv from to ℝ × ℝ.

Instances For

    The abs function on is proper.

    The normSq function on is proper.

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

    Instances For
      @[simp]
      theorem Complex.reClm_apply (z : ) :
      Complex.reClm z = z.re

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

      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.

        Instances For
          @[simp]
          @[simp]
          theorem Complex.dist_conj_conj (z : ) (w : ) :
          dist (↑(starRingEnd ) z) (↑(starRingEnd ) w) = dist z w
          @[simp]
          theorem Complex.nndist_conj_conj (z : ) (w : ) :
          nndist (↑(starRingEnd ) z) (↑(starRingEnd ) w) = nndist z w
          theorem Complex.dist_conj_comm (z : ) (w : ) :
          dist (↑(starRingEnd ) z) w = dist z (↑(starRingEnd ) w)
          theorem Complex.nndist_conj_comm (z : ) (w : ) :
          nndist (↑(starRingEnd ) z) w = nndist z (↑(starRingEnd ) w)

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

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

          Instances For
            @[simp]

            Linear isometry version of the canonical embedding of in .

            Instances For

              The only continuous ring homomorphism from to is the identity.

              Continuous linear map version of the canonical embedding of in .

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

                We have to repeat the lemmas about IsROrC.re and IsROrC.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