English
Let S be convex and x,y ∈ S. For nonnegative p,q with p+q > 0, there exists z ∈ S such that (p+q)z = p x + q y. Equivalently, the point z is a weighted average of x and y lying in S.
Русский
Пусть S выпукло, и x,y ∈ S. Для неотрицательных p,q с p+q > 0 существует z ∈ S такое, что (p+q)z = p x + q y. Иными словами, z — взвешенное среднее x и y внутри S.
LaTeX
$$$\operatorname{Convex}(S) \wedge x \in S \wedge y \in S \wedge p \ge 0 \wedge q \ge 0 \Rightarrow (p+q)z = p x + q y \text{ for some } z \in S$$$
Lean4
theorem exists_mem_add_smul_eq (h : Convex 𝕜 s) {x y : E} {p q : 𝕜} (hx : x ∈ s) (hy : y ∈ s) (hp : 0 ≤ p)
(hq : 0 ≤ q) : ∃ z ∈ s, (p + q) • z = p • x + q • y :=
by
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
· use x, hx
simp
· replace hpq : 0 < p + q := (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
match_scalars <;> field_simp
