The complex numbers

The complex numbers are modelled as ℝ^2 in the obvious way and it is shown that they form a field of characteristic zero. The result that the complex numbers are algebraically closed, see FieldTheory.AlgebraicClosure.

Definition and basic arithmetic

structure Complex : Type

• re : ℝ
• im : ℝ

Complex numbers consist of two Reals: a real part re and an imaginary part im.

def termℂ : Lean.ParserDescr

Equations

• termℂ = Lean.ParserDescr.node `termℂ 1024 (Lean.ParserDescr.symbol "ℂ")

noncomputable instance Complex.instDecidableEqComplex : DecidableEq ℂ

Equations

• Complex.instDecidableEqComplex = Classical.decEq ℂ

@[simp]

theorem Complex.equivRealProd_apply (z : ℂ) : ↑Complex.equivRealProd z = (z.re, z.im)

def Complex.equivRealProd : ℂ ≃ ℝ × ℝ

The equivalence between the complex numbers and ℝ × ℝ.

Equations

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

@[simp]

theorem Complex.eta (z : ℂ) : { re := z.re, im := z.im } = z

theorem Complex.ext {z : ℂ} {w : ℂ} : z.re = w.re → z.im = w.im → z = w

theorem Complex.ext_iff {z : ℂ} {w : ℂ} : z = w ↔ z.re = w.re ∧ z.im = w.im

theorem Complex.re_surjective : Function.Surjective Complex.re

theorem Complex.im_surjective : Function.Surjective Complex.im

@[simp]

theorem Complex.range_re : Set.range Complex.re = Set.univ

@[simp]

theorem Complex.range_im : Set.range Complex.im = Set.univ

def Complex.ofReal' (r : ℝ) : ℂ

The natural inclusion of the real numbers into the complex numbers. The name Complex.ofReal is reserved for the bundled homomorphism.

Equations

• ↑r = { re := r, im := 0 }

instance Complex.instCoeRealComplex : Coe ℝ ℂ

Equations

• Complex.instCoeRealComplex = { coe := Complex.ofReal' }

@[simp]

theorem Complex.ofReal_re (r : ℝ) : (↑r).re = r

@[simp]

theorem Complex.ofReal_im (r : ℝ) : (↑r).im = 0

theorem Complex.ofReal_def (r : ℝ) : ↑r = { re := r, im := 0 }

@[simp]

theorem Complex.ofReal_inj {z : ℝ} {w : ℝ} : ↑z = ↑w ↔ z = w

theorem Complex.ofReal_injective : Function.Injective Complex.ofReal'

instance Complex.canLift : CanLift ℂ ℝ Complex.ofReal' fun z => z.im = 0

Equations

• Complex.canLift = Complex.canLift.proof_1

def Complex.Set.reProdIm (s : Set ℝ) (t : Set ℝ) : Set ℂ

The product of a set on the real axis and a set on the imaginary axis of the complex plane, denoted by s ×ℂ t.

Equations

• s ×ℂ t = Complex.re ⁻¹' s ∩ Complex.im ⁻¹' t

def Complex.«term_×ℂ_» : Lean.TrailingParserDescr

Equations

• Complex.«term_×ℂ_» = Lean.ParserDescr.trailingNode `Complex.term_×ℂ_ 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ℂ ") (Lean.ParserDescr.cat `term 73))

theorem Complex.mem_reProdIm {z : ℂ} {s : Set ℝ} {t : Set ℝ} : z ∈ s ×ℂ t ↔ z.re ∈ s ∧ z.im ∈ t

instance Complex.instZeroComplex : Zero ℂ

Equations

• Complex.instZeroComplex = { zero := ↑0 }

instance Complex.instInhabitedComplex : Inhabited ℂ

Equations

• Complex.instInhabitedComplex = { default := 0 }

@[simp]

theorem Complex.zero_re : 0.re = 0

@[simp]

theorem Complex.zero_im : 0.im = 0

@[simp]

theorem Complex.ofReal_zero : ↑0 = 0

@[simp]

