Persistent I-tangent polynomial
DefinitionEsgk_DistanceNewtonPersistentTangentRootsalgebraic-geometrycomplex-analysispolynomials
This extracts the homogeneous component at the I-circular local order of a homogenized plane polynomial and dehomogenizes it to a complex one-variable polynomial.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_DistanceNewtonITangentHomogeneousForm
import Definitions.Def_Esgk_PlaneCircularLocalChart
import Definitions.Def_Esgk_PlaneCircularLocalOrderDegree
import Definitions.Def_Esgk_PlaneProjectiveHomogenization
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
namespace Esgk
open PachDeZeeuw.Algebraic
variable {n : ℕ}
def circularITangentPolynomial (G : PlanePoly) : Polynomial ℂ :=
circularChartDehomogenization
(MvPolynomial.homogeneousComponent (planeCircularLocalOrderI G)
(projectiveCircularChartI (planeHomogenization G.totalDegree G)))
end Esgk