@[reducible, inline]

abbrev complexNumbers : Type

Definition 4.6.1 (Complex numbers): the set of complex numbers is {a + b i | a, b ∈ ℝ}, where i is a symbol satisfying i^2 = -1. In Lean, this is identified with the existing type ℂ.

Equations

• complexNumbers = ℂ

theorem complexNumbers_exists_real_imag (z : ℂ) : ∃ (a : ℝ) (b : ℝ), z = ↑a + ↑b * Complex.I

Every complex number can be written in the form a + b i with a b : ℝ.

theorem helperForLemma_4_6_2_canonicalDecompositionExists (z : ℂ) : ∃ (p : ℝ × ℝ), z = ↑p.1 + ↑p.2 * Complex.I

Helper for Lemma 4.6.2: every complex number admits a real-imaginary pair representation z = a + bi.

theorem helperForLemma_4_6_2_coordinatesFromRepresentation {z : ℂ} {p : ℝ × ℝ} (h : z = ↑p.1 + ↑p.2 * Complex.I) : p.1 = z.re ∧ p.2 = z.im

Helper for Lemma 4.6.2: any representation z = a + bi must use a = Re(z) and b = Im(z).

theorem helperForLemma_4_6_2_uniqueDecompositionPair (z : ℂ) (p : ℝ × ℝ) (h : z = ↑p.1 + ↑p.2 * Complex.I) : p = (z.re, z.im)

Helper for Lemma 4.6.2: the pair (Re z, Im z) is the unique coefficient pair in a decomposition z = a + bi.

theorem helperForLemma_4_6_2_iSquared : Complex.I ^ 2 = -1

Helper for Lemma 4.6.2: the imaginary unit squares to -1.

theorem helperForLemma_4_6_2_negEqualsNegOneMul (z : ℂ) : -z = -1 * z

Helper for Lemma 4.6.2: negation agrees with multiplication by -1.

theorem complex_unique_decomposition_i_sq_and_neg_mul : (∀ (z : ℂ), ∃! p : ℝ × ℝ, z = ↑p.1 + ↑p.2 * Complex.I) ∧ Complex.I ^ 2 = -1 ∧ ∀ (z : ℂ), -z = -1 * z

Lemma 4.6.2: every z : ℂ has a unique decomposition z = a + b i with a, b : ℝ; moreover i^2 = -1 and -z = (-1)z for all z : ℂ.

@[reducible, inline]

abbrev complexNumbersAsPairs : Type

Definition 4.6.2 (Complex numbers): (i) a complex number is an ordered pair (a, b) with a, b ∈ ℝ; (ii) equality is componentwise, i.e. (a, b) = (c, d) iff a = c and b = d; (iii) the set of all such complex numbers is ℝ × ℝ.

Equations

• complexNumbersAsPairs = (ℝ × ℝ)

@[reducible, inline]

abbrev complexPairAdd (z w : complexNumbersAsPairs) : complexNumbersAsPairs

Componentwise addition on ordered pairs of real numbers.

Equations

• complexPairAdd z w = (z.1 + w.1, z.2 + w.2)

@[reducible, inline]

abbrev complexPairNeg (z : complexNumbersAsPairs) : complexNumbersAsPairs

Componentwise negation on ordered pairs of real numbers.

Equations

• complexPairNeg z = (-z.1, -z.2)

@[reducible, inline]

abbrev complexPairZero : complexNumbersAsPairs

The zero ordered pair (0, 0) in ℝ × ℝ.

Equations

• complexPairZero = (0, 0)

def complexPairAddNegZeroData : (complexNumbersAsPairs → complexNumbersAsPairs → complexNumbersAsPairs) × (complexNumbersAsPairs → complexNumbersAsPairs) × complexNumbersAsPairs

Definition 4.6.3 (Complex addition, negation, and zero): let ℂ be the set of ordered pairs of real numbers. For z = (a, b) and w = (c, d), define z + w := (a + c, b + d), -z := (-a, -b), and 0_C := (0, 0).

