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:

• reCLM
• imCLM
• ofRealCLM
• conjCLE

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.

instance Complex.instNormComplex : Norm ℂ

Equations

• Complex.instNormComplex = { norm := ⇑Complex.abs }

@[simp]

theorem Complex.norm_eq_abs (z : ℂ) : ‖z‖ = Complex.abs z

theorem Complex.norm_I : ‖Complex.I‖ = 1

theorem Complex.norm_exp_ofReal_mul_I (t : ℝ) : ‖Complex.exp (↑t * Complex.I)‖ = 1

instance Complex.instNormedAddCommGroupComplex : NormedAddCommGroup ℂ

Equations

• One or more equations did not get rendered due to their size.

instance Complex.instNormedFieldComplex : NormedField ℂ

Equations

• Complex.instNormedFieldComplex = NormedField.mk Complex.instNormedFieldComplex.proof_1 Complex.instNormedFieldComplex.proof_2

instance Complex.instDenselyNormedFieldComplex : DenselyNormedField ℂ

Equations

• Complex.instDenselyNormedFieldComplex = DenselyNormedField.mk Complex.instDenselyNormedFieldComplex.proof_1

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

Equations

• Complex.instNormedAlgebraComplexToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex = NormedAlgebra.mk (_ : ∀ (r : R) (x : ℂ), ‖r • x‖ ≤ ‖r‖ * ‖x‖)

instance NormedSpace.complexToReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] : NormedSpace ℝ E

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

Equations

• NormedSpace.complexToReal = NormedSpace.restrictScalars ℝ ℂ E

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.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.comap_abs_nhds_zero : Filter.comap (⇑Complex.abs) (nhds 0) = nhds 0

theorem Complex.norm_real (r : ℝ) : ‖↑r‖ = ‖r‖

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

theorem Complex.continuous_abs : Continuous ⇑Complex.abs

theorem Complex.continuous_normSq : Continuous ⇑Complex.normSq

@[simp]

theorem Complex.nnnorm_real (r : ℝ) : ‖↑r‖₊ = ‖r‖₊

@[simp]

theorem Complex.nnnorm_nat (n : ℕ) : ‖↑n‖₊ = ↑n

@[simp]

theorem Complex.nnnorm_int (n : ℤ) : ‖↑n‖₊ = ‖n‖₊

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.equivRealProd_apply_le (z : ℂ) : ‖Complex.equivRealProd z‖ ≤ Complex.abs z

theorem Complex.equivRealProd_apply_le' (z : ℂ) : ‖Complex.equivRealProd z‖ ≤ 1 * Complex.abs z

theorem Complex.lipschitz_equivRealProd : LipschitzWith 1 ⇑Complex.equivRealProd

theorem Complex.antilipschitz_equivRealProd : AntilipschitzWith (NNReal.sqrt 2) ⇑Complex.equivRealProd

theorem Complex.uniformEmbedding_equivRealProd : UniformEmbedding ⇑Complex.equivRealProd

instance Complex.instCompleteSpaceComplexToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex : CompleteSpace ℂ

Equations

• Complex.instCompleteSpaceComplexToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex = (_ : CompleteSpace ℂ)

@[simp]

theorem Complex.equivRealProdCLM_apply : ∀ (a : ℂ), Complex.equivRealProdCLM a = (a.re, a.im)

@[simp]

theorem Complex.equivRealProdCLM_symm_apply_im : ∀ (a : ℝ × ℝ), ((ContinuousLinearEquiv.symm Complex.equivRealProdCLM) a).im = a.2

@[simp]

theorem Complex.equivRealProdCLM_symm_apply_re : ∀ (a : ℝ × ℝ), ((ContinuousLinearEquiv.symm Complex.equivRealProdCLM) a).re = a.1

def Complex.equivRealProdCLM : ℂ ≃L[ℝ] ℝ × ℝ

The natural ContinuousLinearEquiv from ℂ to ℝ × ℝ.

Equations

• Complex.equivRealProdCLM = LinearEquiv.toContinuousLinearEquivOfBounds Complex.equivRealProdLm 1 (Real.sqrt 2) Complex.equivRealProd_apply_le' Complex.equivRealProdCLM.proof_2

