Convex Analysis (Rockafellar, 1970) -- Chapter 02 -- Section 05

noncomputable sectionsection Chap02section Section05

Definiton 8.5.0. Let Unknown identifier `f`f be a proper convex function on Unknown identifier `R`sorry ^ sorry : ?m.5R^Unknown identifier `n`n and let be its recession function. The set of all vectors Unknown identifier `y`y such that is called the recession cone of Unknown identifier `f`f.

def Function.recessionCone {n : Nat} (unused variable `f`

Note: This linter can be disabled with `set_option linter.unusedVariables false`f : EuclideanSpace Real (Fin n) → Real)
    (f0_plus : EuclideanSpace Real (Fin n) → Real) :
    Set (EuclideanSpace Real (Fin n)) :=
  { y | f0_plus y <= 0 }

end Section05end Chap02