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`	ℝ →ₗᵢ[ℝ] ℂ	Embedding of the reals 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.

@[implicit_reducible]

instance Complex.instModuleSelf :

A shortcut instance to ensure computability; otherwise we get the noncomputable instance Complex.instNormedField.toNormedModule.toModule.

@[implicit_reducible]

noncomputable instance Complex.instNormedField :

NormedField ℂ

@[implicit_reducible]

noncomputable instance Complex.instDenselyNormedField :

DenselyNormedField ℂ

@[implicit_reducible]

instance Complex.instNormedAlgebraOfReal {R : Type u_1} [NormedField R] [NormedAlgebra R ℝ] :

NormedAlgebra R ℂ

@[implicit_reducible, instance 900]

noncomputable instance NormedSpace.complexToReal {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] :

NormedSpace ℝ E

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

@[implicit_reducible, instance 900]

noncomputable instance NormedAlgebra.complexToReal {A : Type u_2} [SeminormedRing A] [NormedAlgebra ℂ A] :

NormedAlgebra ℝ A

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

@[simp]

theorem Complex.nnnorm_intCast (n : ℤ) :

‖↑n‖₊ = ‖n‖₊

theorem Complex.continuous_normSq :

Continuous ⇑normSq

theorem Complex.nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :

‖ζ‖₊ = 1

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 = ∑ i ∈ s, f i) (hb : ↑b = ∑ i ∈ s, ↑‖f i‖) :

a ≤ b

theorem Complex.equivRealProd_apply_le (z : ℂ) :

‖equivRealProd z‖ ≤ ‖z‖

theorem Complex.equivRealProd_apply_le' (z : ℂ) :

‖equivRealProd z‖ ≤ 1 * ‖z‖

theorem Complex.lipschitz_equivRealProd :

LipschitzWith 1 ⇑equivRealProd

theorem Complex.antilipschitz_equivRealProd :

AntilipschitzWith (NNReal.sqrt 2) ⇑equivRealProd

theorem Complex.isUniformEmbedding_equivRealProd :

IsUniformEmbedding ⇑equivRealProd

instance Complex.instCompleteSpace :

CompleteSpace ℂ

instance Complex.instT2Space :

noncomputable def Complex.equivRealProdCLM :

ℂ ≃L[ℝ ] ℝ × ℝ

The natural ContinuousLinearEquiv from ℂ to ℝ × ℝ.

Instances For

@[simp]

theorem Complex.equivRealProdCLM_symm_apply_re (a✝ : ℝ × ℝ) :

(equivRealProdCLM.symm a✝).re = a✝.1

@[simp]

theorem Complex.equivRealProdCLM_symm_apply_im (a✝ : ℝ × ℝ) :

(equivRealProdCLM.symm a✝).im = a✝.2

@[simp]

theorem Complex.equivRealProdCLM_apply (a✝ : ℂ) :

equivRealProdCLM a✝ = (a✝.re, a✝.im)

theorem Complex.equivRealProdCLM_symm_apply (p : ℝ × ℝ) :

equivRealProdCLM.symm p = ↑p.1 + ↑p.2 * I

instance Complex.instProperSpace :

ProperSpace ℂ

theorem Complex.tendsto_normSq_cocompact_atTop :

Filter.Tendsto (⇑normSq) (Filter.cocompact ℂ) Filter.atTop

The normSq function on ℂ is proper.

noncomputable def Complex.reCLM :

ℂ →L[ℝ ] ℝ

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

Instances For

theorem Complex.continuous_re :

theorem Complex.uniformContinuous_re :

UniformContinuous re

@[deprecated Complex.uniformContinuous_re (since := "2026-02-03")]

theorem Complex.uniformlyContinuous_re :

UniformContinuous re

Alias of Complex.uniformContinuous_re.

@[simp]

theorem Complex.reCLM_coe :

↑reCLM = reLm

@[simp]

theorem Complex.reCLM_apply (z : ℂ) :

reCLM z = z.re

noncomputable def Complex.imCLM :

ℂ →L[ℝ ] ℝ

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

Instances For

theorem Complex.continuous_im :

theorem Complex.uniformContinuous_im :

UniformContinuous im

@[deprecated Complex.uniformContinuous_im (since := "2026-02-03")]

theorem Complex.uniformlyContinuous_im :

UniformContinuous im

Alias of Complex.uniformContinuous_im.

@[simp]

theorem Complex.imCLM_coe :

↑imCLM = imLm

@[simp]

theorem Complex.imCLM_apply (z : ℂ) :

imCLM z = z.im

theorem Complex.restrictScalars_toSpanSingleton' {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (x : E) :

ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) = reCLM.smulRight x + I • imCLM.smulRight x

theorem Complex.restrictScalars_toSpanSingleton (x : ℂ) :

ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) = x • 1

@[deprecated Complex.restrictScalars_toSpanSingleton' (since := "2025-12-18")]

theorem Complex.restrictScalars_one_smulRight' {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (x : E) :

ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) = reCLM.smulRight x + I • imCLM.smulRight x

Alias of Complex.restrictScalars_toSpanSingleton'.

@[deprecated Complex.restrictScalars_toSpanSingleton (since := "2025-12-18")]

theorem Complex.restrictScalars_one_smulRight (x : ℂ) :

ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.toSpanSingleton ℂ x) = x • 1

Alias of Complex.restrictScalars_toSpanSingleton.

def Complex.conjLIE :

ℂ ≃ₗᵢ[ℝ ] ℂ

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

Instances For

@[simp]

theorem Complex.conjLIE_apply (z : ℂ) :

conjLIE z = (starRingEnd ℂ) z

@[simp]

theorem Complex.conjLIE_symm :

conjLIE.symm = conjLIE

theorem Complex.isometry_conj :

Isometry ⇑(starRingEnd ℂ)

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

instance Complex.instContinuousStar :

ContinuousStar ℂ

theorem Complex.continuous_conj :

Continuous ⇑(starRingEnd ℂ)

theorem Complex.ringHom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : Continuous ⇑f) :

f = RingHom.id ℂ ∨ f = starRingEnd ℂ

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

noncomputable def Complex.conjCAE :

ℂ ≃A[ℝ ] ℂ

The complex-conjugation function from ℂ to itself is a continuous ℝ-algebra isomorphism.

Instances For

@[reducible, inline]

noncomputable abbrev Complex.conjCLE :

ℂ ≃L[ℝ ] ℂ

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

This is an abbreviation for conjCAE coerced to a continuous linear map.

Instances For

@[simp]

theorem Complex.conjLIE_toCLE :

conjLIE.toContinuousLinearEquiv = conjCLE

@[simp]

theorem Complex.conjCAE_toAlgEquiv :

conjCAE.toAlgEquiv = conjAe

@[simp]

theorem Complex.conjCLE_toLinearEquiv :

conjCLE.toLinearEquiv = conjAe.toLinearEquiv

@[simp]

theorem Complex.conjCLE_coe_toLinearMap :

↑↑conjCLE = conjAe.toLinearMap

@[simp]

theorem Complex.conjCAE_apply (z : ℂ) :

conjCAE z = (starRingEnd ℂ) z

theorem Complex.conjCLE_apply (z : ℂ) :

conjCLE z = (starRingEnd ℂ) z

@[simp]

theorem Complex.conjCAE_toLinearMap :

conjCAE.toLinearMap = conjAe.toLinearMap

def Complex.ofRealLI :

ℝ →ₗᵢ[ℝ ] ℂ

Linear isometry version of the canonical embedding of ℝ in ℂ.

Instances For

@[simp]

theorem Complex.ofRealLI_apply (x : ℝ) :

ofRealLI x = ↑x

theorem Complex.isometry_ofReal :

Isometry ofReal

theorem Complex.continuous_ofReal :

Continuous ofReal

theorem Complex.isUniformEmbedding_ofReal :

IsUniformEmbedding ofReal

theorem RCLike.isUniformEmbedding_ofReal {𝕜 : Type u_2} [RCLike 𝕜] :

IsUniformEmbedding ofReal

theorem Filter.tendsto_ofReal_iff {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ} :

Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x) ↔ Tendsto f l (nhds x)

theorem Filter.tendsto_ofReal_iff' {α : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {l : Filter α} {f : α → ℝ} {x : ℝ} :

Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x) ↔ Tendsto f l (nhds x)

theorem Filter.Tendsto.ofReal {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ} (hf : Tendsto f l (nhds x)) :

Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x)

theorem Complex.ringHom_eq_ofReal_of_continuous {f : ℝ →+* ℂ} (h : Continuous ⇑f) :

The only continuous ring homomorphism from ℝ to ℂ is the identity.

noncomputable def Complex.ofRealCLM :

ℝ →L[ℝ ] ℂ

Continuous linear map version of the canonical embedding of ℝ in ℂ.

Instances For

@[simp]

theorem Complex.ofRealCLM_coe :

↑ofRealCLM = ofRealAm.toLinearMap

@[simp]

theorem Complex.ofRealCLM_apply (x : ℝ) :

ofRealCLM x = ↑x

@[implicit_reducible]

noncomputable instance Complex.instRCLike :

theorem RCLike.re_eq_complex_re :

⇑re = Complex.re

theorem RCLike.im_eq_complex_im :

⇑im = Complex.im

theorem RCLike.ofReal_eq_complex_ofReal :

ofReal = Complex.ofReal

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) :

z⁻¹ = (starRingEnd ℂ) z

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

theorem Complex.im_eq_zero_iff_isSelfAdjoint (x : ℂ) :

x.im = 0 ↔ IsSelfAdjoint x

theorem Complex.re_eq_ofReal_of_isSelfAdjoint {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) :

x.re = y ↔ x = ↑y

theorem Complex.ofReal_eq_re_of_isSelfAdjoint {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) :

y = x.re ↔ ↑y = x

def RCLike.complexRingEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) :

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

Instances For

@[simp]

theorem RCLike.complexRingEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (x : 𝕜) :

(complexRingEquiv h) x = ↑(re x) + ↑(im x) * Complex.I

@[simp]

theorem RCLike.complexRingEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (x : ℂ) :

(complexRingEquiv h).symm x = ↑x.re + ↑x.im * I

theorem RCLike.map_nonneg_iff {𝕜 : Type u_2} {𝕜' : Type u_3} [RCLike 𝕜] [RCLike 𝕜'] (h : im I = 1) {a : 𝕜} :

0 ≤ (map 𝕜 𝕜') a ↔ 0 ≤ a

@[simp]

theorem RCLike.to_complex_nonneg_iff {𝕜 : Type u_2} [RCLike 𝕜] {a : 𝕜} :

0 ≤ ↑(re a) + ↑(im a) * Complex.I ↔ 0 ≤ a

def RCLike.complexLinearIsometryEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) :

𝕜 ≃ₗᵢ[ℝ ] ℂ

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

Instances For

@[simp]

theorem RCLike.complexLinearIsometryEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (a✝ : ℂ) :

(complexLinearIsometryEquiv h).symm a✝ = (complexRingEquiv h).invFun a✝

@[simp]

theorem RCLike.complexLinearIsometryEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (a✝ : 𝕜) :

(complexLinearIsometryEquiv h) a✝ = (complexRingEquiv h).toFun a✝

@[simp]

theorem RCLike.toContinuousLinearMap_complexLinearIsometryEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) :

↑(complexLinearIsometryEquiv h).toContinuousLinearEquiv = map 𝕜 ℂ

@[simp]

theorem RCLike.norm_to_complex {𝕜 : Type u_2} [RCLike 𝕜] (a : 𝕜) :

‖↑(re a) + ↑(im a) * Complex.I‖ = ‖a‖

theorem Complex.isometry_intCast :

Isometry Int.cast

theorem Complex.closedEmbedding_intCast :

Topology.IsClosedEmbedding Int.cast

theorem Complex.isClosed_range_intCast :

IsClosed (Set.range Int.cast)

theorem Complex.isOpen_compl_range_intCast :

IsOpen (Set.range Int.cast)ᶜ

theorem Complex.eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) :

z = ↑‖z‖

theorem Complex.orderClosedTopology :

OrderClosedTopology ℂ

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

theorem Complex.norm_of_nonneg' {x : ℂ} (hx : 0 ≤ x) :

↑‖x‖ = x

theorem Complex.re_nonneg_iff_nonneg {x : ℂ} (hx : IsSelfAdjoint x) :

0 ≤ x.re ↔ 0 ≤ x

theorem Complex.re_le_re {x y : ℂ} (h : x ≤ y) :

@[simp]

theorem RCLike.re_to_complex {x : ℂ} :

re x = x.re

@[simp]

theorem RCLike.im_to_complex {x : ℂ} :

im x = x.im

@[simp]

theorem RCLike.I_to_complex :

@[simp]

theorem RCLike.normSq_to_complex {x : ℂ} :

normSq x = Complex.normSq x

@[simp]

theorem RCLike.hasSum_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} :

HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) x L ↔ HasSum f ((starRingEnd 𝕜) x) L

theorem RCLike.hasSum_conj' {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} :

HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) ((starRingEnd 𝕜) x) L ↔ HasSum f x L

@[simp]

theorem RCLike.summable_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} :

Summable (fun (x : α) => (starRingEnd 𝕜) (f x)) L ↔ Summable f L

theorem RCLike.conj_tsum {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) :

(starRingEnd 𝕜) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd 𝕜) (f a)

@[simp]

theorem RCLike.hasSum_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ} {x : ℝ} :

HasSum (fun (x : α) => ↑(f x)) (↑x) L ↔ HasSum f x L

@[simp]

theorem RCLike.summable_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ} :

Summable (fun (x : α) => ↑(f x)) L ↔ Summable f L

theorem RCLike.ofReal_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} (f : α → ℝ) :

↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)

theorem RCLike.hasSum_re {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} (h : HasSum f x L) :

HasSum (fun (x : α) => re (f x)) (re x) L

theorem RCLike.hasSum_im {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} (h : HasSum f x L) :

HasSum (fun (x : α) => im (f x)) (im x) L

theorem RCLike.re_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜} (h : Summable f L) :

re (∑'[L] (a : α), f a) = ∑'[L] (a : α), re (f a)

theorem RCLike.im_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜} (h : Summable f L) :

im (∑'[L] (a : α), f a) = ∑'[L] (a : α), im (f a)

theorem RCLike.hasSum_iff {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) (c : 𝕜) :

HasSum f c L ↔ HasSum (fun (x : α) => re (f x)) (re c) L ∧ HasSum (fun (x : α) => im (f x)) (im c) L

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} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} :

HasSum (fun (x : α) => (starRingEnd ℂ) (f x)) x L ↔ HasSum f ((starRingEnd ℂ) x) L

theorem Complex.hasSum_conj' {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} :

HasSum (fun (x : α) => (starRingEnd ℂ) (f x)) ((starRingEnd ℂ) x) L ↔ HasSum f x L

theorem Complex.summable_conj {α : Type u_1} {f : α → ℂ} :

(Summable fun (x : α) => (starRingEnd ℂ) (f x)) ↔ Summable f

theorem Complex.conj_tsum {α : Type u_1} {L : SummationFilter α} (f : α → ℂ) :

(starRingEnd ℂ) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd ℂ) (f a)

@[simp]

theorem Complex.hasSum_ofReal {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {x : ℝ} :

HasSum (fun (x : α) => ↑(f x)) (↑x) L ↔ HasSum f x L

@[simp]

theorem Complex.summable_ofReal {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} :

Summable (fun (x : α) => ↑(f x)) L ↔ Summable f L

theorem Complex.ofReal_tsum {α : Type u_1} {L : SummationFilter α} (f : α → ℝ) :

↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)

theorem Complex.hasSum_re {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} (h : HasSum f x L) :

HasSum (fun (x : α) => (f x).re) x.re L

theorem Complex.hasSum_im {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} (h : HasSum f x L) :

HasSum (fun (x : α) => (f x).im) x.im L

theorem Complex.re_tsum {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ} (h : Summable f L) :

(∑'[L] (a : α), f a).re = ∑'[L] (a : α), (f a).re

theorem Complex.im_tsum {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ} (h : Summable f L) :

(∑'[L] (a : α), f a).im = ∑'[L] (a : α), (f a).im

theorem Complex.hasSum_iff {α : Type u_1} {L : SummationFilter α} (f : α → ℂ) (c : ℂ) :

HasSum f c L ↔ HasSum (fun (x : α) => (f x).re) c.re L ∧ HasSum (fun (x : α) => (f x).im) c.im L

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

def Complex.slitPlane :

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

Instances For

theorem Complex.mem_slitPlane_iff {z : ℂ} :

z ∈ slitPlane ↔ 0 < z.re ∨ z.im ≠ 0

theorem Complex.mem_slitPlane_or_neg_mem_slitPlane {z : ℂ} (hz : z ≠ 0) :

z ∈ slitPlane ∨ -z ∈ slitPlane

theorem Complex.slitPlane_eq_union :

slitPlane = {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0}

theorem Complex.isOpen_slitPlane :

IsOpen slitPlane

@[simp]

theorem Complex.ofReal_mem_slitPlane {x : ℝ} :

↑x ∈ slitPlane ↔ 0 < x

@[simp]

theorem Complex.neg_ofReal_mem_slitPlane {x : ℝ} :

-↑x ∈ slitPlane ↔ x < 0

@[simp]

theorem Complex.one_mem_slitPlane :

1 ∈ slitPlane

@[simp]

theorem Complex.zero_notMem_slitPlane :

0 ∉ slitPlane

@[simp]

theorem Complex.natCast_mem_slitPlane {n : ℕ} :

↑n ∈ slitPlane ↔ n ≠ 0

@[simp]

theorem Complex.ofNat_mem_slitPlane (n : ℕ) [n.AtLeastTwo] :

OfNat.ofNat n ∈ slitPlane

theorem Complex.mem_slitPlane_iff_not_le_zero {z : ℂ} :

z ∈ slitPlane ↔ ¬z ≤ 0

theorem Complex.compl_Iic_zero :

(Set.Iic 0)ᶜ = slitPlane

theorem Complex.slitPlane_ne_zero {z : ℂ} (hz : z ∈ slitPlane) :

z ≠ 0

theorem Complex.ball_one_subset_slitPlane :

Metric.ball 1 1 ⊆ slitPlane

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

theorem Complex.mem_slitPlane_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) :

1 + z ∈ slitPlane

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

theorem Complex.subset_slitPlane_iff_of_subset_sphere {r : ℝ} {s : Set ℂ} (hs : s ⊆ Metric.sphere 0 r) :

s ⊆ slitPlane ↔ -↑r ∉ s

A subset of the circle centered at the origin in ℂ of radius r is a subset of the slitPlane if it does not contain -r.

theorem IsCompact.reProdIm {s t : Set ℝ} (hs : IsCompact s) (ht : IsCompact t) :

IsCompact (s ×ℂ t)

theorem realPart.norm_le {A : Type u_1} [SeminormedAddCommGroup A] [StarAddMonoid A] [NormedSpace ℂ A] [StarModule ℂ A] [NormedStarGroup A] (x : A) :

‖realPart x‖ ≤ ‖x‖

theorem imaginaryPart.norm_le {A : Type u_1} [SeminormedAddCommGroup A] [StarAddMonoid A] [NormedSpace ℂ A] [StarModule ℂ A] [NormedStarGroup A] (x : A) :

‖imaginaryPart x‖ ≤ ‖x‖