theorem Complex.equivRealProdCLM_symm_apply (p : ℝ × ℝ) : (ContinuousLinearEquiv.symm Complex.equivRealProdCLM) p = ↑p.1 + ↑p.2 * Complex.I

instance Complex.instProperSpaceComplexToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex : ProperSpace ℂ

Equations

• Complex.instProperSpaceComplexToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplex = (_ : ProperSpace ℂ)

theorem Complex.tendsto_abs_cocompact_atTop : Filter.Tendsto (⇑Complex.abs) (Filter.cocompact ℂ) Filter.atTop

The abs function on ℂ is proper.

theorem Complex.tendsto_normSq_cocompact_atTop : Filter.Tendsto (⇑Complex.normSq) (Filter.cocompact ℂ) Filter.atTop

The normSq function on ℂ is proper.

def Complex.reCLM : ℂ →L[ℝ] ℝ

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

Equations

• Complex.reCLM = LinearMap.mkContinuous Complex.reLm 1 Complex.reCLM.proof_1

theorem Complex.continuous_re : Continuous Complex.re

@[simp]

theorem Complex.reCLM_coe : ↑Complex.reCLM = Complex.reLm

@[simp]

theorem Complex.reCLM_apply (z : ℂ) : Complex.reCLM z = z.re

def Complex.imCLM : ℂ →L[ℝ] ℝ

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

Equations

• Complex.imCLM = LinearMap.mkContinuous Complex.imLm 1 Complex.imCLM.proof_1

theorem Complex.continuous_im : Continuous Complex.im

@[simp]

theorem Complex.imCLM_coe : ↑Complex.imCLM = Complex.imLm

@[simp]

theorem Complex.imCLM_apply (z : ℂ) : Complex.imCLM z = z.im

theorem Complex.restrictScalars_one_smulRight' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (x : E) : ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = ContinuousLinearMap.smulRight Complex.reCLM x + Complex.I • ContinuousLinearMap.smulRight Complex.imCLM x

theorem Complex.restrictScalars_one_smulRight (x : ℂ) : ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = x • 1

def Complex.conjLIE : ℂ ≃ₗᵢ[ℝ] ℂ

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

Equations