theorem Complex.ofReal_eq_zero {z : ℝ} : ↑z = 0 ↔ z = 0

theorem Complex.ofReal_ne_zero {z : ℝ} : ↑z ≠ 0 ↔ z ≠ 0

instance Complex.instOneComplex : One ℂ

Equations

• Complex.instOneComplex = { one := ↑1 }

@[simp]

theorem Complex.one_re : 1.re = 1

@[simp]

theorem Complex.one_im : 1.im = 0

@[simp]

theorem Complex.ofReal_one : ↑1 = 1

@[simp]

theorem Complex.ofReal_eq_one {z : ℝ} : ↑z = 1 ↔ z = 1

theorem Complex.ofReal_ne_one {z : ℝ} : ↑z ≠ 1 ↔ z ≠ 1

instance Complex.instAddComplex : Add ℂ

Equations

• Complex.instAddComplex = { add := fun z w => { re := z.re + w.re, im := z.im + w.im } }

@[simp]

theorem Complex.add_re (z : ℂ) (w : ℂ) : (z + w).re = z.re + w.re

@[simp]

theorem Complex.add_im (z : ℂ) (w : ℂ) : (z + w).im = z.im + w.im

@[simp]

theorem Complex.bit0_re (z : ℂ) : (bit0 z).re = bit0 z.re

@[simp]

theorem Complex.bit1_re (z : ℂ) : (bit1 z).re = bit1 z.re

@[simp]

theorem Complex.bit0_im (z : ℂ) : (bit0 z).im = bit0 z.im

@[simp]

theorem Complex.bit1_im (z : ℂ) : (bit1 z).im = bit0 z.im

@[simp]

theorem Complex.ofReal_add (r : ℝ) (s : ℝ) : ↑(r + s) = ↑r + ↑s

@[simp]

theorem Complex.ofReal_bit0 (r : ℝ) : ↑(bit0 r) = bit0 ↑r

@[simp]

theorem Complex.ofReal_bit1 (r : ℝ) : ↑(bit1 r) = bit1 ↑r

instance Complex.instNegComplex : Neg ℂ

Equations

• Complex.instNegComplex = { neg := fun z => { re := -z.re, im := -z.im } }

@[simp]

theorem Complex.neg_re (z : ℂ) : (-z).re = -z.re

@[simp]

theorem Complex.neg_im (z : ℂ) : (-z).im = -z.im

@[simp]

theorem Complex.ofReal_neg (r : ℝ) : ↑(-r) = -↑r

instance Complex.instSubComplex : Sub ℂ

Equations

• Complex.instSubComplex = { sub := fun z w => { re := z.re - w.re, im := z.im - w.im } }

instance Complex.instMulComplex : Mul ℂ

Equations

• Complex.instMulComplex = { mul := fun z w => { re := z.re * w.re - z.im * w.im, im := z.re * w.im + z.im * w.re } }

@[simp]

theorem Complex.mul_re (z : ℂ) (w : ℂ) : (z * w).re = z.re * w.re - z.im * w.im

@[simp]

theorem Complex.mul_im (z : ℂ) (w : ℂ) : (z * w).im = z.re * w.im + z.im * w.re

@[simp]

theorem Complex.ofReal_mul (r : ℝ) (s : ℝ) : ↑(r * s) = ↑r * ↑s

theorem Complex.ofReal_mul_re (r : ℝ) (z : ℂ) : (↑r * z).re = r * z.re

theorem Complex.ofReal_mul_im (r : ℝ) (z : ℂ) : (↑r * z).im = r * z.im

theorem Complex.ofReal_mul' (r : ℝ) (z : ℂ) : ↑r * z = { re := r * z.re, im := r * z.im }

The imaginary unit, I

def Complex.I : ℂ

The imaginary unit.

Equations

• Complex.I = { re := 0, im := 1 }

@[simp]

theorem Complex.I_re : Complex.I.re = 0

@[simp]

theorem Complex.I_im : Complex.I.im = 1

@[simp]

theorem Complex.I_mul_I : Complex.I * Complex.I = -1

