English
Relative geometric interpretation of Farkas' Lemma: for a proper cone C and a map f, if a point b is not in the image C.map f, there exists a y with adjoint separation such that ⟪b,y⟫ < 0 and y lies in the innerDual of C.
Русский
Относительная геометрическая интерпретация леммы Фаркаса: если точка b не лежит в образе C.map f, существует y, удовлетворяющий условию разделения и лежащий в innerDual C, так что ⟪b,y⟫ < 0.
LaTeX
$$$\\neg(b\\in C.map f)\\Rightarrow \\exists y, (\\text{adjoint condition})\\land \\langle b,y\\rangle<0$$$
Lean4
/-- Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones. -/
theorem hyperplane_separation' (C : ProperCone ℝ E) (hx₀ : x₀ ∉ C) : ∃ y, (∀ x ∈ C, 0 ≤ ⟪x, y⟫) ∧ ⟪x₀, y⟫ < 0 :=
by
obtain ⟨f, hf, hf₀⟩ := C.hyperplane_separation_point hx₀
refine ⟨(InnerProductSpace.toDual ℝ E).symm f, ?_⟩
simpa [← real_inner_comm _ ((InnerProductSpace.toDual ℝ E).symm f), *]