• Complex.conjLIE = { toLinearEquiv := AlgEquiv.toLinearEquiv Complex.conjAe, norm_map' := Complex.abs_conj }

@[simp]

theorem Complex.conjLIE_apply (z : ℂ) : Complex.conjLIE z = (starRingEnd ℂ) z

@[simp]

theorem Complex.conjLIE_symm : LinearIsometryEquiv.symm Complex.conjLIE = Complex.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.instContinuousStarComplexToTopologicalSpaceToUniformSpaceToPseudoMetricSpaceToSeminormedRingToSeminormedCommRingToNormedCommRingInstNormedFieldComplexToStarToInvolutiveStarToAddMonoidToAddMonoidWithOneAddGroupWithOneToStarAddMonoidToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingToNonUnitalSeminormedCommRingInstStarRingComplexToNonUnitalNonAssocSemiringToNonUnitalNonAssocCommSemiringToNonUnitalNonAssocCommRingToNonUnitalCommRingCommRing : ContinuousStar ℂ

Equations

• One or more equations did not get rendered due to their size.

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.

def Complex.conjCLE : ℂ ≃L[ℝ] ℂ

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

Equations

• Complex.conjCLE = ContinuousLinearEquiv.mk Complex.conjLIE.toLinearEquiv

@[simp]

theorem Complex.conjCLE_coe : Complex.conjCLE.toLinearEquiv = AlgEquiv.toLinearEquiv Complex.conjAe

@[simp]

theorem Complex.conjCLE_apply (z : ℂ) : Complex.conjCLE z = (starRingEnd ℂ) z

def Complex.ofRealLI : ℝ →ₗᵢ[ℝ] ℂ

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

Equations

• Complex.ofRealLI = { toLinearMap := AlgHom.toLinearMap Complex.ofRealAm, norm_map' := Complex.norm_real }

theorem Complex.isometry_ofReal : Isometry Complex.ofReal'

theorem Complex.continuous_ofReal : Continuous Complex.ofReal'

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

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

def Complex.ofRealCLM : ℝ →L[ℝ] ℂ

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

Equations

• Complex.ofRealCLM = LinearIsometry.toContinuousLinearMap Complex.ofRealLI

@[simp]

theorem Complex.ofRealCLM_coe : ↑Complex.ofRealCLM = AlgHom.toLinearMap Complex.ofRealAm

@[simp]

theorem Complex.ofRealCLM_apply (x : ℝ) : Complex.ofRealCLM x = ↑x

noncomputable instance Complex.instIsROrCComplex : IsROrC ℂ

Equations

• One or more equations did not get rendered due to their size.

theorem IsROrC.re_eq_complex_re : ⇑IsROrC.re = Complex.re

theorem IsROrC.im_eq_complex_im : ⇑IsROrC.im = Complex.im

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

@[simp]

theorem IsROrC.complexRingEquiv_apply {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) (x : 𝕜) : (IsROrC.complexRingEquiv h) x = ↑(IsROrC.re x) + ↑(IsROrC.im x) * Complex.I

@[simp]

theorem IsROrC.complexRingEquiv_symm_apply {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) (x : ℂ) : (RingEquiv.symm (IsROrC.complexRingEquiv h)) x = ↑x.re + ↑x.im * IsROrC.I

def IsROrC.complexRingEquiv {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : 𝕜 ≃+* ℂ

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsROrC.complexLinearIsometryEquiv_apply {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : ∀ (a : 𝕜), (IsROrC.complexLinearIsometryEquiv h) a = (IsROrC.complexRingEquiv h).toEquiv.toFun a

@[simp]

theorem IsROrC.complexLinearIsometryEquiv_toFun {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : ∀ (a : 𝕜), (IsROrC.complexLinearIsometryEquiv h) a = (IsROrC.complexRingEquiv h).toEquiv.toFun a

@[simp]

theorem IsROrC.complexLinearIsometryEquiv_symm_apply {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : ∀ (a : ℂ), (LinearIsometryEquiv.symm (IsROrC.complexLinearIsometryEquiv h)) a = (IsROrC.complexRingEquiv h).toEquiv.invFun a

@[simp]

theorem IsROrC.complexLinearIsometryEquiv_invFun {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : ∀ (a : ℂ), (IsROrC.complexLinearIsometryEquiv h).toLinearEquiv.invFun a = (IsROrC.complexRingEquiv h).toEquiv.invFun a

def IsROrC.complexLinearIsometryEquiv {𝕜 : Type u_2} [IsROrC 𝕜] (h : IsROrC.im IsROrC.I = 1) : 𝕜 ≃ₗᵢ[ℝ] ℂ

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

Equations

• One or more equations did not get rendered due to their size.

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.

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

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

def Complex.slitPlane : Set ℂ

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

Equations

• Complex.slitPlane = {z : ℂ | 0 < z.re ∨ z.im ≠ 0}

theorem Complex.mem_slitPlane_iff {z : ℂ} : z ∈ Complex.slitPlane ↔ 0 < z.re ∨ z.im ≠ 0

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

theorem Complex.isOpen_slitPlane : IsOpen Complex.slitPlane

@[simp]

theorem Complex.ofReal_mem_slitPlane {x : ℝ} : ↑x ∈ Complex.slitPlane ↔ 0 < x

@[simp]

theorem Complex.neg_ofReal_mem_slitPlane {x : ℝ} : -↑x ∈ Complex.slitPlane ↔ x < 0

@[simp]

theorem Complex.one_mem_slitPlane : 1 ∈ Complex.slitPlane

@[simp]

theorem Complex.zero_not_mem_slitPlane : 0 ∉ Complex.slitPlane

@[simp]

theorem Complex.nat_cast_mem_slitPlane {n : ℕ} : ↑n ∈ Complex.slitPlane ↔ n ≠ 0

@[simp]

theorem Complex.ofNat_mem_slitPlane (n : ℕ) [h : Nat.AtLeastTwo n] : OfNat.ofNat n ∈ Complex.slitPlane

theorem Complex.mem_slitPlane_iff_not_le_zero {z : ℂ} : z ∈ Complex.slitPlane ↔ ¬z ≤ 0

theorem Complex.compl_Iic_zero : (Set.Iic 0)ᶜ = Complex.slitPlane

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

theorem Complex.ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ Complex.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 ∈ Complex.slitPlane

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