Equations

• complexPairAddNegZeroData = (complexPairAdd, complexPairNeg, complexPairZero)

theorem complex_addition_abelian_group_axioms : (∀ (z₁ z₂ : ℂ), z₁ + z₂ = z₂ + z₁) ∧ (∀ (z₁ z₂ z₃ : ℂ), z₁ + z₂ + z₃ = z₁ + (z₂ + z₃)) ∧ (∀ (z₁ : ℂ), z₁ + 0 = z₁ ∧ 0 + z₁ = z₁) ∧ ∀ (z₁ : ℂ), z₁ + -z₁ = 0 ∧ -z₁ + z₁ = 0

Lemma 4.6.1 (Addition on ℂ satisfies the abelian group axioms): for all z₁ z₂ z₃ : ℂ, (i) z₁ + z₂ = z₂ + z₁, (ii) (z₁ + z₂) + z₃ = z₁ + (z₂ + z₃), (iii) z₁ + 0 = 0 + z₁ = z₁, and (iv) z₁ + (-z₁) = (-z₁) + z₁ = 0. In particular, (ℂ, +) is an abelian group with identity element 0.

def complexPairMulOneData : (complexNumbersAsPairs → complexNumbersAsPairs → complexNumbersAsPairs) × complexNumbersAsPairs

Definition 4.6.4 (Complex multiplication): for complex numbers viewed as ordered pairs z = (a, b) and w = (c, d), their product is zw = (ac - bd, ad + bc), and the complex multiplicative identity is 1_C = (1, 0).

Equations

• complexPairMulOneData = (fun (z w : complexNumbersAsPairs) => (z.1 * w.1 - z.2 * w.2, z.1 * w.2 + z.2 * w.1), 1, 0)

def realToComplexEmbedding : ℝ → ℂ

Definition 4.6.5 (Embedding of real numbers into complex numbers): define ι : ℝ → ℂ by identifying x : ℝ with (x, 0) in ℂ.

Equations

• realToComplexEmbedding x = ↑x

theorem realToComplexEmbedding_respects_operations : (∀ (x y : ℝ), x = y ↔ realToComplexEmbedding x = realToComplexEmbedding y) ∧ (∀ (x₁ x₂ : ℝ), realToComplexEmbedding (x₁ + x₂) = realToComplexEmbedding x₁ + realToComplexEmbedding x₂) ∧ (∀ (x : ℝ), realToComplexEmbedding (-x) = -realToComplexEmbedding x) ∧ ∀ (x₁ x₂ : ℝ), realToComplexEmbedding (x₁ * x₂) = realToComplexEmbedding x₁ * realToComplexEmbedding x₂

The embedding of real numbers into complex numbers preserves equality, addition, negation, and multiplication.

def imaginaryUnit : ℂ

Definition 4.6.6 (Imaginary unit): the imaginary unit is the complex number i ∈ ℂ defined by i := (0, 1).

Equations

• imaginaryUnit = { re := 0, im := 1 }

def IsRealComplex (z : ℂ) : Prop

A complex number is real when its imaginary part vanishes.

Equations

• IsRealComplex z = (z.im = 0)

def IsPurelyImaginaryComplex (z : ℂ) : Prop

A complex number is purely imaginary when its real part vanishes.

Equations

• IsPurelyImaginaryComplex z = (z.re = 0)

theorem complex_real_imaginary_parts_and_conjugate (z : ℂ) : z = ↑z.re + Complex.I * ↑z.im ∧ (IsRealComplex z ↔ z.im = 0) ∧ (IsPurelyImaginaryComplex z ↔ z.re = 0) ∧ star z = ↑z.re - Complex.I * ↑z.im

Definition 4.6.7 (Real and imaginary parts; complex conjugate): for z : ℂ, z = Re(z) + i Im(z), a number is real iff Im(z) = 0, a number is purely imaginary iff Re(z) = 0, and the complex conjugate is conj z = Re(z) - i Im(z).

