not_disjoint_segment_convexHull_triple

English

Stone's Separation Theorem asserts the existence of a convex set separating two disjoint convex sets by a convex cover.

Русский

Теорема Стоуна о разделении утверждает существование выпуклого множества, разделяющего две непересекающиеся выпуклые множества.

LaTeX

$$$\exists C: Set(E),\ Convex(C) \land Convex(C^c) \land s \subseteq C \land t \subseteq C^c$$$

Lean4

/-- In a tetrahedron with vertices `x`, `y`, `p`, `q`, any segment `[u, v]` joining the opposite
edges `[x, p]` and `[y, q]` passes through any triangle of vertices `p`, `q`, `z` where
`z ∈ [x, y]`. -/
theorem not_disjoint_segment_convexHull_triple {p q u v x y z : E} (hz : z ∈ segment 𝕜 x y) (hu : u ∈ segment 𝕜 x p)
    (hv : v ∈ segment 𝕜 y q) : ¬Disjoint (segment 𝕜 u v) (convexHull 𝕜 { p, q, z }) :=
  by
  rw [not_disjoint_iff]
  obtain ⟨az, bz, haz, hbz, habz, rfl⟩ := hz
  obtain rfl | haz' := haz.eq_or_lt
  · rw [zero_add] at habz
    rw [zero_smul, zero_add, habz, one_smul]
    refine ⟨v, by apply right_mem_segment, segment_subset_convexHull ?_ ?_ hv⟩ <;> simp
  obtain ⟨av, bv, hav, hbv, habv, rfl⟩ := hv
  obtain rfl | hav' := hav.eq_or_lt
  · rw [zero_add] at habv
    rw [zero_smul, zero_add, habv, one_smul]
    exact ⟨q, right_mem_segment _ _ _, subset_convexHull _ _ <| by simp⟩
  obtain ⟨au, bu, hau, hbu, habu, rfl⟩ := hu
  have hab : 0 < az * av + bz * au := by positivity
  refine
    ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q),
      ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
  · positivity
  · positivity
  · rw [← add_div, div_self]; positivity
  classical
  let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
  let z : Fin 3 → E := ![p, q, az • x + bz • y]
  have hw₀ : ∀ i, 0 ≤ w i := by
    rintro i
    fin_cases i
    · exact mul_nonneg (mul_nonneg haz hav) hbu
    · exact mul_nonneg (mul_nonneg hbz hau) hbv
    · exact mul_nonneg hau hav
  have hw : ∑ i, w i = az * av + bz * au :=
    by
    trans az * av * bu + (bz * au * bv + au * av)
    · simp [w, Fin.sum_univ_succ]
    linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu
  have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z]
  convert
    (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i) (by rwa [hw]) fun i _ => hz i :
      Finset.univ.centerMass w z ∈ _)
  rw [Finset.centerMass, hw]
  trans (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
  · module
  congr 3
  simp [w, z]

Похожие утверждения