Multiset of missing squared distances

Definition

Esgk_DistanceSquaredMissingMultiset

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

finite-combinatoricsgeometrymultisets

For a configuration point, this forms the multiset containing each ordered distance value's squared value with its missing-neighbor multiplicity.

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 Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


namespace Esgk

open scoped BigOperators

variable {n : ℕ}

 
noncomputable def distanceSquaredMissingMultiset
    (p : Config n) (i : Fin n) : Multiset ℝ :=
  (OrderedDistanceValues p).val.bind fun r ↦
    Multiset.replicate (DistanceMissingMultiplicity p i r) (r ^ 2)


end Esgk

View graph