theorem helperForProposition_4_6_2_re_eq_add_star (z : ℂ) : ↑z.re = (z + star z) / 2

Helper for Proposition 4.6.2: Re(z) equals (z + \bar z)/2 written with star.

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

Helper for Proposition 4.6.2: Im(z) equals (z - \bar z)/(2i) written with star.

theorem complex_re_and_im_eq_conjugate_formulas (z : ℂ) : ↑z.re = (z + star z) / 2 ∧ ↑z.im = (z - star z) / (2 * Complex.I)

Proposition 4.6.2: for every complex number z ∈ ℂ, Re(z) = (z + \overline{z}) / 2 and Im(z) = (z - \overline{z}) / (2i).

theorem helperForLemma_4_6_3_conj_add_neg_mul (z w : ℂ) : star (z + w) = star z + star w ∧ star (-z) = -star z ∧ star (z * w) = star z * star w

Helper for Lemma 4.6.3: complex conjugation preserves addition, negation, and multiplication.

theorem helperForLemma_4_6_3_conj_involutive (z : ℂ) : star (star z) = z

Helper for Lemma 4.6.3: complex conjugation is involutive.

theorem helperForLemma_4_6_3_conj_eq_iff_eq (z w : ℂ) : star z = star w ↔ z = w

Helper for Lemma 4.6.3: complex conjugation is injective.

theorem helperForLemma_4_6_3_conj_fixed_iff_isReal (z : ℂ) : star z = z ↔ IsRealComplex z

Helper for Lemma 4.6.3: fixed points of conjugation are exactly the real complex numbers.

theorem complex_conjugation_involution (z w : ℂ) : star (z + w) = star z + star w ∧ star (-z) = -star z ∧ star (z * w) = star z * star w ∧ star (star z) = z ∧ (star z = star w ↔ z = w) ∧ (star z = z ↔ IsRealComplex z)

