Singular and radial-critical sample points

Definition

Esgk_PlaneCurveExceptionalSample

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This selects the points of a finite planar sample that are singular points of a given polynomial curve or radial-critical points relative to a fixed center.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCurveRadialCritical
import Definitions.Def_Esgk_PlaneCurveSafeComponents
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Definitions.Def_LeanFormalizations_PachDeZeeuw_Bezout
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CurveInterface
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

open Set MvPolynomial
open PachDeZeeuw.Algebraic hiding Point2

namespace Esgk

 
def planeCurveExceptionalSample (G : PlanePoly) (a : Point2) (S : Finset Point2) :
    Finset Point2 := by
  classical
  exact S.filter (fun p ↦ p ∈ SingularPointSet G ∨ p ∈ planeRadialCriticalZeroSet G a)


end Esgk

View graph