noncomputable def HexRootsMathlib.affineHomotopy (f g : Polynomial ℂ) (t : ℝ) : Polynomial ℂ

The affine polynomial path from g at t = 0 to f at t = 1.

Equations

• HexRootsMathlib.affineHomotopy f g t = g + Polynomial.C ↑t * (f - g)

@[simp]

theorem HexRootsMathlib.affineHomotopy.zero (f g : Polynomial ℂ) : affineHomotopy f g 0 = g

@[simp]

theorem HexRootsMathlib.affineHomotopy.one (f g : Polynomial ℂ) : affineHomotopy f g 1 = f

@[simp]

theorem HexRootsMathlib.affineHomotopy.eval (f g : Polynomial ℂ) (t : ℝ) (z : ℂ) : Polynomial.eval z (affineHomotopy f g t) = Polynomial.eval z g + ↑t * (Polynomial.eval z f - Polynomial.eval z g)

@[simp]

theorem HexRootsMathlib.affineHomotopy.derivative (f g : Polynomial ℂ) (t : ℝ) : Polynomial.derivative (affineHomotopy f g t) = affineHomotopy (Polynomial.derivative f) (Polynomial.derivative g) t

theorem HexRootsMathlib.affineHomotopy.continuous_eval (f g : Polynomial ℂ) (c : ℂ) (R : ℝ) : Continuous fun (q : ℝ × ℝ) => Polynomial.eval (circleMap c R q.2) (affineHomotopy f g q.1)

Evaluation of the affine path along a fixed parameterized circle is jointly continuous in the homotopy parameter and circle parameter.

theorem HexRootsMathlib.affineHomotopy.continuous_derivativeEval (f g : Polynomial ℂ) (c : ℂ) (R : ℝ) : Continuous fun (q : ℝ × ℝ) => Polynomial.eval (circleMap c R q.2) (Polynomial.derivative (affineHomotopy f g q.1))

Derivative evaluation of the affine path along a fixed parameterized circle is jointly continuous in both parameters.

theorem HexRootsMathlib.affineHomotopy.continuous_rootsInDisc {f g : Polynomial ℂ} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hboundary : ∀ t ∈ Set.Icc 0 1, ∀ z ∈ Metric.sphere c R, Polynomial.eval z (affineHomotopy f g t) ≠ 0) : ContinuousOn (fun (t : ℝ) => rootsInDisc (affineHomotopy f g t) c R) (Set.Icc 0 1)

The root count of a boundary-nonvanishing affine polynomial homotopy is continuous on its parameter interval.

theorem HexRootsMathlib.affineHomotopy.rootsInDisc_eq {f g : Polynomial ℂ} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hboundary : ∀ t ∈ Set.Icc 0 1, ∀ z ∈ Metric.sphere c R, Polynomial.eval z (affineHomotopy f g t) ≠ 0) : rootsInDisc g c R = rootsInDisc f c R

A boundary-nonvanishing affine homotopy has equal root counts at its two endpoints.