English
Let K be a nonempty closed convex cone in a real Hilbert space H and b ∉ K. Then there exists a vector y such that ⟨x,y⟩ ≥ 0 for all x ∈ K, and ⟨y,b⟩ < 0.
Русский
Пусть K — непустой замкнутый выпуклый конус в вещественном пространстве с скалярным произведением. Если b не принадлежит K, то существует вектор y, такой что для всех x ∈ K выполняется ⟨x,y⟩ ≥ 0 и ⟨y,b⟩ < 0.
LaTeX
$$$\\exists y\\in H, (\\forall x\\in K, \\langle x,y\\rangle \\ge 0) \\land \\langle y,b\\rangle < 0$$$
Lean4
/-- This is a stronger version of the Hahn-Banach separation theorem for closed convex cones. This
is also the geometric interpretation of Farkas' lemma. -/
theorem hyperplane_separation_of_nonempty_of_isClosed_of_notMem (K : ConvexCone ℝ H) (ne : (K : Set H).Nonempty)
(hc : IsClosed (K : Set H)) {b : H} (disj : b ∉ K) : ∃ y : H, (∀ x : H, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0 := by
-- let `z` be the point in `K` closest to `b`
obtain ⟨z, hzK, infi⟩ := exists_norm_eq_iInf_of_complete_convex ne hc.isComplete K.convex b
have hinner := (norm_eq_iInf_iff_real_inner_le_zero K.convex hzK).1 infi
use z - b
constructor
· -- the rest of the proof is a straightforward calculation
rintro x hxK
specialize hinner _ (K.add_mem hxK hzK)
rwa [add_sub_cancel_right, real_inner_comm, ← neg_nonneg, neg_eq_neg_one_mul, ← real_inner_smul_right, neg_smul,
one_smul, neg_sub] at hinner
· -- as `K` is closed and non-empty, it is pointed
have hinner₀ :=
hinner 0
(ConvexCone.Pointed.of_nonempty_of_isClosed (C := K) ne hc)
-- the rest of the proof is a straightforward calculation
rw [zero_sub, inner_neg_right, Right.neg_nonpos_iff] at hinner₀
have hbz : b - z ≠ 0 := by
rw [sub_ne_zero]
contrapose! hzK
rwa [← hzK]
rw [← neg_zero, lt_neg, ← neg_one_mul, ← real_inner_smul_left, smul_sub, neg_smul, one_smul, neg_smul, neg_sub_neg,
one_smul]
calc
0 < ⟪b - z, b - z⟫_ℝ := lt_of_not_ge ((Iff.not real_inner_self_nonpos).2 hbz)
_ = ⟪b - z, b - z⟫_ℝ + 0 := (add_zero _).symm
_ ≤ ⟪b - z, b - z⟫_ℝ + ⟪b - z, z⟫_ℝ := (add_le_add rfl.ge hinner₀)
_ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm
_ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel]
