Theorems · Definition · geometry

Finset.centroidWeightsIndicator

(k : Type u_1) → [DivisionRing k] → {ι : Type u_4} → Finset ι → ι → k

centroidWeights gives the weights for the centroid as a constant function, which is suitable when summing over the points whose centroid is being taken. This function gives the weights in a form suitable for summing over a larger set of points, as an indicator function that is zero outside the set whose centroid is being taken. In the case of a Fintype, the sum may be over univ.

Defined in

Mathlib.LinearAlgebra.AffineSpace.Centroid

Cited by

7 results in Mathlib

Foundations

Depth 54 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRing