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 ≠ ⊤)
:
Text 15.0.30: Let f : ℝⁿ → [0, +∞] be a nonnegative closed convex function with f 0 = 0,
and let fᵒ be its polar in the extended sense, defined by
fᵒ x⋆ = inf { μ⋆ ≥ 0 | ⟪x, x⋆⟫ ≤ 1 + μ⋆ * f x for all x }.
Then for all x ∈ dom f and x⋆ ∈ dom fᵒ, one has
⟪x, x⋆⟫ ≤ 1 + f x * fᵒ x⋆.
In this development, ℝⁿ is Fin n → ℝ, fᵒ is polarConvex f, and effective-domain
assumptions are modeled by f x ≠ ⊤ and polarConvex f x⋆ ≠ ⊤.