2 Roots of Complex Polynomials (New)
2.1 Generic helper maps
We use the local notation ‘Cstar‘ to refer to the subtype of nonzero complex numbers.
local notation "Cstar" => {z : ℂ // z ≠ 0}
The canonical inclusion of a sphere into the corresponding closed ball.
def sphereToClosedBall [PseudoMetricSpace α]
(x : α) (r : ℝ) :
Metric.sphere x r → Metric.closedBall x r
This is just the inclusion map induced by the elementary containment \(\operatorname {sphere}(x,r)\subseteq \operatorname {closedBall}(x,r)\).
After forgetting the subtype, the sphere-to-ball inclusion is the identity on points.
theorem coe_sphereToClosedBall
[PseudoMetricSpace α]
(x : α) (r : ℝ) (y : Metric.sphere x r) :
sphereToClosedBall x r y = y
This follows immediately from the fact that the inclusion map does not change the underlying point.
2.2 Homotopies through loops
A homotopy \(H\colon I\times I\to X\) is a homotopy through loops if each horizontal slice has the same initial and terminal point.
def IsLoopHomotopy
[TopologicalSpace X] (H : C(I × I, X)) :
Prop
This is the direct formalization of the condition that every slice \(t\mapsto H(s,t)\) is a loop.
2.3 Circle-valued helper constructions
The canonical inclusion of the unit circle into the closed unit disk.
abbrev toClosedUnitDisk :
Circle → Metric.closedBall (0 : ℂ) 1
This is the general sphere-to-closed-ball inclusion specialized to the unit circle in \(\mathbb {C}\).
After forgetting the subtype, the inclusion of the circle into the closed disk does not change the underlying complex number.
theorem coe_toClosedUnitDisk (z : Circle) :
((toClosedUnitDisk z :
Metric.closedBall (0 : ℂ) 1) : ℂ) = z
The inclusion map is literally the identity on the underlying point.
Given a continuous map \(\psi \colon S^1\to X\), its associated loop is obtained by precomposing with the standard parametrization \(t\mapsto \exp (2\pi i t)\) of the circle on \(I\).
def circleLoop
[TopologicalSpace X] (f : C(Circle, X)) :
Path (f 1) (f 1)
The map is continuous by composition, and its endpoints agree because the circle parametrization takes both \(0\) and \(1\) to the point \(1\in S^1\).
The associated loop evaluates at \(t\in I\) as \(\psi (\exp (2\pi i t))\).
theorem circleLoop_apply
[TopologicalSpace X] (f : C(Circle, X))
(t : I) :
(ContinuousMap.circleLoop f) t =
f (Circle.exp (2 * Real.pi * (t : ℝ)))
This is just the defining formula for the associated loop.
A homotopy of circle maps induces a homotopy of the associated loops by precomposing with the standard circle parametrization.
def circleLoopHomotopy
[TopologicalSpace X] {f g : C(Circle, X)}
(H : ContinuousMap.Homotopy f g) :
C(I × I, X)
This is obtained by composing the given homotopy with the standard map from \(I\) to the circle.
The induced homotopy evaluates by the expected formula \(\widehat H(s,t)=H(s,\exp (2\pi i t))\).
theorem circleLoopHomotopy_apply
[TopologicalSpace X] {f g : C(Circle, X)}
(H : ContinuousMap.Homotopy f g) (x : I × I) :
circleLoopHomotopy H x =
H (x.1, Circle.exp (2 * Real.pi * (x.2 : ℝ)))
This is immediate from the definition of the induced homotopy.
The induced homotopy of associated loops is a homotopy through loops.
theorem circleLoopHomotopy_isLoopHomotopy
[TopologicalSpace X] {f g : C(Circle, X)}
(H : ContinuousMap.Homotopy f g) :
ContinuousMap.IsLoopHomotopy
(circleLoopHomotopy H)
For each fixed \(s\), the two endpoints correspond to the same point of the circle because \(\exp (0)=\exp (2\pi i)=1\).
At the left endpoint of the homotopy parameter, the induced loop homotopy recovers the associated loop of the initial map.
theorem circleLoopHomotopy_zero_left
[TopologicalSpace X] {f g : C(Circle, X)}
(H : ContinuousMap.Homotopy f g) (t : I) :
circleLoopHomotopy H (0, t) =
(ContinuousMap.circleLoop f) t
This is the defining property of a homotopy at time \(0\), evaluated along the circle parametrization.
At the right endpoint of the homotopy parameter, the induced loop homotopy recovers the associated loop of the terminal map.
theorem circleLoopHomotopy_one_left
[TopologicalSpace X] {f g : C(Circle, X)}
(H : ContinuousMap.Homotopy f g) (t : I) :
circleLoopHomotopy H (1, t) =
(ContinuousMap.circleLoop g) t
This is the corresponding defining property of a homotopy at time \(1\).
2.4 Lifts and winding numbers of loops
Internally, we identify \(\mathbb {C}^\times \) (as the group of units in \(\mathbb {C}\)) with the subtype of nonzero complex numbers.
def complexUnitsHomeomorphNeZero :
ℂˣ ≃ₜ Cstar
This is the standard homeomorphism between units in a field and the corresponding nonzero subtype.
A units-valued continuous map can be viewed as a continuous map to nonzero complex numbers.
noncomputable def toNonzeroSubtype
[TopologicalSpace α] (f : C(α, ℂˣ)) :
C(α, Cstar)
Compose the given map with the homeomorphism from \(\mathbb {C}^\times \) to the nonzero-complex subtype.
A continuous map to nonzero complex numbers can be viewed as a units-valued continuous map.
noncomputable def fromNonzeroSubtype
[TopologicalSpace α] (f : C(α, Cstar)) :
C(α, ℂˣ)
This is the inverse construction, using the inverse homeomorphism.
After coercing to \(\mathbb {C}\), the map obtained by passing from units to the nonzero subtype has the same values as the original map.
theorem coe_toNonzeroSubtype_apply
[TopologicalSpace α] (f : C(α, ℂˣ)) (x : α) :
(ContinuousMap.toNonzeroSubtype f x : ℂ) =
(f x : ℂ)
Both sides are definitionally the same underlying complex number.
After coercing to \(\mathbb {C}\), the map obtained by passing from the nonzero subtype to units has the same values as the original map.
theorem coe_fromNonzeroSubtype_apply
[TopologicalSpace α] (f : C(α, Cstar)) (x : α)
:
((ContinuousMap.fromNonzeroSubtype f x : ℂˣ) :
ℂ) = (f x : ℂ)
Applying the forward homeomorphism to the units-valued version recovers the original subtype-valued map, and coercing to \(\mathbb {C}\) then gives the claim.
Passing from the nonzero subtype to units and back again does not change a continuous map.
theorem toNonzeroSubtype_fromNonzeroSubtype
[TopologicalSpace α] (f : C(α, Cstar)) :
ContinuousMap.toNonzeroSubtype
(ContinuousMap.fromNonzeroSubtype f) = f
This is the left-inverse identity for the homeomorphism between units and the nonzero subtype.
Passing from units to the nonzero subtype and back again does not change a continuous map.
theorem fromNonzeroSubtype_toNonzeroSubtype
[TopologicalSpace α] (f : C(α, ℂˣ)) :
ContinuousMap.fromNonzeroSubtype
(ContinuousMap.toNonzeroSubtype f) = f
This is the corresponding right-inverse identity.
A units-valued path can be viewed as a path in the nonzero-complex subtype.
noncomputable def toNonzeroSubtype
{u v : ℂˣ} (γ : Path u v) :
Path (complexUnitsHomeomorphNeZero u)
(complexUnitsHomeomorphNeZero v)
Map the path through the same homeomorphism from units to nonzero complex numbers.
After coercing to \(\mathbb {C}\), the converted path has the same pointwise values as the original path.
theorem coe_toNonzeroSubtype_apply
{u v : ℂˣ} (γ : Path u v) (t : I) :
((Path.toNonzeroSubtype γ t : Cstar) : ℂ) =
(γ t : ℂ)
This is immediate from the definition of the path map.
Given a path in \(\mathbb {C}\setminus \{ 0\} \) and a chosen logarithm of its starting point, lift the path through the covering map \(\exp \colon \mathbb {C}\to \mathbb {C}\setminus \{ 0\} \).
noncomputable def expLift
{z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
(hw0 : Complex.exp w0 = (z₀ : ℂ)) :
C(I, ℂ)
This is the path-lifting theorem for the already-upstream covering map ‘Complex.exp‘.
The lifted path projects back to the original path under the exponential map.
theorem expLift_apply
{z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
(hw0 : Complex.exp w0 = (z₀ : ℂ)) (t : I) :
Complex.exp (Path.expLift γ w0 hw0 t) =
(γ t : ℂ)
This is exactly the lifting property supplied by the covering-space API, after forgetting the codomain subtype.
The lifted path starts at the prescribed basepoint.
theorem expLift_zero
{z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
(hw0 : Complex.exp w0 = (z₀ : ℂ)) :
Path.expLift γ w0 hw0 0 = w0
This is the standard initial-value property of the lifted path.
Any other lift of the same path with the same starting point agrees with the canonical lifted path.
theorem eq_expLift
{z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
(hw0 : Complex.exp w0 = (z₀ : ℂ))
(Γ : C(I, ℂ))
(hlift : ∀ t, Complex.exp (Γ t) = (γ t : ℂ))
(h0 : Γ 0 = w0) :
Γ = Path.expLift γ w0 hw0
This is uniqueness of lifts for the covering map \(\exp \), specialized to paths in \(\mathbb {C}\setminus \{ 0\} \).
Adding an integral multiple of \(2\pi i\) does not change the exponential.
theorem exp_add_int_mul_two_pi_I_eq
(z : ℂ) (n : ℤ) :
Complex.exp (z + n * (2 * Real.pi *
Complex.I)) = Complex.exp z
This is the usual \(2\pi i\)-periodicity of the complex exponential map.
Two lifts of the same path differ by a constant integral multiple of \(2\pi i\).
theorem eq_add_int_mul_two_pi_I_of_lifts
{z₀ z₁ : Cstar} (γ : Path z₀ z₁)
(Γ₀ Γ₁ : C(I, ℂ))
(hΓ₀ : ∀ t, Complex.exp (Γ₀ t) = (γ t : ℂ))
(hΓ₁ : ∀ t, Complex.exp (Γ₁ t) = (γ t : ℂ)) :
∃ n : ℤ, ∀ t, Γ₁ t =
Γ₀ t + n * (2 * Real.pi * Complex.I)
At the initial point, the two lifts have the same exponential, so their values differ by an integral multiple of \(2\pi i\). Shifting one lift by that constant does not change its projection, and uniqueness of lifts then shows the two lifts agree everywhere.
The winding number of a loop in \(\mathbb {C}\setminus \{ 0\} \) is defined from the endpoint difference of a lift through the exponential covering map.
noncomputable def windingNumber
{z : Cstar} (γ : Path z z) :
ℤ
Choose the lift beginning at \(\log (z)\). Since the path is a loop, the endpoints of the lift have the same exponential, hence differ by an integral multiple of \(2\pi i\); that integer is the winding number.
If \(\Gamma \) is any lift of a loop in \(\mathbb {C}\setminus \{ 0\} \), then the endpoint quotient \((\Gamma (1)-\Gamma (0))/(2\pi i)\) computes the winding number.
theorem windingNumber_eq_of_lift
{z : Cstar} (γ : Path z z) (Γ : C(I, ℂ))
(hlift : ∀ t, Complex.exp (Γ t) = (γ t : ℂ)) :
(Γ 1 - Γ 0) / (2 * Real.pi * Complex.I) =
Path.windingNumber γ
Any lift differs from the canonical lift by a constant integral multiple of \(2\pi i\), so the endpoint difference and hence the quotient by \(2\pi i\) are unchanged.
Loops in \(\mathbb {C}\setminus \{ 0\} \) that are freely homotopic through loops have the same winding number.
theorem windingNumber_eq_of_homotopy
{z z' : Cstar} (γ : Path z z)
(γ' : Path z' z') (H : C(I × I, Cstar))
(hhom : ContinuousMap.IsLoopHomotopy H)
(hzero : ∀ t, H (0, t) = γ t)
(hone : ∀ t, H (1, t) = γ' t) :
Path.windingNumber γ = Path.windingNumber γ'
Lift the whole free homotopy through the exponential covering map. The two boundary loops of the lift differ by a constant integral multiple of \(2\pi i\) along the side edges, so their endpoint differences agree and hence their winding numbers agree.
The constant loop has winding number zero.
theorem windingNumber_refl
(z : Cstar) :
Path.windingNumber (Path.refl z) = 0
The constant loop is lifted by a constant logarithm, whose endpoint difference is zero.
The winding number of a loop in \(\mathbb {C}^\times \) is defined by transporting the loop to \(\mathbb {C}\setminus \{ 0\} \) and using the previous definition.
noncomputable def unitsWindingNumber
{u : ℂˣ} (γ : Path u u) :
ℤ
Use the homeomorphism between \(\mathbb {C}^\times \) and the subtype of nonzero complex numbers.
Any exponential lift of a loop in \(\mathbb {C}^\times \) computes its winding number by the same endpoint quotient formula.
theorem unitsWindingNumber_eq_of_lift
{u : ℂˣ} (γ : Path u u) (Γ : C(I, ℂ))
(hlift : ∀ t, Complex.exp (Γ t) = (γ t : ℂ)) :
(Γ 1 - Γ 0) / (2 * Real.pi * Complex.I) =
Path.unitsWindingNumber γ
After transporting the loop to the nonzero subtype, this is exactly the previous lifting formula.
Freely homotopic loops in \(\mathbb {C}^\times \) have the same winding number.
theorem unitsWindingNumber_eq_of_homotopy
{u u' : ℂˣ} (γ : Path u u) (γ' : Path u' u')
(H : C(I × I, ℂˣ))
(hhom : ContinuousMap.IsLoopHomotopy H)
(hzero : ∀ t, H (0, t) = γ t)
(hone : ∀ t, H (1, t) = γ' t) :
Path.unitsWindingNumber γ =
Path.unitsWindingNumber γ'
Transport the homotopy through the homeomorphism from \(\mathbb {C}^\times \) to \(\mathbb {C}\setminus \{ 0\} \) and apply homotopy invariance there.
The constant loop in \(\mathbb {C}^\times \) has winding number zero.
theorem unitsWindingNumber_refl
(u : ℂˣ) :
Path.unitsWindingNumber (Path.refl u) = 0
After transporting to the nonzero subtype, this becomes the previous statement for constant loops.
2.5 Winding numbers of circle maps
The winding number of a continuous map from the circle to \(\mathbb {C}^\times \) is the winding number of its associated loop.
noncomputable def windingNumber
(f : C(Circle, ℂˣ)) :
ℤ
This is the modern ‘Path‘-based version of passing from a circle map to its associated loop and taking the loop winding number.
A constant map from the circle to \(\mathbb {C}^\times \) has winding number zero.
theorem windingNumber_const
(c : ℂˣ) :
windingNumber (ContinuousMap.const _ c :
C(Circle, ℂˣ)) = 0
The associated loop of a constant circle map is the constant loop, whose winding number is zero.
Homotopic circle maps into \(\mathbb {C}^\times \) have the same winding number.
theorem windingNumber_eq_of_homotopy
{f g : C(Circle, ℂˣ)}
(H : ContinuousMap.Homotopy f g) :
windingNumber f = windingNumber g
Precompose the homotopy with the standard parametrization of the circle to obtain a free homotopy between the associated loops, then apply homotopy invariance for loop winding numbers.
If two maps into \(\Bbbk ^\times \) satisfy the walking-dog inequality \(\lVert f(x)-g(x)\rVert {\lt} \lVert f(x)\rVert \) pointwise, then they are homotopic through maps into \(\Bbbk ^\times \).
theorem exists_homotopy_of_norm_sub_lt
[TopologicalSpace α] [RCLike 𝕜]
{f g : C(α, 𝕜ˣ)}
(hclose :
∀ z : α, ‖(f z : 𝕜) - g z‖ <
‖(f z : 𝕜)‖) :
Nonempty (ContinuousMap.Homotopy f g)
Use the straight-line homotopy \((1-t)f+t g\). If this vanished at some point, then \(f=t(f-g)\) there, which would force \(\| f\| \le \| f-g\| \), contradicting the hypothesis.
Circle maps satisfying the walking-dog inequality have the same winding number.
theorem windingNumber_eq_of_norm_sub_lt
{f g : C(Circle, ℂˣ)}
(hclose :
∀ z : Circle, ‖(f z : ℂ) - g z‖ <
‖(f z : ℂ)‖) :
windingNumber f = windingNumber g
Apply the previous existence theorem for a homotopy and then homotopy invariance of winding number.
If a map from the unit circle to \(\mathbb {C}^\times \) extends to the closed unit disk through maps into \(\mathbb {C}^\times \), then its winding number is zero.
theorem windingNumber_eq_zero_of_exists_extension
{f : C(Circle, ℂˣ)}
{F : C(Metric.closedBall (0 : ℂ) 1, ℂˣ)}
(hF :
∀ z : Circle,
F (Circle.toClosedUnitDisk z) = f z) :
windingNumber f = 0
Radially contract the closed disk to its center. Composing the extension with this contraction produces a homotopy from the boundary map to a constant map, and constant maps have winding number zero.
The same vanishing result holds for extensions valued in the nonzero-complex subtype, after transporting through the units/nonzero bridge.
theorem windingNumber_eq_zero_of_exists_extension'
{f : C(Circle, ℂˣ)}
{F : C(Metric.closedBall (0 : ℂ) 1,
{z : ℂ // z ≠ 0})}
(hF :
∀ z : Circle,
F (Circle.toClosedUnitDisk z) =
ContinuousMap.toNonzeroSubtype f z) :
windingNumber f = 0
Convert the subtype-valued extension into a units-valued extension and apply the previous theorem.
2.6 Monomials on the circle
Given \(a,c\in \mathbb {C}^\times \) and \(n\in \mathbb N\), define the circle map \(z\mapsto a\, (cz)^n\) with values in \(\mathbb {C}^\times \).
noncomputable def circleScaledMonomial
(a c : ℂˣ) (n : ℕ) :
C(Circle, ℂˣ)
The underlying formula is continuous, and it never vanishes because \(a\), \(c\), and every point of the circle are nonzero.
After coercing to \(\mathbb {C}\), the scaled monomial has the expected pointwise formula \(a\, (cz)^n\).
theorem coe_circleScaledMonomial_apply
(a c : ℂˣ) (n : ℕ) (z : Circle) :
((circleScaledMonomial a c n z : ℂˣ) : ℂ) =
a * (((c : ℂ) * z) ^ n)
This is immediate from the definition.
For \(R{\gt}0\), the map \(z\mapsto a\, (Rz)^n\) is obtained by specializing the previous construction to the nonzero scalar \(R\).
noncomputable def circleMonomial
(a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R) :
C(Circle, ℂˣ)
This is just the scaled monomial with \(c=R\in \mathbb {C}^\times \).
After coercing to \(\mathbb {C}\), the circle monomial evaluates as \(a\, (Rz)^n\).
theorem coe_circleMonomial_apply
(a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R)
(z : Circle) :
((circleMonomial a n R hR z : ℂˣ) : ℂ) =
a * (((R : ℂ) * z) ^ n)
Unfold the specialized definition and simplify.
The winding number of the map \(z\mapsto a\, (cz)^n\) on the unit circle is \(n\).
theorem circleScaledMonomial_windingNumber
(a c : ℂˣ) (n : ℕ) :
ContinuousMap.windingNumber
(circleScaledMonomial a c n) = (n : ℤ)
Choose a logarithm of the nonzero constant \(a c^n\). Then \(t\mapsto \log (ac^n)+n(2\pi t)i\) is a lift of the associated loop, and its endpoint difference is exactly \(2\pi n i\).
For \(R{\gt}0\), the winding number of the map \(z\mapsto a\, (Rz)^n\) on the unit circle is \(n\).
theorem circleMonomial_windingNumber
(a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R) :
ContinuousMap.windingNumber (circleMonomial a
n R hR) = (n : ℤ)
This is the previous theorem applied to the special case \(c=R\in \mathbb {C}^\times \).
2.7 Polynomial maps on the circle and disk
If a polynomial has no zeros on the circle of radius \(R\), then \(z\mapsto p(Rz)\) defines a map from the unit circle to \(\mathbb {C}^\times \).
noncomputable def mapCircleUnits
(p : Polynomial ℂ) (R : ℝ)
(hR : ∀ z : Circle, p.eval ((R : ℂ) * z) ≠ 0)
:
C(Circle, ℂˣ)
The polynomial evaluation map is continuous, and the nonvanishing hypothesis upgrades it to a units-valued map.
If a polynomial has no zeros on the closed unit disk of radius \(R\), then \(z\mapsto p(Rz)\) defines a map from that disk to \(\mathbb {C}^\times \).
noncomputable def mapClosedUnitDiskUnits
(p : Polynomial ℂ) (R : ℝ)
(hR :
∀ z : Metric.closedBall (0 : ℂ) 1,
p.eval ((R : ℂ) * z) ≠ 0) :
C(Metric.closedBall (0 : ℂ) 1, ℂˣ)
This is the disk-valued analogue of the previous construction.
After coercing to \(\mathbb {C}\), the circle-valued units map evaluates as \(p(Rz)\).
theorem coe_mapCircleUnits_apply
(p : Polynomial ℂ) (R : ℝ)
(hR : ∀ z : Circle, p.eval ((R : ℂ) * z) ≠ 0)
(z : Circle) :
((Polynomial.mapCircleUnits p R hR z : ℂˣ) :
ℂ) = p.eval ((R : ℂ) * z)
This is immediate from the definition.
After coercing to \(\mathbb {C}\), the disk-valued units map evaluates as \(p(Rz)\).
theorem coe_mapClosedUnitDiskUnits_apply
(p : Polynomial ℂ) (R : ℝ)
(hR :
∀ z : Metric.closedBall (0 : ℂ) 1,
p.eval ((R : ℂ) * z) ≠ 0)
(z : Metric.closedBall (0 : ℂ) 1) :
((Polynomial.mapClosedUnitDiskUnits p R hR z :
ℂˣ) : ℂ) = p.eval ((R : ℂ) * z)
Again this is immediate from the definition.
For a nonconstant complex polynomial, the leading term eventually dominates the sum of the lower terms on circles of large radius.
theorem leadingTerm_dominates_on_circle
(p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
∃ R0 : ℝ, 0 < R0 ∧ ∀ R : ℝ, R0 ≤ R →
∀ z : Circle, ‖p.eval ((R : ℂ) * z) -
p.leadingCoeff * (((R : ℂ) * z) ^
p.natDegree)‖ < ‖p.leadingCoeff * (((R : ℂ) *
z) ^ p.natDegree)‖
Choose \(R\) so large that the sum of the lower-order coefficients is small compared with the leading coefficient. On the circle of radius \(R\), the lower-order terms are then bounded by a strictly smaller quantity than the norm of the leading term.
For sufficiently large \(R\), the restriction of a nonconstant polynomial to the circle of radius \(R\) has winding number equal to the degree of the polynomial.
theorem eventually_windingNumber_eq_natDegree
(p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
∃ R0 : ℝ, 0 < R0 ∧ ∀ R : ℝ, R0 ≤ R →
∃ f : C(Circle, ℂˣ), (∀ z, (f z : ℂ) = p.eval
((R : ℂ) * z)) ∧ ContinuousMap.windingNumber f
= (p.natDegree : ℤ)
For large radius, the polynomial map is uniformly close on the circle to its leading monomial in the walking-dog sense. The monomial has winding number equal to the degree, so the polynomial map has the same winding number.
Every nonconstant complex polynomial has a complex root.
theorem exists_root_of_natDegree_pos
(p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
∃ z : ℂ, p.IsRoot z
Assume the polynomial has no complex roots. Then it is nonzero on the whole plane, so the map \(z\mapsto p(Rz)\) extends from the unit circle to the closed unit disk through nonzero values. Hence its winding number must be zero. On the other hand, for sufficiently large \(R\), the previous theorem shows that the same winding number is the positive degree of the polynomial, a contradiction.