Commit 2025-11-14 11:51 109eba69

feat(Analysis/Convex/Combination): centerMass_const, centerMass_congr (#31451) Add the lemma:

lemma Finset.centerMass_const (hw : ∑ j ∈ t, w j ≠ 0) (c : E) :
    t.centerMass w (Function.const _ c) = c := by

along with various congruence lemmas that help with applying this in cases where the points are constant for the nonzero weights in t, but not necessarily everywhere.