theorem ERealFunction.primalObjective_ge_neg_dualObjective {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f g : H → ↑(Set.Ioi ⊥)) (x u : H) : -fenchelDualObjective f g u ≤ primalObjective f g x

Proposition 15.9 (1): every primal value dominates the negative dual value, i.e. -fenchelDualObjective f g u ≤ primalObjective f g x.

theorem ERealFunction.iInf_primalObjective_ge_neg_iInf_dualObjective {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (f g : H → ↑(Set.Ioi ⊥)) : -⨅ (u : H), fenchelDualObjective f g u ≤ ⨅ (x : H), primalObjective f g x

Proposition 15.9 (2): the infimum of the primal objective is bounded below by the negative of the infimum of the dual objective.