[Merged by Bors] - feat(linear_algebra/affine_space/combination, analysis/convex/combination): basic lemmas about affine combinations, center of mass, centroid

[ocfnash]

---

Split off from other work to simplify later review.

[kbuzzard]

Very nice!

[YaelDillies]

This is very much needed glue between affine_combination, finset.center_mass and finset.centroid!

Could you also add this lemma? I feel like it belongs in this PR.

lemma affine_combination_eq_center_mass {ι : Type*} {t : finset ι} {p : ι → E} {w : ι → ℝ}
  (hw₂ : ∑ i in t, w i = 1) :
  affine_combination t p w = center_mass t w p :=
begin
  rw affine_combination_eq_weighted_vsub_of_point_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
  simp only [vsub_eq_sub, add_zero, finset.weighted_vsub_of_point_apply, vadd_eq_add, sub_zero],
  rw center_mass_eq_of_sum_1 _ _ hw₂,
end

Note that it suggests swapping the arguments of finset.center_mass.

[ocfnash]

Could you also add this lemma? I feel like it belongs in this PR.

I’m afraid I’m traveling until Sep 21 and have phone-only internet. Thank you for the review!

I will be delighted to take up these good suggestions when I return, or else please feel free to adopt this PR.

[YaelDillies]

Note that this will conflict with #9268 but afterwards affine_combination_eq_center_mass will become unconditional.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Canceled.

[sgouezel]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests