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

Add the lemma:

```lean
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.

Author: jsm28

Mathlib/Analysis/Convex/Combination.lean

@@ -144,6 +144,34 @@ end Finset
 
 variable {z}
 
+lemma Finset.centerMass_const (hw : ∑ j ∈ t, w j ≠ 0) (c : E) :
+    t.centerMass w (Function.const _ c) = c := by
+  simp [centerMass, ← sum_smul, hw]
+
+lemma Finset.centerMass_congr [DecidableEq ι] {t' : Finset ι} {w' : ι → R} {z' : ι → E}
+    (h : ∀ i, (i ∈ t ∧ w i ≠ 0 ∨ i ∈ t' ∧ w' i ≠ 0) → i ∈ t ∩ t' ∧ w i = w' i ∧ z i = z' i) :
+    t.centerMass w z = t'.centerMass w' z' := by
+  classical
+  rw [← centerMass_filter_ne_zero, centerMass, ← centerMass_filter_ne_zero, centerMass]
+  congr 1
+  · congr 1
+    exact sum_congr (by grind) (by grind)
+  · exact sum_congr (by grind) (by grind)
+
+lemma Finset.centerMass_congr_finset [DecidableEq ι] {t' : Finset ι}
+    (h : ∀ i ∈ t ∪ t', w i ≠ 0 → i ∈ t ∩ t') : t.centerMass w z = t'.centerMass w z :=
+  centerMass_congr (by grind)
+
+lemma Finset.centerMass_congr_weights {w' : ι → R} (h : ∀ i ∈ t, w i = w' i) :
+    t.centerMass w z = t.centerMass w' z := by
+  classical
+  exact centerMass_congr (by grind)
+
+lemma Finset.centerMass_congr_fun {z' : ι → E} (h : ∀ i ∈ t, w i ≠ 0 → z i = z' i) :
+    t.centerMass w z = t.centerMass w z' := by
+  classical
+  exact centerMass_congr (by grind)
+
 lemma Finset.centerMass_of_sum_add_sum_eq_zero {s t : Finset ι}
     (hw : ∑ i ∈ s, w i + ∑ i ∈ t, w i = 0) (hz : ∑ i ∈ s, w i • z i + ∑ i ∈ t, w i • z i = 0) :
     s.centerMass w z = t.centerMass w z := by