fix: re-port Mathlib.Analysis.Convex.Cone.Proper (#5646)

Forward port [#19008](leanprover-community/mathlib#19008)

When I ported this file (Mathlib/Analysis/Convex/Cone/Proper.lean) I did not realize that `mathport` had used an older commit without the latest PR. I'm forward porting it now.

Mathlib/Analysis/Convex/Cone/Proper.lean

@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Apurva Nakade
 
 ! This file was ported from Lean 3 source module analysis.convex.cone.proper
-! leanprover-community/mathlib commit 74f1d61944a5a793e8c939d47608178c0a0cb0c2
+! leanprover-community/mathlib commit 147b294346843885f952c5171e9606616a8fd869
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Analysis.Convex.Cone.Dual
+import Mathlib.Analysis.InnerProductSpace.Adjoint
 
 /-!
 # Proper cones
@@ -22,8 +23,6 @@ linear programs, the results from this file can be used to prove duality theorem
 ## TODO
 
 The next steps are:
-- Prove the cone version of Farkas' lemma (2.3.4 in the reference).
-- Add comap, adjoint
 - Add convex_cone_class that extends set_like and replace the below instance
 - Define the positive cone as a proper cone.
 - Define primal and dual cone programs and prove weak duality.
@@ -38,6 +37,7 @@ The next steps are:
 
 -/
 
+open ContinuousLinearMap Filter Set
 
 namespace ConvexCone
 
@@ -163,12 +163,14 @@ variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
 variable {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
 
+variable {G : Type _} [NormedAddCommGroup G] [InnerProductSpace ℝ G]
+
 protected theorem pointed (K : ProperCone ℝ E) : (K : ConvexCone ℝ E).Pointed :=
   (K : ConvexCone ℝ E).pointed_of_nonempty_of_isClosed K.nonempty' K.isClosed
 #align proper_cone.pointed ProperCone.pointed
 
 /-- The closure of image of a proper cone under a continuous `ℝ`-linear map is a proper cone. We
-use continuous maps here so that the adjoint of f is also a map between proper cones. -/
+use continuous maps here so that the comap of f is also a map between proper cones. -/
 noncomputable def map (f : E →L[ℝ] F) (K : ProperCone ℝ E) : ProperCone ℝ F where
   toConvexCone := ConvexCone.closure (ConvexCone.map (f : E →ₗ[ℝ] F) ↑K)
   nonempty' :=
@@ -210,20 +212,101 @@ theorem mem_dual {K : ProperCone ℝ E} {y : E} : y ∈ dual K ↔ ∀ ⦃x⦄,
   rw [← mem_coe, coe_dual, mem_innerDualCone _ _]; rfl
 #align proper_cone.mem_dual ProperCone.mem_dual
 
--- TODO: add comap, adjoint
+/-- The preimage of a proper cone under a continuous `ℝ`-linear map is a proper cone. -/
+noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E
+    where
+  toConvexCone := ConvexCone.comap (f : E →ₗ[ℝ] F) S
+  nonempty' :=
+    ⟨0, by
+      simp only [ConvexCone.comap, mem_preimage, map_zero, SetLike.mem_coe, mem_coe]
+      apply ProperCone.pointed⟩
+  is_closed' := by
+    simp only [ConvexCone.comap, ContinuousLinearMap.coe_coe]
+    apply IsClosed.preimage f.2 S.isClosed
+#align proper_cone.comap ProperCone.comap
+
+@[simp]
+theorem coe_comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : (S.comap f : Set E) = f ⁻¹' S :=
+  rfl
+#align proper_cone.coe_comap ProperCone.coe_comap
+
+@[simp]
+theorem comap_id (S : ConvexCone ℝ E) : S.comap LinearMap.id = S :=
+  SetLike.coe_injective preimage_id
+#align proper_cone.comap_id ProperCone.comap_id
+
+theorem comap_comap (g : F →L[ℝ] G) (f : E →L[ℝ] F) (S : ProperCone ℝ G) :
+    (S.comap g).comap f = S.comap (g.comp f) :=
+  SetLike.coe_injective <| by congr
+#align proper_cone.comap_comap ProperCone.comap_comap
+
+@[simp]
+theorem mem_comap {f : E →L[ℝ] F} {S : ProperCone ℝ F} {x : E} : x ∈ S.comap f ↔ f x ∈ S :=
+  Iff.rfl
+#align proper_cone.mem_comap ProperCone.mem_comap
+
 end InnerProductSpace
 
 section CompleteSpace
 
 variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
 
+variable {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
+
 /-- The dual of the dual of a proper cone is itself. -/
 @[simp]
 theorem dual_dual (K : ProperCone ℝ E) : K.dual.dual = K :=
   ProperCone.ext' <|
     (K : ConvexCone ℝ E).innerDualCone_of_innerDualCone_eq_self K.nonempty' K.isClosed
 #align proper_cone.dual_dual ProperCone.dual_dual
 
+/-- This is a relative version of
+`ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem`, which we recover by setting
+`f` to be the identity map. This is a geometric interpretation of the Farkas' lemma
+stated using proper cones. -/
+theorem hyperplane_separation (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F} :
+    b ∈ K.map f ↔ ∀ y : F, adjoint f y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ :=
+  Iff.intro
+    (by
+      -- suppose `b ∈ K.map f`
+      simp only [ProperCone.mem_map, ProperCone.mem_dual, adjoint_inner_right,
+        ConvexCone.mem_closure, mem_closure_iff_seq_limit]
+      -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
+      rintro ⟨seq, hmem, htends⟩ y hinner
+      suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ;
+      exact
+        ge_of_tendsto'
+          (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id)
+            htends)
+          h
+      intro n
+      obtain ⟨_, h, hseq⟩ := hmem n
+      simpa only [← hseq, real_inner_comm] using hinner h)
+    (by
+      -- proof by contradiction
+      -- suppose `b ∉ K.map f`
+      intro h
+      contrapose! h
+      -- as `b ∉ K.map f`, there is a hyperplane `y` separating `b` from `K.map f`
+      obtain ⟨y, hxy, hyb⟩ :=
+        ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem _ (K.map f).nonempty
+          (K.map f).isClosed h
+      -- the rest of the proof is a straightforward algebraic manipulation
+      refine' ⟨y, _, hyb⟩
+      simp_rw [ProperCone.mem_dual, adjoint_inner_right]
+      intro x hxK
+      apply hxy (f x)
+      rw [ProperCone.coe_map]
+      apply subset_closure
+      rw [SetLike.mem_coe, ConvexCone.mem_map]
+      refine' ⟨x, hxK, by rw [coe_coe]⟩)
+#align proper_cone.hyperplane_separation ProperCone.hyperplane_separation
+
+theorem hyperplane_separation_of_nmem (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F}
+    (disj : b ∉ K.map f) : ∃ y : F, adjoint f y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0 := by
+  contrapose! disj; rwa [K.hyperplane_separation]
+#align proper_cone.hyperplane_separation_of_nmem ProperCone.hyperplane_separation_of_nmem
+
 end CompleteSpace
 
 end ProperCone