theorem Complex.I_mul (z : ℂ) : Complex.I * z = { re := -z.im, im := z.re }

theorem Complex.I_ne_zero : Complex.I ≠ 0

theorem Complex.mk_eq_add_mul_I (a : ℝ) (b : ℝ) : { re := a, im := b } = ↑a + ↑b * Complex.I

@[simp]

theorem Complex.re_add_im (z : ℂ) : ↑z.re + ↑z.im * Complex.I = z

theorem Complex.mul_I_re (z : ℂ) : (z * Complex.I).re = -z.im

theorem Complex.mul_I_im (z : ℂ) : (z * Complex.I).im = z.re

theorem Complex.I_mul_re (z : ℂ) : (Complex.I * z).re = -z.im

theorem Complex.I_mul_im (z : ℂ) : (Complex.I * z).im = z.re

@[simp]

theorem Complex.equivRealProd_symm_apply (p : ℝ × ℝ) : ↑Complex.equivRealProd.symm p = ↑p.fst + ↑p.snd * Complex.I

Commutative ring instance and lemmas

instance Complex.instNontrivialComplex : Nontrivial ℂ

Equations

• Complex.instNontrivialComplex = Complex.instNontrivialComplex.proof_1

instance Complex.instSMulRealComplex {R : Type u_1} [SMul R ℝ] : SMul R ℂ

Equations

• Complex.instSMulRealComplex = { smul := fun r x => { re := r • x.re - 0 * x.im, im := r • x.im + 0 * x.re } }

theorem Complex.smul_re {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) : (r • z).re = r • z.re

theorem Complex.smul_im {R : Type u_1} [SMul R ℝ] (r : R) (z : ℂ) : (r • z).im = r • z.im

@[simp]

theorem Complex.real_smul {x : ℝ} {z : ℂ} : x • z = ↑x * z

instance Complex.addCommGroup : AddCommGroup ℂ

Equations

• Complex.addCommGroup = AddCommGroup.mk Complex.addCommGroup.proof_11

instance Complex.Complex.addGroupWithOne : AddGroupWithOne ℂ

Equations

• Complex.Complex.addGroupWithOne = let src := Complex.addCommGroup; AddGroupWithOne.mk SubNegMonoid.zsmul Complex.Complex.addGroupWithOne.proof_7

instance Complex.commRing : CommRing ℂ

Equations

• Complex.commRing = let src := Complex.Complex.addGroupWithOne; CommRing.mk Complex.commRing.proof_13

instance Complex.instRingComplex : Ring ℂ

This shortcut instance ensures we do not find Ring via the noncomputable Complex.field instance.

Equations

• Complex.instRingComplex = inferInstance

instance Complex.instCommSemiringComplex : CommSemiring ℂ

This shortcut instance ensures we do not find CommSemiring via the noncomputable Complex.field instance.

Equations

• Complex.instCommSemiringComplex = inferInstance

instance Complex.instSemiringComplex : Semiring ℂ

This shortcut instance ensures we do not find Semiring via the noncomputable Complex.field instance.

Equations

• Complex.instSemiringComplex = inferInstance

def Complex.reAddGroupHom : ℂ →+ ℝ

The "real part" map, considered as an additive group homomorphism.

Equations

