Convex combinations in strictly convex sets and spaces.

This file proves lemmas about convex combinations of points in strictly convex sets and strictly convex spaces.

theorem StrictConvex.centerMass_mem_interior {R : Type u_1} {V : Type u_2} {ι : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [TopologicalSpace V] [AddCommGroup V] [Module R V] {s : Set V} {t : Finset ι} {w : ι → R} {z : ι → V} (hs : StrictConvex R s) : (∀ i ∈ t, 0 ≤ w i) → ∀ (i j : ι), i ∈ t → j ∈ t → z i ≠ z j → w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ s) → t.centerMass w z ∈ interior s

theorem StrictConvex.sum_mem_interior {R : Type u_1} {V : Type u_2} {ι : Type u_4} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [TopologicalSpace V] [AddCommGroup V] [Module R V] {s : Set V} {t : Finset ι} {w : ι → R} {z : ι → V} (hs : StrictConvex R s) (h0 : ∀ i ∈ t, 0 ≤ w i) (h1 : ∑ i ∈ t, w i = 1) {i j : ι} (hi : i ∈ t) (hj : j ∈ t) (hij : z i ≠ z j) (hi0 : w i ≠ 0) (hj0 : w j ≠ 0) (hz : ∀ i ∈ t, z i ∈ s) : ∑ k ∈ t, w k • z k ∈ interior s

theorem centerMass_mem_ball_of_strictConvexSpace {V : Type u_2} {ι : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] {t : Finset ι} {w : ι → ℝ} {p : V} {r : ℝ} {z : ι → V} (h0 : ∀ i ∈ t, 0 ≤ w i) {i j : ι} (hi : i ∈ t) (hj : j ∈ t) (hij : z i ≠ z j) (hi0 : w i ≠ 0) (hj0 : w j ≠ 0) (hz : ∀ i ∈ t, z i ∈ Metric.closedBall p r) : t.centerMass w z ∈ Metric.ball p r

theorem sum_mem_ball_of_strictConvexSpace {V : Type u_2} {ι : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] {t : Finset ι} {w : ι → ℝ} {p : V} {r : ℝ} {z : ι → V} (h0 : ∀ i ∈ t, 0 ≤ w i) (h1 : ∑ i ∈ t, w i = 1) {i j : ι} (hi : i ∈ t) (hj : j ∈ t) (hij : z i ≠ z j) (hi0 : w i ≠ 0) (hj0 : w j ≠ 0) (hz : ∀ i ∈ t, z i ∈ Metric.closedBall p r) : ∑ k ∈ t, w k • z k ∈ Metric.ball p r

theorem norm_sum_lt_of_strictConvexSpace {V : Type u_2} {ι : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] {t : Finset ι} {w : ι → ℝ} {r : ℝ} {z : ι → V} (h0 : ∀ i ∈ t, 0 ≤ w i) (h1 : ∑ i ∈ t, w i = 1) {i j : ι} (hi : i ∈ t) (hj : j ∈ t) (hij : z i ≠ z j) (hi0 : w i ≠ 0) (hj0 : w j ≠ 0) (hz : ∀ i ∈ t, ‖z i‖ ≤ r) : ‖∑ k ∈ t, w k • z k‖ < r

theorem dist_affineCombination_lt_of_strictConvexSpace {V : Type u_2} {P : Type u_3} {ι : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {t : Finset ι} {w : ι → ℝ} {p₀ : P} {r : ℝ} {p : ι → P} (h0 : ∀ i ∈ t, 0 ≤ w i) (h1 : ∑ i ∈ t, w i = 1) {i j : ι} (hi : i ∈ t) (hj : j ∈ t) (hij : p i ≠ p j) (hi0 : w i ≠ 0) (hj0 : w j ≠ 0) (hp : ∀ i ∈ t, dist (p i) p₀ ≤ r) : dist ((Finset.affineCombination ℝ t p) w) p₀ < r

theorem Affine.Simplex.dist_lt_of_mem_closedInterior_of_strictConvexSpace {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) {r : ℝ} {p₀ p : P} (hp : p ∈ s.closedInterior) (hp' : ∀ (i : Fin (n + 1)), p ≠ s.points i) (hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r) : dist p p₀ < r

theorem Affine.Simplex.dist_lt_of_mem_interior_of_strictConvexSpace {V : Type u_2} {P : Type u_3} [NormedAddCommGroup V] [NormedSpace ℝ V] [StrictConvexSpace ℝ V] [PseudoMetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) {r : ℝ} {p₀ p : P} (hp : p ∈ s.interior) (hr : ∀ (i : Fin (n + 1)), dist (s.points i) p₀ ≤ r) : dist p p₀ < r