Centroid of an indexed planar configuration

Definition

Esgk_ConfigurationCentroid

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

discrete-geometrygeometry

For an indexed configuration $p=(p_1,\dots,p_n)$ of $n$ points in the plane, configCentroid p is the centroid

c(p)=\frac1n\sum_{j=1}^n p_j .

It is the center of the annulus that contains a configuration with few distinct distances and no four points on a common circle, in the theorem Esgk.thin_annulus_sq_of_noFourCocircular.

Formalization Note The configuration is a map Fin n → ℝ². For $n=0$ the formula gives the origin, because the Lean inverse of $0$ is $0$ .

Definition code

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

import Definitions.Def_Esgk_Foundation

namespace Esgk

open EuclideanGeometry
open scoped BigOperators
variable {n : ℕ}

noncomputable def configCentroid (p : Config n) : Point :=
  (n : ℝ)⁻¹ • ∑ j, p j

end Esgk

View graph