Power-sum polynomial for squared distances
DefinitionEsgk_DistanceNewtonPowerSumPolynomialalgebrageometrypolynomials
For a finite configuration and a nonnegative exponent, this defines the plane polynomial formed from the corresponding power sum of squared distances and the ordered distinct-distance values.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_DistanceDeficiencyNewton
import Definitions.Def_Esgk_Energy
import Definitions.Def_Esgk_Foundation
import Definitions.Def_Esgk_PlaneAffineIsometryDistancePolynomial
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 EuclideanGeometry PachDeZeeuw.Algebraic
open scoped BigOperators
variable {n : ℕ}
def distanceNewtonPowerSumPolynomial (p : Config n) (t : ℕ) : PlanePoly :=
MvPolynomial.C (3 * ∑ r ∈ OrderedDistanceValues p, (r ^ 2) ^ t) -
∑ q : Fin n, (planeSquaredDistancePolynomial (p q)) ^ t
end Esgk