Convex Analysis (Rockafellar, 1970) -- Chapter 03 -- Section 15 -- Part 17

Text 15.0.30: Let be a nonnegative closed convex function with Unknown identifier `f`sorry = 0 : Propf 0 = 0, and let be its polar in the extended sense, defined by

.

Then for all Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `dom`dom f and , one has .

In this development, is Fin sorry → ℝ : TypeFin Unknown identifier `n`n → ℝ, is polarConvex sorry : (Fin ?m.1 → ℝ) → ERealpolarConvex Unknown identifier `f`f, and effective-domain assumptions are modeled by Unknown identifier `f`sorry ≠ ⊤ : Propf x ≠ ⊤ and .

theorem inner_le_one_add_mul_polarConvex_of_nonneg_closedConvex_zero {n : ℕ} (f : (Fin n → ℝ) → EReal) (x xStar : Fin n → ℝ) (hx : f x ≠ ⊤) (hxStar : polarConvex f xStar ≠ ⊤) : ((x ⬝ᵥ xStar : ℝ) : EReal) ≤ (1 : EReal) + f x * polarConvex f xStar := by simpa using (inner_le_one_add_mul_polarConvex (f := f) (x := x) (xStar := xStar) hx hxStar)