English
The dual of a singleton equals the preimage of the positive cone under the corresponding linear map.
Русский
Дуал единичного множества равен предобразу положительного конуса по соответствующей линейной карте.
LaTeX
$$dual p {x} = (positive R R).comap (p.toContPerfPair x)$$
Lean4
/-- Geometric interpretation of **Farkas' lemma**. Also stronger version of the
**Hahn-Banach separation theorem** for proper cones. -/
theorem hyperplane_separation (C : ProperCone ℝ E) (hKconv : Convex ℝ K) (hKcomp : IsCompact K) (hKC : Disjoint K C) :
∃ f : StrongDual ℝ E, (∀ x ∈ C, 0 ≤ f x) ∧ ∀ x ∈ K, f x < 0 :=
by
obtain rfl | ⟨x₀, hx₀⟩ := K.eq_empty_or_nonempty
· exact ⟨0, by simp⟩
obtain ⟨f, u, v, hu, huv, hv⟩ := geometric_hahn_banach_compact_closed hKconv hKcomp C.convex C.isClosed hKC
have hv₀ : v < 0 := by simpa using hv 0 C.zero_mem
refine ⟨f, fun x hx ↦ ?_, fun x hx ↦ (hu x hx).trans_le <| huv.le.trans hv₀.le⟩
by_contra! hx₀
simpa [hx₀.ne] using
hv ((v * (f x)⁻¹) • x) (C.smul_mem hx <| le_of_lt <| mul_pos_of_neg_of_neg hv₀ <| inv_neg''.2 hx₀)