• Complex.reAddGroupHom = { toZeroHom := { toFun := Complex.re, map_zero' := Complex.zero_re }, map_add' := Complex.add_re }

@[simp]

theorem Complex.coe_reAddGroupHom : ↑Complex.reAddGroupHom = Complex.re

def Complex.imAddGroupHom : ℂ →+ ℝ

The "imaginary part" map, considered as an additive group homomorphism.

Equations

• Complex.imAddGroupHom = { toZeroHom := { toFun := Complex.im, map_zero' := Complex.zero_im }, map_add' := Complex.add_im }

@[simp]

theorem Complex.coe_imAddGroupHom : ↑Complex.imAddGroupHom = Complex.im

@[simp]

theorem Complex.I_pow_bit0 (n : ℕ) : Complex.I ^ bit0 n = (-1) ^ n

@[simp]

theorem Complex.I_pow_bit1 (n : ℕ) : Complex.I ^ bit1 n = (-1) ^ n * Complex.I

@[simp]

theorem Complex.ofReal_ofNat (n : ℕ) [Nat.AtLeastTwo n] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Complex.re_ofNat (n : ℕ) [Nat.AtLeastTwo n] : (OfNat.ofNat n).re = OfNat.ofNat n

@[simp]

theorem Complex.im_ofNat (n : ℕ) [Nat.AtLeastTwo n] : (OfNat.ofNat n).im = 0

Complex conjugation

instance Complex.instStarRingComplexToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingComplex : StarRing ℂ

This defines the complex conjugate as the star operation of the StarRing ℂ. It is recommended to use the ring endomorphism version starRingEnd, available under the notation conj in the locale ComplexConjugate.

Equations

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

@[simp]

theorem Complex.conj_re (z : ℂ) : (↑(starRingEnd ℂ) z).re = z.re

@[simp]

theorem Complex.conj_im (z : ℂ) : (↑(starRingEnd ℂ) z).im = -z.im

theorem Complex.conj_ofReal (r : ℝ) : ↑(starRingEnd ℂ) ↑r = ↑r

@[simp]

theorem Complex.conj_I : ↑(starRingEnd ℂ) Complex.I = -Complex.I

theorem Complex.conj_bit0 (z : ℂ) : ↑(starRingEnd ℂ) (bit0 z) = bit0 (↑(starRingEnd ℂ) z)

theorem Complex.conj_bit1 (z : ℂ) : ↑(starRingEnd ℂ) (bit1 z) = bit1 (↑(starRingEnd ℂ) z)

theorem Complex.conj_neg_I : ↑(starRingEnd ℂ) (-Complex.I) = Complex.I

theorem Complex.conj_eq_iff_real {z : ℂ} : ↑(starRingEnd ℂ) z = z ↔ ∃ r, z = ↑r

theorem Complex.conj_eq_iff_re {z : ℂ} : ↑(starRingEnd ℂ) z = z ↔ ↑z.re = z

theorem Complex.conj_eq_iff_im {z : ℂ} : ↑(starRingEnd ℂ) z = z ↔ z.im = 0

@[simp]

theorem Complex.star_def : star = ↑(starRingEnd ℂ)

Norm squared

def Complex.normSq : ℂ →*₀ ℝ

The norm squared function.

Equations

• Complex.normSq = { toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := Complex.normSq.proof_1 }, map_one' := Complex.normSq.proof_2, map_mul' := Complex.normSq.proof_3 }

theorem Complex.normSq_apply (z : ℂ) : ↑Complex.normSq z = z.re * z.re + z.im * z.im

@[simp]

theorem Complex.normSq_ofReal (r : ℝ) : ↑Complex.normSq ↑r = r * r

@[simp]

theorem Complex.normSq_mk (x : ℝ) (y : ℝ) : ↑Complex.normSq { re := x, im := y } = x * x + y * y

theorem Complex.normSq_add_mul_I (x : ℝ) (y : ℝ) : ↑Complex.normSq (↑x + ↑y * Complex.I) = x ^ 2 + y ^ 2

theorem Complex.normSq_eq_conj_mul_self {z : ℂ} : ↑(↑Complex.normSq z) = ↑(starRingEnd ℂ) z * z

theorem Complex.normSq_zero : ↑Complex.normSq 0 = 0

theorem Complex.normSq_one : ↑Complex.normSq 1 = 1

@[simp]

theorem Complex.normSq_I : ↑Complex.normSq Complex.I = 1

theorem Complex.normSq_nonneg (z : ℂ) : 0 ≤ ↑Complex.normSq z

@[simp]

theorem Complex.range_normSq : Set.range ↑Complex.normSq = Set.Ici 0

theorem Complex.normSq_eq_zero {z : ℂ} : ↑Complex.normSq z = 0 ↔ z = 0

@[simp]

theorem Complex.normSq_pos {z : ℂ} : 0 < ↑Complex.normSq z ↔ z ≠ 0

@[simp]

theorem Complex.normSq_neg (z : ℂ) : ↑Complex.normSq (-z) = ↑Complex.normSq z

@[simp]

theorem Complex.normSq_conj (z : ℂ) : ↑Complex.normSq (↑(starRingEnd ℂ) z) = ↑Complex.normSq z

theorem Complex.normSq_mul (z : ℂ) (w : ℂ) : ↑Complex.normSq (z * w) = ↑Complex.normSq z * ↑Complex.normSq w

theorem Complex.normSq_add (z : ℂ) (w : ℂ) : ↑Complex.normSq (z + w) = ↑Complex.normSq z + ↑Complex.normSq w + 2 * (z * ↑(starRingEnd ℂ) w).re

theorem Complex.re_sq_le_normSq (z : ℂ) : z.re * z.re ≤ ↑Complex.normSq z

theorem Complex.im_sq_le_normSq (z : ℂ) : z.im * z.im ≤ ↑Complex.normSq z

theorem Complex.mul_conj (z : ℂ) : z * ↑(starRingEnd ℂ) z = ↑(↑Complex.normSq z)

theorem Complex.add_conj (z : ℂ) : z + ↑(starRingEnd ℂ) z = ↑(2 * z.re)

def Complex.ofReal : ℝ →+* ℂ

The coercion ℝ → ℂ as a RingHom.

Equations

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

@[simp]

theorem Complex.ofReal_eq_coe (r : ℝ) : ↑Complex.ofReal r = ↑r

@[simp]

theorem Complex.I_sq : Complex.I ^ 2 = -1

@[simp]

theorem Complex.sub_re (z : ℂ) (w : ℂ) : (z - w).re = z.re - w.re

@[simp]

theorem Complex.sub_im (z : ℂ) (w : ℂ) : (z - w).im = z.im - w.im

@[simp]

theorem Complex.ofReal_sub (r : ℝ) (s : ℝ) : ↑(r - s) = ↑r - ↑s

@[simp]

theorem Complex.ofReal_pow (r : ℝ) (n : ℕ) : ↑(r ^ n) = ↑r ^ n

theorem Complex.sub_conj (z : ℂ) : z - ↑(starRingEnd ℂ) z = ↑(2 * z.im) * Complex.I

theorem Complex.normSq_sub (z : ℂ) (w : ℂ) : ↑Complex.normSq (z - w) = ↑Complex.normSq z + ↑Complex.normSq w - 2 * (z * ↑(starRingEnd ℂ) w).re

Inversion

noncomputable instance Complex.instInvComplex : Inv ℂ

Equations

• Complex.instInvComplex = { inv := fun z => ↑(starRingEnd ℂ) z * ↑(↑Complex.normSq z)⁻¹ }

theorem Complex.inv_def (z : ℂ) : z⁻¹ = ↑(starRingEnd ℂ) z * ↑(↑Complex.normSq z)⁻¹

@[simp]

theorem Complex.inv_re (z : ℂ) : z⁻¹.re = z.re / ↑Complex.normSq z

@[simp]

theorem Complex.inv_im (z : ℂ) : z⁻¹.im = -z.im / ↑Complex.normSq z

@[simp]

theorem Complex.ofReal_inv (r : ℝ) : ↑r⁻¹ = (↑r)⁻¹

theorem Complex.inv_zero : 0⁻¹ = 0

theorem Complex.mul_inv_cancel {z : ℂ} (h : z ≠ 0) : z * z⁻¹ = 1

noncomputable instance Complex.instRatCastComplex : RatCast ℂ

Equations

• Complex.instRatCastComplex = { ratCast := Rat.castRec }

Cast lemmas

@[simp]

theorem Complex.ofReal_nat_cast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem Complex.nat_cast_re (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem Complex.nat_cast_im (n : ℕ) : (↑n).im = 0

@[simp]

theorem Complex.ofReal_int_cast (n : ℤ) : ↑↑n = ↑n

@[simp]

theorem Complex.int_cast_re (n : ℤ) : (↑n).re = ↑n

@[simp]

theorem Complex.int_cast_im (n : ℤ) : (↑n).im = 0

@[simp]

theorem Complex.rat_cast_im (q : ℚ) : (↑q).im = 0

@[simp]

theorem Complex.rat_cast_re (q : ℚ) : (↑q).re = ↑q

Field instance and lemmas

noncomputable instance Complex.instField : Field ℂ

Equations

• Complex.instField = Field.mk zpowRec (@Complex.mul_inv_cancel) Complex.inv_zero fun n z => n • z

@[simp]

theorem Complex.I_zpow_bit0 (n : ℤ) : Complex.I ^ bit0 n = (-1) ^ n

@[simp]

theorem Complex.I_zpow_bit1 (n : ℤ) : Complex.I ^ bit1 n = (-1) ^ n * Complex.I

theorem Complex.div_re (z : ℂ) (w : ℂ) : (z / w).re = z.re * w.re / ↑Complex.normSq w + z.im * w.im / ↑Complex.normSq w

theorem Complex.div_im (z : ℂ) (w : ℂ) : (z / w).im = z.im * w.re / ↑Complex.normSq w - z.re * w.im / ↑Complex.normSq w

theorem Complex.conj_inv (x : ℂ) : ↑(starRingEnd ℂ) x⁻¹ = (↑(starRingEnd ℂ) x)⁻¹

@[simp]

theorem Complex.ofReal_div (r : ℝ) (s : ℝ) : ↑(r / s) = ↑r / ↑s

@[simp]

theorem Complex.ofReal_zpow (r : ℝ) (n : ℤ) : ↑(r ^ n) = ↑r ^ n

@[simp]

theorem Complex.div_I (z : ℂ) : z / Complex.I = -(z * Complex.I)

@[simp]

theorem Complex.inv_I : Complex.I⁻¹ = -Complex.I

theorem Complex.normSq_inv (z : ℂ) : ↑Complex.normSq z⁻¹ = (↑Complex.normSq z)⁻¹

theorem Complex.normSq_div (z : ℂ) (w : ℂ) : ↑Complex.normSq (z / w) = ↑Complex.normSq z / ↑Complex.normSq w

@[simp]

theorem Complex.ofReal_rat_cast (n : ℚ) : ↑↑n = ↑n

Characteristic zero

instance Complex.charZero : CharZero ℂ

Equations

• Complex.charZero = Complex.charZero.proof_1

theorem Complex.re_eq_add_conj (z : ℂ) : ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2

A complex number z plus its conjugate conj z is 2 times its real part.

theorem Complex.im_eq_sub_conj (z : ℂ) : ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * Complex.I)

A complex number z minus its conjugate conj z is 2i times its imaginary part.

Absolute value

theorem Complex.AbsTheory.abs_conj (z : ℂ) : Real.sqrt (↑Complex.normSq (↑(starRingEnd ℂ) z)) = Real.sqrt (↑Complex.normSq z)

noncomputable def Complex.abs : AbsoluteValue ℂ ℝ

The complex absolute value function, defined as the square root of the norm squared.

Equations

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

theorem Complex.abs_def : ↑Complex.abs = fun z => Real.sqrt (↑Complex.normSq z)

theorem Complex.abs_apply {z : ℂ} : ↑Complex.abs z = Real.sqrt (↑Complex.normSq z)

@[simp]

theorem Complex.abs_ofReal (r : ℝ) : ↑Complex.abs ↑r = |r|

theorem Complex.abs_of_nonneg {r : ℝ} (h : 0 ≤ r) : ↑Complex.abs ↑r = r

theorem Complex.abs_of_nat (n : ℕ) : ↑Complex.abs ↑n = ↑n

theorem Complex.mul_self_abs (z : ℂ) : ↑Complex.abs z * ↑Complex.abs z = ↑Complex.normSq z

theorem Complex.sq_abs (z : ℂ) : ↑Complex.abs z ^ 2 = ↑Complex.normSq z

@[simp]

theorem Complex.sq_abs_sub_sq_re (z : ℂ) : ↑Complex.abs z ^ 2 - z.re ^ 2 = z.im ^ 2

@[simp]

theorem Complex.sq_abs_sub_sq_im (z : ℂ) : ↑Complex.abs z ^ 2 - z.im ^ 2 = z.re ^ 2

@[simp]

theorem Complex.abs_I : ↑Complex.abs Complex.I = 1

@[simp]

theorem Complex.abs_two : ↑Complex.abs 2 = 2

@[simp]

theorem Complex.range_abs : Set.range ↑Complex.abs = Set.Ici 0

@[simp]

theorem Complex.abs_conj (z : ℂ) : ↑Complex.abs (↑(starRingEnd ℂ) z) = ↑Complex.abs z

@[simp]

theorem Complex.abs_prod {ι : Type u_1} (s : Finset ι) (f : ι → ℂ) : ↑Complex.abs (Finset.prod s f) = Finset.prod s fun I => ↑Complex.abs (f I)

theorem Complex.abs_pow (z : ℂ) (n : ℕ) : ↑Complex.abs (z ^ n) = ↑Complex.abs z ^ n

theorem Complex.abs_zpow (z : ℂ) (n : ℤ) : ↑Complex.abs (z ^ n) = ↑Complex.abs z ^ n

theorem Complex.abs_re_le_abs (z : ℂ) : |z.re| ≤ ↑Complex.abs z

theorem Complex.abs_im_le_abs (z : ℂ) : |z.im| ≤ ↑Complex.abs z

theorem Complex.re_le_abs (z : ℂ) : z.re ≤ ↑Complex.abs z

theorem Complex.im_le_abs (z : ℂ) : z.im ≤ ↑Complex.abs z

@[simp]

theorem Complex.abs_re_lt_abs {z : ℂ} : |z.re| < ↑Complex.abs z ↔ z.im ≠ 0

@[simp]

theorem Complex.abs_im_lt_abs {z : ℂ} : |z.im| < ↑Complex.abs z ↔ z.re ≠ 0

@[simp]

theorem Complex.abs_abs (z : ℂ) : |↑Complex.abs z| = ↑Complex.abs z

theorem Complex.abs_le_abs_re_add_abs_im (z : ℂ) : ↑Complex.abs z ≤ |z.re| + |z.im|

instance Complex.instNeZeroRealInstZeroRealOfNatToOfNat1InstOneReal : NeZero 1

Equations

• Complex.instNeZeroRealInstZeroRealOfNatToOfNat1InstOneReal = Complex.instNeZeroRealInstZeroRealOfNatToOfNat1InstOneReal.proof_1

theorem Complex.abs_le_sqrt_two_mul_max (z : ℂ) : ↑Complex.abs z ≤ Real.sqrt 2 * max |z.re| |z.im|

theorem Complex.abs_re_div_abs_le_one (z : ℂ) : |z.re / ↑Complex.abs z| ≤ 1

theorem Complex.abs_im_div_abs_le_one (z : ℂ) : |z.im / ↑Complex.abs z| ≤ 1

@[simp]

theorem Complex.abs_cast_nat (n : ℕ) : ↑Complex.abs ↑n = ↑n

@[simp]

theorem Complex.int_cast_abs (n : ℤ) : |↑n| = ↑Complex.abs ↑n

theorem Complex.normSq_eq_abs (x : ℂ) : ↑Complex.normSq x = ↑Complex.abs x ^ 2

Cauchy sequences

theorem Complex.isCauSeq_re (f : CauSeq ℂ ↑Complex.abs) : IsCauSeq abs fun n => (↑f n).re

theorem Complex.isCauSeq_im (f : CauSeq ℂ ↑Complex.abs) : IsCauSeq abs fun n => (↑f n).im

noncomputable def Complex.cauSeqRe (f : CauSeq ℂ ↑Complex.abs) : CauSeq ℝ abs

The real part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations

• Complex.cauSeqRe f = { val := fun n => (↑f n).re, property := (_ : IsCauSeq abs fun n => (↑f n).re) }

noncomputable def Complex.cauSeqIm (f : CauSeq ℂ ↑Complex.abs) : CauSeq ℝ abs

The imaginary part of a complex Cauchy sequence, as a real Cauchy sequence.

Equations

• Complex.cauSeqIm f = { val := fun n => (↑f n).im, property := (_ : IsCauSeq abs fun n => (↑f n).im) }

theorem Complex.isCauSeq_abs {f : ℕ → ℂ} (hf : IsCauSeq (↑Complex.abs) f) : IsCauSeq abs (↑Complex.abs ∘ f)

noncomputable def Complex.limAux (f : CauSeq ℂ ↑Complex.abs) : ℂ

The limit of a Cauchy sequence of complex numbers.

Equations

• Complex.limAux f = { re := CauSeq.lim (Complex.cauSeqRe f), im := CauSeq.lim (Complex.cauSeqIm f) }

theorem Complex.equiv_limAux (f : CauSeq ℂ ↑Complex.abs) : f ≈ CauSeq.const (↑Complex.abs) (Complex.limAux f)

instance Complex.instIsComplete : CauSeq.IsComplete ℂ ↑Complex.abs

Equations

• Complex.instIsComplete = Complex.instIsComplete.proof_1

theorem Complex.lim_eq_lim_im_add_lim_re (f : CauSeq ℂ ↑Complex.abs) : CauSeq.lim f = ↑(CauSeq.lim (Complex.cauSeqRe f)) + ↑(CauSeq.lim (Complex.cauSeqIm f)) * Complex.I

theorem Complex.lim_re (f : CauSeq ℂ ↑Complex.abs) : CauSeq.lim (Complex.cauSeqRe f) = (CauSeq.lim f).re

theorem Complex.lim_im (f : CauSeq ℂ ↑Complex.abs) : CauSeq.lim (Complex.cauSeqIm f) = (CauSeq.lim f).im

theorem Complex.isCauSeq_conj (f : CauSeq ℂ ↑Complex.abs) : IsCauSeq ↑Complex.abs fun n => ↑(starRingEnd ℂ) (↑f n)

noncomputable def Complex.cauSeqConj (f : CauSeq ℂ ↑Complex.abs) : CauSeq ℂ ↑Complex.abs

The complex conjugate of a complex Cauchy sequence, as a complex Cauchy sequence.

Equations

• Complex.cauSeqConj f = { val := fun n => ↑(starRingEnd ℂ) (↑f n), property := (_ : IsCauSeq ↑Complex.abs fun n => ↑(starRingEnd ℂ) (↑f n)) }

theorem Complex.lim_conj (f : CauSeq ℂ ↑Complex.abs) : CauSeq.lim (Complex.cauSeqConj f) = ↑(starRingEnd ℂ) (CauSeq.lim f)

noncomputable def Complex.cauSeqAbs (f : CauSeq ℂ ↑Complex.abs) : CauSeq ℝ abs

The absolute value of a complex Cauchy sequence, as a real Cauchy sequence.

Equations

• Complex.cauSeqAbs f = { val := ↑Complex.abs ∘ ↑f, property := (_ : IsCauSeq abs (↑Complex.abs ∘ ↑f)) }

theorem Complex.lim_abs (f : CauSeq ℂ ↑Complex.abs) : CauSeq.lim (Complex.cauSeqAbs f) = ↑Complex.abs (CauSeq.lim f)

@[simp]

theorem Complex.ofReal_prod {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(Finset.prod s fun i => f i) = Finset.prod s fun i => ↑(f i)

@[simp]

theorem Complex.ofReal_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(Finset.sum s fun i => f i) = Finset.sum s fun i => ↑(f i)

@[simp]

theorem Complex.re_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (Finset.sum s fun i => f i).re = Finset.sum s fun i => (f i).re

@[simp]

theorem Complex.im_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (Finset.sum s fun i => f i).im = Finset.sum s fun i => (f i).im