Lemma 4.6.3 (Complex conjugation is an involution): for z w : ℂ, complex conjugation satisfies \overline{z + w} = \bar z + \bar w, \overline{-z} = -\bar z, \overline{z w} = \bar z \, \bar w, \overline{\bar z} = z, ` and moreover \bar z = \bar w iff z = w, while \bar z = z iff z is real.

@[reducible, inline]

noncomputable abbrev complexAbsoluteValue (z : ℂ) : ℝ

Definition 4.6.8 (Complex absolute value): for z = a + bi with a b : ℝ, the complex absolute value is the nonnegative real number |z| = sqrt (a^2 + b^2) = (a^2 + b^2)^(1/2). In Lean this is represented by the complex norm ‖z‖.

Equations

• complexAbsoluteValue z = ‖z‖

theorem complexAbsoluteValue_nonnegative (z : ℂ) : 0 ≤ complexAbsoluteValue z

Lemma 4.6.4: for every z ∈ ℂ, the complex absolute value |z| is a non-negative real number.

theorem complexAbsoluteValue_eq_zero_iff (z : ℂ) : complexAbsoluteValue z = 0 ↔ z = 0

Lemma 4.6.5: for every z ∈ ℂ, we have |z| = 0 if and only if z = 0.

theorem helperForLemma_4_6_6_mulConj_eq_normSqCast (z : ℂ) : z * star z = ↑(Complex.normSq z)

Helper for Lemma 4.6.6: z * conjugate(z) is the real scalar Complex.normSq z, viewed in ℂ.

theorem helperForLemma_4_6_6_mulConj_re_eq_normSq (z : ℂ) : (z * star z).re = Complex.normSq z

Helper for Lemma 4.6.6: the real part of z * conjugate(z) is Complex.normSq z.

theorem helperForLemma_4_6_6_mulConj_re_eq_absSq (z : ℂ) : (z * star z).re = complexAbsoluteValue z ^ 2

Helper for Lemma 4.6.6: (z * conjugate(z)).re equals |z|^2.

theorem helperForLemma_4_6_6_sqrt_absSq_eq_absValue (z : ℂ) : √(complexAbsoluteValue z ^ 2) = complexAbsoluteValue z

Helper for Lemma 4.6.6: √(|z|^2) = |z|.

theorem complex_mul_conj_eq_abs_sq_and_abs_eq_sqrt (z : ℂ) : z * star z = ↑(complexAbsoluteValue z) ^ 2 ∧ complexAbsoluteValue z = √(z * star z).re

Lemma 4.6.6: for every z ∈ ℂ, we have z * \overline{z} = |z|^2. In particular, |z| = sqrt (z * \overline{z}), interpreted in Lean as |z| = sqrt ((z * \overline{z}).re).

theorem complexAbsoluteValue_mul (z w : ℂ) : complexAbsoluteValue (z * w) = complexAbsoluteValue z * complexAbsoluteValue w

Lemma 4.6.7: for all z, w ∈ ℂ, the complex absolute value is multiplicative: |zw| = |z| |w|.

theorem complexAbsoluteValue_conj (z : ℂ) : complexAbsoluteValue (star z) = complexAbsoluteValue z

Lemma 4.6.8: for every z ∈ ℂ, the complex absolute value is invariant under complex conjugation: |\overline{z}| = |z|.

theorem complexAbsoluteValue_div_of_ne_zero (z w : ℂ) : w ≠ 0 → complexAbsoluteValue (z / w) = complexAbsoluteValue z / complexAbsoluteValue w

Proposition 4.6.3: if z, w ∈ ℂ and w ≠ 0, then |z / w| = |z| / |w|.

noncomputable def complexReciprocalQuotientPartialData : (ℂ → Option ℂ) × (ℂ → ℂ → Option ℂ)

Definition 4.6.9 (Complex reciprocal and quotient): for z : ℂ, the reciprocal is undefined at 0 and is |z|^{-2} \overline{z} otherwise; for z w : ℂ, the quotient z / w is defined when w ≠ 0 by z * w^{-1}.

Equations

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

noncomputable def complexReciprocalPartial (z : ℂ) : Option ℂ

Partial complex reciprocal: undefined at 0, and otherwise given by |z|^{-2} \overline{z}.

Equations

• complexReciprocalPartial z = complexReciprocalQuotientPartialData.1 z

noncomputable def complexQuotientPartial (z w : ℂ) : Option ℂ

Partial complex quotient: for z w : ℂ, this is defined by mapping w to its partial reciprocal and multiplying by z.

Equations

• complexQuotientPartial z w = complexReciprocalQuotientPartialData.2 z w

noncomputable def complexExponential (z : ℂ) : ℂ

Definition 4.6.10 (Complex exponential): for each z ∈ ℂ, the complex exponential is defined by the power series exp(z) = ∑' n : ℕ, z^n / n!.

Equations

• complexExponential z = ∑' (n : ℕ), z ^ n / ↑n.factorial

theorem complex_exp_add (z w : ℂ) : Complex.exp (z + w) = Complex.exp z * Complex.exp w

Theorem 4.6.1: for all z, w ∈ ℂ, one has exp(z + w) = exp(z) exp(w).

theorem complex_exp_conj (z : ℂ) : Complex.exp (star z) = star (Complex.exp z)

Proposition 4.6.1: for every z ∈ ℂ, the complex exponential commutes with complex conjugation, i.e. exp(conj z) = conj (exp z).

theorem helperForLemma_4_6_9_absRe_le_complexAbs (z : ℂ) : |z.re| ≤ complexAbsoluteValue z

Helper for Lemma 4.6.9: the absolute value of the real part is bounded by the complex absolute value.

theorem helperForLemma_4_6_9_negComplexAbs_le_re (z : ℂ) : -complexAbsoluteValue z ≤ z.re

Helper for Lemma 4.6.9: the real part is bounded below by the negated complex absolute value.

theorem helperForLemma_4_6_9_re_le_complexAbs (z : ℂ) : z.re ≤ complexAbsoluteValue z

Helper for Lemma 4.6.9: the real part is bounded above by the complex absolute value.

theorem realPart_le_complexAbsoluteValue (z : ℂ) : -complexAbsoluteValue z ≤ z.re ∧ z.re ≤ complexAbsoluteValue z

Lemma 4.6.9: for every complex number z, its real part is bounded by its complex absolute value: -|z| ≤ Re(z) ≤ |z|.

theorem helperForLemma_4_6_10_absIm_le_complexAbs (z : ℂ) : |z.im| ≤ complexAbsoluteValue z

Helper for Lemma 4.6.10: the absolute value of the imaginary part is bounded by the complex absolute value.

theorem helperForLemma_4_6_10_negComplexAbs_le_im (z : ℂ) : -complexAbsoluteValue z ≤ z.im

Helper for Lemma 4.6.10: the imaginary part is bounded below by the negated complex absolute value.

theorem helperForLemma_4_6_10_im_le_complexAbs (z : ℂ) : z.im ≤ complexAbsoluteValue z

Helper for Lemma 4.6.10: the imaginary part is bounded above by the complex absolute value.

theorem imagPart_le_complexAbsoluteValue (z : ℂ) : -complexAbsoluteValue z ≤ z.im ∧ z.im ≤ complexAbsoluteValue z

Lemma 4.6.10: for every z ∈ ℂ, the imaginary part is bounded by the complex absolute value: -|z| ≤ Im(z) ≤ |z|.

theorem complexAbsoluteValue_le_abs_re_add_abs_im (z : ℂ) : complexAbsoluteValue z ≤ |z.re| + |z.im|

Lemma 4.6.11: for every z ∈ ℂ, the complex absolute value is bounded by the sum of the absolute values of its real and imaginary parts: |z| ≤ |Re(z)| + |Im(z)|.

theorem complexAbsoluteValue_add_le (z w : ℂ) : complexAbsoluteValue (z + w) ≤ complexAbsoluteValue z + complexAbsoluteValue w

Lemma 4.6.12: for all z, w ∈ ℂ, the complex absolute value satisfies the triangle inequality |z + w| ≤ |z| + |w|.

theorem helperForProposition_4_6_4_normEq_iff_sameRay (z w : ℂ) : complexAbsoluteValue (z + w) = complexAbsoluteValue z + complexAbsoluteValue w ↔ SameRay ℝ z w

Helper for Proposition 4.6.4: equality in the triangle inequality for complex norm is equivalent to the two numbers lying on the same real ray.

theorem helperForProposition_4_6_4_sameRay_to_existsPosMul (z w : ℂ) (hz : z ≠ 0) (hw : w ≠ 0) (hzw : SameRay ℝ z w) : ∃ (c : ℝ), 0 < c ∧ z = ↑c * w

Helper for Proposition 4.6.4: two nonzero complex numbers on the same real ray differ by multiplication by a positive real scalar.

theorem helperForProposition_4_6_4_existsPosMul_to_normEq (z w : ℂ) : (∃ (c : ℝ), 0 < c ∧ z = ↑c * w) → complexAbsoluteValue (z + w) = complexAbsoluteValue z + complexAbsoluteValue w

Helper for Proposition 4.6.4: if one complex number is a positive real multiple of another, then equality holds in the triangle inequality.

theorem complexAbsoluteValue_add_eq_add_iff_exists_pos_real_mul (z w : ℂ) (hz : z ≠ 0) (hw : w ≠ 0) : complexAbsoluteValue (z + w) = complexAbsoluteValue z + complexAbsoluteValue w ↔ ∃ (c : ℝ), 0 < c ∧ z = ↑c * w

Proposition 4.6.4: for nonzero complex numbers z and w, |z + w| = |z| + |w| if and only if there exists a real number c > 0 such that z = c w.

theorem helperForProposition_4_6_5_posNegOne_from_posI (Pos : ℂ → Prop) (hMulPos : ∀ (z w : ℂ), Pos z → Pos w → Pos (z * w)) (hPosI : Pos Complex.I) : Pos (-1)

Helper for Proposition 4.6.5: if i is positive and positivity is closed under multiplication, then -1 is positive.

theorem helperForProposition_4_6_5_posNegOne_from_negI (Pos Neg : ℂ → Prop) (hNegToPos : ∀ (z : ℂ), Neg z → Pos (-z)) (hMulPos : ∀ (z w : ℂ), Pos z → Pos w → Pos (z * w)) (hNegI : Neg Complex.I) : Pos (-1)

Helper for Proposition 4.6.5: if i is negative, negation sends negatives to positives, and positivity is multiplicatively closed, then -1 is positive.

theorem helperForProposition_4_6_5_posNegOne (Pos Neg : ℂ → Prop) (hTrichotomy : ∀ (z : ℂ), Pos z ∨ Neg z ∨ z = 0) (hNegToPos : ∀ (z : ℂ), Neg z → Pos (-z)) (hMulPos : ∀ (z w : ℂ), Pos z → Pos w → Pos (z * w)) : Pos (-1)

Helper for Proposition 4.6.5: trichotomy at i, together with the negation rule Neg z → Pos (-z) and multiplicative closure of positivity, forces -1 to be positive.

theorem helperForProposition_4_6_5_contradiction_from_posNegOne (Pos Neg : ℂ → Prop) (hPosNegExclusive : ∀ (z : ℂ), ¬(Pos z ∧ Neg z)) (hPosToNeg : ∀ (z : ℂ), Pos z → Neg (-z)) (hMulPos : ∀ (z w : ℂ), Pos z → Pos w → Pos (z * w)) (hPosNegOne : Pos (-1)) : False

Helper for Proposition 4.6.5: if -1 is positive, positivity is closed under multiplication, and positives negate to negatives, then exclusivity of positive/negative classes yields a contradiction.

theorem no_complex_positive_negative_zero_partition : ¬∃ (Pos : ℂ → Prop) (Neg : ℂ → Prop), (∀ (z : ℂ), (Pos z ∨ Neg z ∨ z = 0) ∧ ¬(Pos z ∧ Neg z) ∧ ¬(Pos z ∧ z = 0) ∧ ¬(Neg z ∧ z = 0)) ∧ (∀ (z : ℂ), Pos z → Neg (-z)) ∧ (∀ (z : ℂ), Neg z → Pos (-z)) ∧ (∀ (z w : ℂ), Pos z → Pos w → Pos (z + w)) ∧ ∀ (z w : ℂ), Pos z → Pos w → Pos (z * w)

Proposition 4.6.5: there does not exist a partition of ℂ into positive, negative, and zero classes such that for every z, w : ℂ: (i) exactly one of Pos z, Neg z, or z = 0 holds, (ii) positivity/negativity are exchanged by negation, (iii) positive numbers are closed under addition, and (iv) positive numbers are closed under multiplication.

theorem complex_tendsto_iff_re_im_tendsto (zSeq : ℕ → ℂ) (z : ℂ) : have d := fun (z₁ z₂ : ℂ) => ‖z₁ - z₂‖; ((∀ (z₁ z₂ : ℂ), 0 ≤ d z₁ z₂) ∧ (∀ (z₁ z₂ : ℂ), d z₁ z₂ = 0 ↔ z₁ = z₂) ∧ (∀ (z₁ z₂ : ℂ), d z₁ z₂ = d z₂ z₁) ∧ ∀ (z₁ z₂ z₃ : ℂ), d z₁ z₃ ≤ d z₁ z₂ + d z₂ z₃) ∧ ((∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, d (zSeq n) z < ε) ↔ Filter.Tendsto (fun (n : ℕ) => (zSeq n).re) Filter.atTop (nhds z.re) ∧ Filter.Tendsto (fun (n : ℕ) => (zSeq n).im) Filter.atTop (nhds z.im))

Lemma 4.6.13: with d(z,w) = |z - w| on ℂ, this gives the usual metric on ℂ; moreover, a sequence z_n converges to z in this metric iff both real and imaginary parts converge, i.e. Re(z_n) → Re(z) and Im(z_n) → Im(z).

theorem helperForLemma_4_6_14_arith_tendsto_bundle (zSeq wSeq : ℕ → ℂ) (z w c : ℂ) (hz : Filter.Tendsto zSeq Filter.atTop (nhds z)) (hw : Filter.Tendsto wSeq Filter.atTop (nhds w)) : Filter.Tendsto (fun (n : ℕ) => zSeq n + wSeq n) Filter.atTop (nhds (z + w)) ∧ Filter.Tendsto (fun (n : ℕ) => zSeq n - wSeq n) Filter.atTop (nhds (z - w)) ∧ Filter.Tendsto (fun (n : ℕ) => c * zSeq n) Filter.atTop (nhds (c * z)) ∧ Filter.Tendsto (fun (n : ℕ) => zSeq n * wSeq n) Filter.atTop (nhds (z * w))

Helper for Lemma 4.6.14: bundled arithmetic limit laws in ℂ for sum, difference, scalar multiplication, and product.

theorem helperForLemma_4_6_14_star_tendsto (zSeq : ℕ → ℂ) (z : ℂ) (hz : Filter.Tendsto zSeq Filter.atTop (nhds z)) : Filter.Tendsto (fun (n : ℕ) => star (zSeq n)) Filter.atTop (nhds (star z))

Helper for Lemma 4.6.14: conjugation preserves sequence limits in ℂ.

theorem helperForLemma_4_6_14_div_tendsto (zSeq wSeq : ℕ → ℂ) (z w : ℂ) (hz : Filter.Tendsto zSeq Filter.atTop (nhds z)) (hw : Filter.Tendsto wSeq Filter.atTop (nhds w)) : (∀ (n : ℕ), wSeq n ≠ 0) → w ≠ 0 → Filter.Tendsto (fun (n : ℕ) => zSeq n / wSeq n) Filter.atTop (nhds (z / w))

Helper for Lemma 4.6.14: quotient limit law in ℂ under nonzero limit.

theorem complex_limit_laws (zSeq wSeq : ℕ → ℂ) (z w c : ℂ) (hz : Filter.Tendsto zSeq Filter.atTop (nhds z)) (hw : Filter.Tendsto wSeq Filter.atTop (nhds w)) : Filter.Tendsto (fun (n : ℕ) => zSeq n + wSeq n) Filter.atTop (nhds (z + w)) ∧ Filter.Tendsto (fun (n : ℕ) => zSeq n - wSeq n) Filter.atTop (nhds (z - w)) ∧ Filter.Tendsto (fun (n : ℕ) => c * zSeq n) Filter.atTop (nhds (c * z)) ∧ Filter.Tendsto (fun (n : ℕ) => zSeq n * wSeq n) Filter.atTop (nhds (z * w)) ∧ Filter.Tendsto (fun (n : ℕ) => star (zSeq n)) Filter.atTop (nhds (star z)) ∧ ((∀ (n : ℕ), wSeq n ≠ 0) → w ≠ 0 → Filter.Tendsto (fun (n : ℕ) => zSeq n / wSeq n) Filter.atTop (nhds (z / w)))

Lemma 4.6.14 (Complex limit laws): if zₙ → z and wₙ → w in ℂ, then zₙ + wₙ → z + w, zₙ - wₙ → z - w, c zₙ → c z, zₙ wₙ → z w, and conj zₙ → conj z; moreover, if wₙ ≠ 0 for all n and w ≠ 0, then zₙ / wₙ → z / w.