Commit 2025-12-06 00:03 89ec9c84

feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces (#31452) Add various lemmas that combinations of points (nonnegative weights, at least two weights of distinct points nonzero) in strictly convex sets lie in the interior of that set, or in strictly convex spaces or affine spaces for such spaces lie in a ball when the points lie in the corresponding closed ball. These are analogous to existing lemmas for convex combinations and for pairs of points in strictly convex sets or spaces. In particular, the way StrictConvex.centerMass_mem_interior is stated with various hypotheses after the colon follows how Convex.centerMass_mem is stated (the hypotheses could of course move before the colon if they were then generalized for the induction). Convenience lemmas for the cases of closedInterior (excluding vertices) of a simplex, and interior of a simplex, are included. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Triangle.20interior.20and.20its.20circumsphere/with/540305703 requested such a statement (in a different form). They don't include anything for bundled spheres since those are currently defined in Mathlib.Geometry.Euclidean, though given a suitable more generic name for the bundled sphere structure, various basic material about such spheres could move to a more generic metric space location, at which point it would be reasonable to add versions of these statements that use bundled spheres.