English
Let s ⊆ V and x ∉ convexHull(s). Suppose a finite family of points a_i ∈ s with nonnegative weights w_i summing to 1, and suppose x sees the convex combination ∑ w_i a_i with respect to convexHull(s). Then x sees every term a_i with positive weight. In particular, if hw_i > 0, then a_i is visible from x within convexHull(s).
Русский
Пусть s ⊆ V и x не лежит в выпуклой оболочке s. Пусть конечная сумма точек a_i ∈ s с неотрицательными весами w_i, где сумма w_i = 1, образует выпукл. комбинацию ∑ w_i a_i, которую x «видит» в convexHull(s). Тогда x видит каждый член a_i, у которого вес w_i > 0.
LaTeX
$$$\forall ι\ t\ Finset\ ι,\ a:ι\to V,\ w:ι\to\mathbb{R},\ (hw_0:\forall i\in t, 0\le w_i)\ (hw_1:\sum_{i\in t} w_i=1)\ (ha:\forall i\in t, a_i\in s)\ (hx:\ x\notin convexHull\ 𝕜\ s)\ (hw:\ IsVisible 𝕜 (convexHull 𝕜 s) x (\sum_{i\in t} w_i \cdot a_i))\ {i}\ (hi: i\in t) (hwi: 0< w_i) :\ IsVisible 𝕜 (convexHull 𝕜 s) x (a_i).$$
Lean4
/-- If a point `x` sees a convex combination of points of a set `s` through `convexHull ℝ s ∌ x`,
then it sees all terms of that combination.
Note that the converse does not hold. -/
theorem of_convexHull_of_pos {ι : Type*} {t : Finset ι} {a : ι → V} {w : ι → 𝕜} (hw₀ : ∀ i ∈ t, 0 ≤ w i)
(hw₁ : ∑ i ∈ t, w i = 1) (ha : ∀ i ∈ t, a i ∈ s) (hx : x ∉ convexHull 𝕜 s)
(hw : IsVisible 𝕜 (convexHull 𝕜 s) x (∑ i ∈ t, w i • a i)) {i : ι} (hi : i ∈ t) (hwi : 0 < w i) :
IsVisible 𝕜 (convexHull 𝕜 s) x (a i) := by
classical
obtain hwi | hwi : w i = 1 ∨ w i < 1 := eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁
· convert hw
rw [← one_smul 𝕜 (a i), ← hwi, eq_comm]
rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁
refine sum_eq_single _ (fun j hj hji ↦ ?_) (by simp [hi])
rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]
rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, h⟩
replace hε₀ : 0 < ε := hε₀.lt_of_ne <| by rintro rfl; simp at h
replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
have : 0 < 1 - ε := by linarith
have hwi : 0 < 1 - w i := by linarith
refine
hw (z := lineMap x (∑ j ∈ t, w j • a j) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹))) ?_ <|
sbtw_lineMap_iff.2
⟨(ne_of_mem_of_not_mem ((convex_convexHull ..).sum_mem hw₀ hw₁ fun i hi ↦ subset_convexHull _ _ <| ha _ hi)
hx).symm,
by positivity, (div_lt_one <| by positivity).2 ?_⟩
· have :
Wbtw 𝕜 (lineMap x (a i) ε) (lineMap x (∑ j ∈ t, w j • a j) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
(∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) :=
by
refine ⟨((1 - w i) / w i) / ((1 - ε) / ε + (1 - w i) / w i + 1), ⟨by positivity, ?_⟩, ?_⟩
· refine (div_le_one <| by positivity).2 ?_
calc
(1 - w i) / w i = 0 + (1 - w i) / w i + 0 := by simp
_ ≤ (1 - ε) / ε + (1 - w i) / w i + 1 := by gcongr <;> positivity
have : w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j :=
by
rw [smul_sum]
simp_rw [smul_smul, mul_div_cancel₀ _ hwi.ne']
exact add_sum_erase _ (fun i ↦ w i • a i) hi
simp_rw [lineMap_apply_module, ← this, smul_add, smul_smul]
match_scalars <;> field_simp <;> ring
refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_
· intro j hj
have := hw₀ j <| erase_subset _ _ hj
positivity
· rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
· exact fun j hj ↦ subset_convexHull _ _ <| ha _ <| erase_subset _ _ hj
· exact lt_add_of_pos_left _ <| by positivity
