Prove IsClosed.convexHull_subset_affineSpan_isInSight except for `I…

…sInSight.of_convexHull_of_pos`

LeanCamCombi/Mathlib/Analysis/Convex/Between.lean

@@ -0,0 +1,27 @@
+import Mathlib.Analysis.Convex.Between
+import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineMap
+
+open AffineMap
+
+variable {k V P : Type*}
+
+section OrderedRing
+variable [OrderedRing k] [AddCommGroup V] [Module k V] [AddTorsor V P] {Q : AffineSubspace k P}
+  {p₀ p₁ p₂ : P}
+
+lemma AffineSubspace.mem_of_wbtw (h₀₁₂ : Wbtw k p₀ p₁ p₂) (h₀ : p₀ ∈ Q) (h₂ : p₂ ∈ Q) : p₁ ∈ Q := by
+  obtain ⟨ε, -, rfl⟩ := h₀₁₂; exact lineMap_mem _ h₀ h₂
+
+end OrderedRing
+
+section LinearOrderedField
+variable [LinearOrderedField k] [AddCommGroup V] [Module k V] [AddTorsor V P]
+  {Q : AffineSubspace k P} {p₀ p₁ p₂ : P}
+
+lemma AffineSubspace.right_mem_of_wbtw (h₀₁₂ : Wbtw k p₀ p₁ p₂) (h₀ : p₀ ∈ Q) (h₁ : p₁ ∈ Q)
+    (h₀₁ : p₀ ≠ p₁) : p₂ ∈ Q := by
+  obtain ⟨ε, -, rfl⟩ := h₀₁₂
+  have hε : ε ≠ 0 := by rintro rfl; simp at h₀₁
+  simpa [hε] using lineMap_mem ε⁻¹ h₀ h₁
+
+end LinearOrderedField

LeanCamCombi/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

@@ -3,7 +3,12 @@ import Mathlib.LinearAlgebra.AffineSpace.AffineMap
 namespace AffineMap
 variable {k V1 P1 : Type*} [Ring k] [AddCommGroup V1] [Module k V1] [AddTorsor V1 P1] {p₀ p₁ : P1}
 
-lemma lineMap_lineMap (c d : k) : lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c) := by
+@[simp] lemma lineMap_lineMap_right (c d : k) :
+    lineMap p₀ (lineMap p₀ p₁ c) d = lineMap p₀ p₁ (d * c) := by
   simp [lineMap_apply, mul_smul]
 
+-- @[simp] lemma lineMap_lineMap_left (c d : k) :
+--     lineMap (lineMap p₀ p₁ c) p₁ d = lineMap p₀ p₁ (1 - (1 - d) * c) := by
+--   simp [lineMap_apply, mul_smul]; sorry
+
 end AffineMap

LeanCamCombi/Sight/Sight.lean

@@ -1,8 +1,8 @@
 import Mathlib.Analysis.Convex.Between
 import Mathlib.Analysis.Convex.Topology
-import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.AffineMap
+import LeanCamCombi.Mathlib.Analysis.Convex.Between
 
-open AffineMap Filter Set
+open AffineMap Filter Finset Set
 open scoped Topology
 
 variable {𝕜 V P : Type*}
@@ -46,28 +46,52 @@ lemma IsOpen.eq_of_isInSight_of_left_mem (hs : IsOpen s) (hsxy : IsInSight 𝕜
   filter_upwards [hmem, hsbtw] with δ hmem hsbtw
   exact hsxy hmem hsbtw
 
+lemma IsInSight.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 : IsInSight 𝕜 (convexHull 𝕜 s) x (∑ i ∈ t, w i • a i)) {i : ι}
+    (hi : i ∈ t) (hwi : 0 < w i) : IsInSight 𝕜 (convexHull 𝕜 s) x (a i) := sorry
+
 end Module
 
 section Real
 variable [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] [TopologicalAddGroup V]
   [ContinuousSMul ℝ V] {s : Set V} {x y z : V}
 
-lemma IsClosed.exists_isInSight (hs : IsClosed s) (hy : y ∈ s) :
+lemma IsClosed.exists_wbtw_isInSight (hs : IsClosed s) (hy : y ∈ s) (x : V) :
     ∃ z ∈ s, Wbtw ℝ x z y ∧ IsInSight ℝ s x z := by
   let t : Set ℝ := Ici 0 ∩ lineMap x y ⁻¹' s
   have ht₁ : 1 ∈ t := by simpa [t]
   have ht : BddBelow t := bddBelow_Ici.inter_of_left
   let δ : ℝ := sInf t
-  have hδ₁ : δ ≤ 1 := csInf_le bddBelow_Ici.inter_of_left ht₁
+  have hδ₁ : δ ≤ 1 := csInf_le ht ht₁
   obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
     (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht
   refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩
   rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, -, h⟩
   replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h
   replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
-  rw [lineMap_lineMap] at hε
+  rw [lineMap_lineMap_right] at hε
   exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_lt <| mul_lt_of_lt_one_left hδ₀ hε₁
 
--- lemma subset_coneHull :
+lemma IsInSight.mem_convexHull_isInSight (hx : x ∉ convexHull ℝ s) (hy : y ∈ convexHull ℝ s)
+    (hxy : IsInSight ℝ (convexHull ℝ s) x y) :
+    y ∈ convexHull ℝ {z ∈ s | IsInSight ℝ (convexHull ℝ s) x z} := by
+  classical
+  obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
+  rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
+    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
+  exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
+    fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsInSight.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
+      (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩
+
+lemma IsClosed.convexHull_subset_affineSpan_isInSight (hs : IsClosed (convexHull ℝ s))
+    (hx : x ∉ convexHull ℝ s) :
+    convexHull ℝ s ⊆ affineSpan ℝ ({x} ∪ {y ∈ s | IsInSight ℝ (convexHull ℝ s) x y}) := by
+  rintro y hy
+  obtain ⟨z, hz, hxzy, hxz⟩ := hs.exists_wbtw_isInSight hy x
+  -- TODO: `calc` doesn't work with `∈` :(
+  exact AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
+    (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
+      hxz.mem_convexHull_isInSight hx hz) (ne_of_mem_of_not_mem hz hx).symm
 
 end Real